The Čech complex of O(d) on polynomial projective space, degreewise

cechCochainsDegreewiseAddEquiv identifies degree n of Mathlib's Čech complex of O(d), taken over the variable chart cover, with polynomialVariableCechCochains — the explicit product of homogeneous degree-zero localizations.

Main definitions

• polynomialVariableChart — the variable basic-open cover of polynomial Proj;
• twistPresheaf — the AddCommGrpCat-valued presheaf of O(d), which is what Mathlib's Čech complex consumes;
• cechCochainsDegreewiseAddEquiv — the degreewise comparison;
• polynomialVariableCechComplex — the algebraic Čech complex, with the differential carried across that comparison;
• polynomialVariableCechComplexIso — Mathlib's Čech complex is that algebraic complex.

Main statements

• piObj_polynomialVariableChart — the categorical product of the charts along a Čech index is the basic open of the product denominator;
• cechIndexEquiv_map_face — the comparison carries a Čech face restriction to the algebraic face map;
• cechCochainsDegreewiseAddEquiv_d and polynomialVariableCechComplex_d_apply — the differential is the alternating sum of the algebraic faces.

Implementation notes

Three shape mismatches separate the two sides, and each is resolved by a different mechanism.

The outer product. Degree n of the Čech complex is a categorical product ∏ᶜ in AddCommGrpCat, indexed by Fin (n + 1) → ι, while polynomialVariableCechCochains is a Pi type. AddCommGrpCat.piAddEquivPi bridges them. That is the whole reason it exists; note the AddEquiv form is needed rather than piIsoPi, because the next step is AddEquiv.piCongrRight and piIsoPi's codomain is a bundled object.

The inner product. The Čech term evaluates the presheaf on ∏ᶜ (U ∘ x), a categorical product in Opens, whereas the algebraic side names the open as a single basic open. piObj_polynomialVariableChart identifies them: the product in Opens is the infimum (the category is a complete lattice), and basicOpen_polynomialVariableCechDenominator already says the infimum of the charts is the basic open of the product. This is an equality of opens, not merely an isomorphism, so it transports through eqToIso rather than a comparison map.

The coefficients. cechTermSectionAddEquiv lands in the Type-valued sheaf, while the Čech complex needs the AddCommGrpCat-valued presheaf. No conversion is required: associatedPresheafInAddCommGrp is defined by bundling exactly that section type, so the two are definitionally equal and the per-index equivalence is reused unchanged.

Degree n of the complex is definitionally the product over Fin (n + 1) → ι — no dsimp or unfolding lemma is needed to expose it, and AddCommGrpCat.piAddEquivPi applies to it directly.

The differential. cechCochainsDegreewiseAddEquiv compares one degree at a time; polynomialVariableCechComplex carries the differential across it, so d ∘ d = 0 and the comparison isomorphism are both free, and the alternating-sum formula is a theorem about the complex rather than an obligation inside its construction.

That formula is stated twice. cechCochainsDegreewiseAddEquiv_d reads Mathlib's differential through the comparison, and polynomialVariableCechComplex_d_apply phrases the same fact against the algebraic complex's own d. The first is the one to prove things with: the second puts the equation under the complex's carrier coercion, where .X n is semireducible and CochainComplex.of.d hides behind a dite, so a cochain has to be typed in the carrier rather than in the bare Pi type for anything to rewrite.

Tags

Čech complex, projective space, twisting sheaf, homogeneous localization

noncomputable def AlgebraicGeometry.Proj.polynomialVariableChart (ι k : Type u) [Field k] : ι → TopologicalSpace.Opens ↑(ProjectiveSpectrum.top (MvPolynomial.polynomialGrading ι k))

The variable basic-open cover of polynomial Proj: the chart where the i-th coordinate is invertible. This is the cover the algebraic Čech terms are indexed by.

Equations

• AlgebraicGeometry.Proj.polynomialVariableChart ι k i = ProjectiveSpectrum.basicOpen (MvPolynomial.polynomialGrading ι k) (MvPolynomial.X i)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.twistPresheaf (ι k : Type u) [Field k] (d : ℕ) : TopCat.Presheaf AddCommGrpCat (ProjectiveSpectrum.top (MvPolynomial.polynomialGrading ι k))

The AddCommGrpCat-valued presheaf of O(d) on polynomial Proj.

Mathlib's Čech complex is built from a presheaf valued in a preadditive category with products, so the Type-valued sheaf that the section comparisons are stated against cannot be used directly. Its underlying type is unchanged, which is what lets cechTermSectionAddEquiv be reused here without a conversion step.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.piObj_polynomialVariableChart (ι k : Type u) [Field k] {n : ℕ} (x : Fin (n + 1) → ι) : ∏ᶜ polynomialVariableChart ι k ∘ x = ProjectiveSpectrum.basicOpen (MvPolynomial.polynomialGrading ι k) (MvPolynomial.polynomialVariableCechDenominator ι k x)

The categorical product of the charts along a Čech index is the basic open of the product denominator.

The product in Opens is the infimum, because the category is a complete lattice; the rest is basicOpen_polynomialVariableCechDenominator. The conclusion is an equality of opens rather than an isomorphism, which is what lets the presheaf be transported across it by eqToIso.

noncomputable def AlgebraicGeometry.Proj.cechIndexEquiv (ι k : Type u) [Field k] (d : ℕ) {n : ℕ} (x : Fin (n + 1) → ι) : ↑((twistPresheaf ι k d).obj (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x))) ≃+ ↥(MvPolynomial.polynomialVariableCechTerm ι k d n x)

One index of the degreewise comparison: the sections of O(d) on the categorical product of charts along x, identified with the explicit homogeneous localization at that index.

Two steps: the identification of the open (piObj_polynomialVariableChart, transported by eqToIso) and the section comparison (cechTermSectionAddEquiv).

Equations

• AlgebraicGeometry.Proj.cechIndexEquiv ι k d x = (CategoryTheory.eqToIso ⋯).addCommGroupIsoToAddEquiv.trans (AlgebraicGeometry.Proj.cechTermSectionAddEquiv ι k d x).symm

noncomputable def AlgebraicGeometry.Proj.cechCochainsDegreewiseAddEquiv (ι k : Type u) [Field k] (d n : ℕ) : ↑(((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).obj (twistPresheaf ι k d)).X n) ≃+ MvPolynomial.polynomialVariableCechCochains ι k d n

Degree n of the Čech complex of O(d) over the variable charts is the explicit product of homogeneous degree-zero localizations.

The outer product is AddCommGrpCat.piAddEquivPi and each factor is cechIndexEquiv. Degreewise only — the Čech differential is not claimed to correspond here.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.cechCochainsDegreewiseAddEquiv_apply (ι k : Type u) [Field k] (d n : ℕ) (t : ↑(((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).obj (twistPresheaf ι k d)).X n)) (x : Fin (n + 1) → ι) : (cechCochainsDegreewiseAddEquiv ι k d n) t x = (cechIndexEquiv ι k d x) ((AddCommGrpCat.piAddEquivPi fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).I) => (twistPresheaf ι k d).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).obj i))) t x)

The degreewise comparison, read one index at a time: project, then compare that index.

Stated against AddCommGrpCat.piAddEquivPi rather than Limits.Pi.π because the latter needs its family supplied explicitly to elaborate; AddCommGrpCat.piIsoPi_hom_eval_apply converts between them where a caller actually needs the categorical projection.

theorem AlgebraicGeometry.Proj.cechCochainsDegreewiseAddEquiv_symm_apply (ι k : Type u) [Field k] (d n : ℕ) (s : MvPolynomial.polynomialVariableCechCochains ι k d n) (x : Fin (n + 1) → ι) : (AddCommGrpCat.piAddEquivPi fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).I) => (twistPresheaf ι k d).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).obj i))) ((cechCochainsDegreewiseAddEquiv ι k d n).symm s) x = (cechIndexEquiv ι k d x).symm (s x)

The inverse comparison, read one index at a time.

theorem AlgebraicGeometry.Proj.cechIndexEquiv_map_face (ι k : Type u) [Field k] (d : ℕ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) (g : ∏ᶜ polynomialVariableChart ι k ∘ x ⟶ ∏ᶜ polynomialVariableChart ι k ∘ x ∘ j.succAbove) (w : ↑((twistPresheaf ι k d).obj (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x ∘ j.succAbove)))) : (cechIndexEquiv ι k d x) ((CategoryTheory.ConcreteCategory.hom ((twistPresheaf ι k d).map g.op)) w) = (MvPolynomial.polynomialVariableCechFace ι k d x j) ((cechIndexEquiv ι k d (x ∘ j.succAbove)) w)

The per-index square: the comparison carries a Čech face restriction to the algebraic face.

The morphism g is left arbitrary on purpose. It ranges over Opens, where there is at most one morphism between two objects, so the face inclusion Mathlib's Čech nerve produces is the morphism here and needs no separate identification — Subsingleton.elim supplies it. The two eqToHoms identifying the categorical product of charts with the basic open of the denominator collapse into the same twistPresheaf.map, leaving exactly the restriction that cechTermSectionAddEquiv_res_face handles.

The explicit algebraic Čech complex

cechCochainsDegreewiseAddEquiv compares one degree at a time. Carrying the differential across it turns that family of comparisons into an isomorphism of cochain complexes, which is what makes Hⁱ(Pⁿ, O(d)) the cohomology of a complex written in homogeneous localizations.

The differential is defined by transport rather than as an alternating sum. That is deliberate: d ∘ d = 0 and the comparison isomorphism are then both free, and the alternating-sum formula becomes a separate lemma about this complex instead of a proof obligation inside its construction.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.cechComplexOfTwist (ι k : Type u) [Field k] (d : ℕ) : CochainComplex AddCommGrpCat ℕ

Mathlib's Čech complex of O(d) over the variable charts.

Equations

• AlgebraicGeometry.Proj.cechComplexOfTwist ι k d = (CategoryTheory.cechComplexFunctor (AlgebraicGeometry.Proj.polynomialVariableChart ι k)).obj (AlgebraicGeometry.Proj.twistPresheaf ι k d)

noncomputable def AlgebraicGeometry.Proj.cechCochainsIso (ι k : Type u) [Field k] (d n : ℕ) : (cechComplexOfTwist ι k d).X n ≅ AddCommGrpCat.of (MvPolynomial.polynomialVariableCechCochains ι k d n)

The degreewise comparison, as an isomorphism of bundled abelian groups.

Equations

• AlgebraicGeometry.Proj.cechCochainsIso ι k d n = (AlgebraicGeometry.Proj.cechCochainsDegreewiseAddEquiv ι k d n).toAddCommGrpIso

theorem AlgebraicGeometry.Proj.cechCochainsDegreewiseAddEquiv_d (ι k : Type u) [Field k] (d n : ℕ) (t : ↑((cechComplexOfTwist ι k d).X n)) (x : Fin (n + 2) → ι) : (cechCochainsDegreewiseAddEquiv ι k d (n + 1)) ((CategoryTheory.ConcreteCategory.hom ((cechComplexOfTwist ι k d).d n (n + 1))) t) x = ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.polynomialVariableCechFace ι k d x j) ((cechCochainsDegreewiseAddEquiv ι k d n) t (x ∘ j.succAbove))

The Čech differential in homogeneous localizations. Reading Mathlib's Čech differential through the degreewise comparison gives the alternating sum of the algebraic face maps.

This is the computable form of the differential, and it is stated against the comparison rather than against polynomialVariableCechComplex's own d on purpose: the latter puts the equation under the complex's carrier coercion, where .X n is semireducible and neither rw nor show reaches the Pi type being indexed. polynomialVariableCechComplex_d_apply derives that form from this one, where CochainComplex.of_d applies to a morphism instead.

noncomputable def AlgebraicGeometry.Proj.polynomialVariableCechComplex (ι k : Type u) [Field k] (d : ℕ) : CochainComplex AddCommGrpCat ℕ

The algebraic Čech complex of O(d): in degree n, the explicit product of degree-zero homogeneous localizations, with the differential carried over from Mathlib's Čech complex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.polynomialVariableCechComplexIso (ι k : Type u) [Field k] (d : ℕ) : cechComplexOfTwist ι k d ≅ polynomialVariableCechComplex ι k d

The Čech complex of O(d) over the variable charts is the explicit algebraic complex.

Composed with the Čech-to-derived comparison of DerivedAlgGeo.Topology.Sheaves.Cech.GlobalComparison, this presents every Hⁱ(Pⁿ, O(d)) as the cohomology of a complex of homogeneous localizations.

Equations

• AlgebraicGeometry.Proj.polynomialVariableCechComplexIso ι k d = HomologicalComplex.Hom.isoOfComponents (fun (n : ℕ) => AlgebraicGeometry.Proj.cechCochainsIso ι k d n) ⋯

theorem AlgebraicGeometry.Proj.polynomialVariableCechComplex_d_apply (ι k : Type u) [Field k] (d n : ℕ) (s : ↑((polynomialVariableCechComplex ι k d).X n)) (x : Fin (n + 2) → ι) : (CategoryTheory.ConcreteCategory.hom ((polynomialVariableCechComplex ι k d).d n (n + 1))) s x = ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.polynomialVariableCechFace ι k d x j) (s (x ∘ j.succAbove))

The differential of the algebraic Čech complex, in coordinates.

The complex is defined by transport, so this is what makes it computable: Hⁱ(Pⁿ, O(d)) is the cohomology of a complex of homogeneous localizations whose differential is the alternating sum of the explicit face maps.

s is taken in the complex's own carrier rather than in polynomialVariableCechCochains ι k d n. The two are definitionally equal, but only the former lets the differential be rewritten: CochainComplex.of.d hides behind a dite that only CochainComplex.of_d opens, and with s typed as the bare Pi type the rewritten term fails to be type-correct at instances transparency.

The same complex for a twist of either sign

Everything above is repeated for d : ℤ. Nothing in this layer knows about the sign: the three shape mismatches recorded in the module docstring — the outer product, the inner product, and the coefficients — are all statements about the cover, and piObj_polynomialVariableChart is therefore reused verbatim rather than restated. The only twist-dependent inputs are the section comparison intCechTermSectionAddEquiv and its face compatibility intCechTermSectionAddEquiv_res_face, and both are already proved with the sign absorbed.

This is the layer #332's dévissage consumes. The nonnegative layer above is not a special case of it — natShift and intShift are different graded families, related only by transport — so it is kept as it stands and #340's vanishing theorem continues to read it.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.intTwistPresheaf (ι k : Type u) [Field k] (d : ℤ) : TopCat.Presheaf AddCommGrpCat (ProjectiveSpectrum.top (MvPolynomial.polynomialGrading ι k))

The AddCommGrpCat-valued presheaf of O(d) for an integer twist.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.intCechIndexEquiv (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 1) → ι) : ↑((intTwistPresheaf ι k d).obj (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x))) ≃+ ↥(MvPolynomial.polynomialVariableIntCechTerm ι k d n x)

One index of the degreewise comparison, for an integer twist.

Equations

• AlgebraicGeometry.Proj.intCechIndexEquiv ι k d x = (CategoryTheory.eqToIso ⋯).addCommGroupIsoToAddEquiv.trans (AlgebraicGeometry.Proj.intCechTermSectionAddEquiv ι k d x).symm

noncomputable def AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : ↑(((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).obj (intTwistPresheaf ι k d)).X n) ≃+ MvPolynomial.polynomialVariableIntCechCochains ι k d n

Degree n of the Čech complex of an integer twist O(d) over the variable charts is the explicit product of homogeneous degree-zero localizations.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv_apply (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (t : ↑(((CategoryTheory.cechComplexFunctor (polynomialVariableChart ι k)).obj (intTwistPresheaf ι k d)).X n)) (x : Fin (n + 1) → ι) : (intCechCochainsDegreewiseAddEquiv ι k d n) t x = (intCechIndexEquiv ι k d x) ((AddCommGrpCat.piAddEquivPi fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).I) => (intTwistPresheaf ι k d).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).obj i))) t x)

The degreewise comparison, read one index at a time.

theorem AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv_symm_apply (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (s : MvPolynomial.polynomialVariableIntCechCochains ι k d n) (x : Fin (n + 1) → ι) : (AddCommGrpCat.piAddEquivPi fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).I) => (intTwistPresheaf ι k d).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := polynomialVariableChart ι k }.cech).obj { len := n })).obj i))) ((intCechCochainsDegreewiseAddEquiv ι k d n).symm s) x = (intCechIndexEquiv ι k d x).symm (s x)

The inverse comparison, read one index at a time.

theorem AlgebraicGeometry.Proj.intCechIndexEquiv_map_face (ι k : Type u) [Field k] (d : ℤ) {n : ℕ} (x : Fin (n + 2) → ι) (j : Fin (n + 2)) (g : ∏ᶜ polynomialVariableChart ι k ∘ x ⟶ ∏ᶜ polynomialVariableChart ι k ∘ x ∘ j.succAbove) (w : ↑((intTwistPresheaf ι k d).obj (Opposite.op (∏ᶜ polynomialVariableChart ι k ∘ x ∘ j.succAbove)))) : (intCechIndexEquiv ι k d x) ((CategoryTheory.ConcreteCategory.hom ((intTwistPresheaf ι k d).map g.op)) w) = (MvPolynomial.polynomialVariableIntCechFace ι k d x j) ((intCechIndexEquiv ι k d (x ∘ j.succAbove)) w)

The per-index square for an integer twist: the comparison carries a Čech face restriction to the algebraic face. As in the nonnegative case, g is arbitrary because Opens is thin.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Proj.intCechComplexOfTwist (ι k : Type u) [Field k] (d : ℤ) : CochainComplex AddCommGrpCat ℕ

Mathlib's Čech complex of an integer twist O(d) over the variable charts.

Equations

• AlgebraicGeometry.Proj.intCechComplexOfTwist ι k d = (CategoryTheory.cechComplexFunctor (AlgebraicGeometry.Proj.polynomialVariableChart ι k)).obj (AlgebraicGeometry.Proj.intTwistPresheaf ι k d)

noncomputable def AlgebraicGeometry.Proj.intCechCochainsIso (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) : (intCechComplexOfTwist ι k d).X n ≅ AddCommGrpCat.of (MvPolynomial.polynomialVariableIntCechCochains ι k d n)

The degreewise comparison for an integer twist, as an isomorphism of bundled abelian groups.

Equations

• AlgebraicGeometry.Proj.intCechCochainsIso ι k d n = (AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv ι k d n).toAddCommGrpIso

theorem AlgebraicGeometry.Proj.intCechCochainsDegreewiseAddEquiv_d (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (t : ↑((intCechComplexOfTwist ι k d).X n)) (x : Fin (n + 2) → ι) : (intCechCochainsDegreewiseAddEquiv ι k d (n + 1)) ((CategoryTheory.ConcreteCategory.hom ((intCechComplexOfTwist ι k d).d n (n + 1))) t) x = ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.polynomialVariableIntCechFace ι k d x j) ((intCechCochainsDegreewiseAddEquiv ι k d n) t (x ∘ j.succAbove))

The Čech differential of an integer twist in homogeneous localizations.

noncomputable def AlgebraicGeometry.Proj.polynomialVariableIntCechComplex (ι k : Type u) [Field k] (d : ℤ) : CochainComplex AddCommGrpCat ℕ

The algebraic Čech complex of an integer twist O(d), with the differential carried over from Mathlib's Čech complex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.polynomialVariableIntCechComplexIso (ι k : Type u) [Field k] (d : ℤ) : intCechComplexOfTwist ι k d ≅ polynomialVariableIntCechComplex ι k d

The Čech complex of an integer twist O(d) over the variable charts is the explicit algebraic complex.

Equations

• AlgebraicGeometry.Proj.polynomialVariableIntCechComplexIso ι k d = HomologicalComplex.Hom.isoOfComponents (fun (n : ℕ) => AlgebraicGeometry.Proj.intCechCochainsIso ι k d n) ⋯

theorem AlgebraicGeometry.Proj.polynomialVariableIntCechComplex_d_apply (ι k : Type u) [Field k] (d : ℤ) (n : ℕ) (s : ↑((polynomialVariableIntCechComplex ι k d).X n)) (x : Fin (n + 2) → ι) : (CategoryTheory.ConcreteCategory.hom ((polynomialVariableIntCechComplex ι k d).d n (n + 1))) s x = ∑ j : Fin (n + 2), (-1) ^ ↑j • (MvPolynomial.polynomialVariableIntCechFace ι k d x j) (s (x ∘ j.succAbove))

The differential of the algebraic Čech complex of an integer twist, in coordinates.