The base-field-linear form of the Čech comparison

Everything in the Čech lane is valued in AddCommGrpCat, and the interface a finiteness theorem has to discharge is not: Module.Finite k needs the k-module structure that coherentScalarAction supplies. This file supplies the missing half.

The k-action on a cohomology group is not extra data. For r : k, multiplication by r is an endomorphism of the sheaf -- varietyScalarAction, built from the central action of global functions through the variety's structure morphism -- and the action on cohomology is the map that endomorphism induces. So both sides of the Čech comparison carry an action for the same reason, and k-linearity of the comparison is exactly the statement that it commutes with the maps induced by an endomorphism, which is cechComparisonAddEquiv_naturality.

noncomputable def AlgebraicGeometry.Cohomology.cechCohomologyFunctor {X : TopCat} {ind : Type u} (U : ind → TopologicalSpace.Opens ↑X) (n : ℕ) : CategoryTheory.Functor (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) AddCommGrpCat

Čech cohomology of an abelian sheaf on a space, as a functor.

The comparison is stated against cechCohomology, which is an abbreviation for the same homology group; naming the functor is what lets an endomorphism of the sheaf act.

Equations

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

instance AlgebraicGeometry.Cohomology.cechCohomologyFunctor_additive {X : TopCat} {ind : Type u} (U : ind → TopologicalSpace.Opens ↑X) (n : ℕ) : (cechCohomologyFunctor U n).Additive

noncomputable def AlgebraicGeometry.Cohomology.cechScalarAction (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (n : ℕ) : k →+* AddMonoid.End ↑((cechCohomologyFunctor U n).obj ((Scheme.Modules.toSheaf Y).obj M))

The base-field action on the Čech cohomology of a module sheaf over a variety.

It is the action of varietyScalarAction pushed through two additive functors: the forgetful functor to abelian sheaves, and Čech cohomology.

Equations

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

@[reducible]

noncomputable def AlgebraicGeometry.Cohomology.cechCohomologyModule (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (n : ℕ) : Module k ↑((cechCohomologyFunctor U n).obj ((Scheme.Modules.toSheaf Y).obj M))

The base-field module structure on Čech cohomology.

Equations

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

theorem AlgebraicGeometry.Cohomology.cechScalarAction_apply {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (n : ℕ) (r : k) (x : ↑((cechCohomologyFunctor U n).obj ((Scheme.Modules.toSheaf Y).obj M))) : ((cechScalarAction k Y M U n) r) x = (AddCommGrpCat.Hom.hom ((cechCohomologyFunctor U n).map ((Scheme.Modules.toSheaf Y).map ((varietyScalarAction Y M) r)))) x

Scalar multiplication on Čech cohomology is the map induced by multiplication on the sheaf.

theorem AlgebraicGeometry.Cohomology.cechComparisonAddEquiv_smul {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (I : CategoryTheory.InjectiveResolution ((Scheme.Modules.toSheaf Y).obj M)) (hExt : CategoryTheory.HasExt (TopCat.Sheaf AddCommGrpCat ↑Y.toPresheafedSpace)) (hcover : CategoryTheory.Sheaf.IsCechAcyclicCover U ((Scheme.Modules.toSheaf Y).obj M)) (n : ℕ) (r : k) (x : ↑(CategoryTheory.cechCohomology U ((Scheme.Modules.toSheaf Y).obj M).obj n)) : (CategoryTheory.Sheaf.cechComparisonAddEquiv CategoryTheory.Limits.isTerminalTop U I hExt hcover n) (((cechScalarAction k Y M U n) r) x) = (CategoryTheory.Sheaf.H.map ((Scheme.Modules.toSheaf Y).map ((varietyScalarAction Y M) r)) n) ((CategoryTheory.Sheaf.cechComparisonAddEquiv CategoryTheory.Limits.isTerminalTop U I hExt hcover n) x)

The Čech-to-derived comparison is k-linear.

The scalar action on both sides is induced by one endomorphism of the sheaf, so this is the naturality square of cechComparisonAddEquiv at multiplication by r, with the canonical lift of that endomorphism to the chosen resolution.

theorem AlgebraicGeometry.Cohomology.cechComparisonAddEquiv_coherentSmul {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (I : CategoryTheory.InjectiveResolution ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (hcover : CategoryTheory.Sheaf.IsCechAcyclicCover U ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (n : ℕ) (r : k) (x : ↑(CategoryTheory.cechCohomology U ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F)).obj n)) : (CategoryTheory.Sheaf.cechComparisonAddEquiv CategoryTheory.Limits.isTerminalTop U I ⋯ hcover n) (((cechScalarAction k Y ((Coh.ι Y).obj F) U n) r) x) = ((coherentHScalarAction k Y n F) r) ((CategoryTheory.Sheaf.cechComparisonAddEquiv CategoryTheory.Limits.isTerminalTop U I ⋯ hcover n) x)

The Čech comparison against coherentScalarAction.

This is the form the finiteness interface consumes: the target is the group coherentH names, carrying the action coherentScalarAction supplies, and the comparison respects it.

The HasExt reconciliation is made here and is explicit. coherentH fixes its witness as HasExt.standard _ at HasExt.{u + 1}, while the Čech lane passes the witness positionally so that instance search cannot pick HasExt.{u} -- a different group. The two conventions meet by instantiating the positional witness at HasExt.standard _, written out below rather than left to elaboration.

noncomputable def AlgebraicGeometry.Cohomology.cechComparisonLinearEquiv {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (I : CategoryTheory.InjectiveResolution ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (hcover : CategoryTheory.Sheaf.IsCechAcyclicCover U ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (n : ℕ) : ↑((cechCohomologyFunctor U n).obj ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) ≃ₗ[k] ↑((linearCoherentH k Y n).obj F)

The Čech comparison as a k-linear equivalence.

This is the form the finiteness interface consumes: the underlying additive equivalence is the Čech-to-derived comparison, and the scalar action it respects is coherentScalarAction.

Equations

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

theorem AlgebraicGeometry.Cohomology.module_finite_linearCoherentH_of_cech {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) {ind : Type u} (U : ind → TopologicalSpace.Opens ↥Y) (I : CategoryTheory.InjectiveResolution ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (hcover : CategoryTheory.Sheaf.IsCechAcyclicCover U ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F))) (n : ℕ) (hfin : Module.Finite k ↑((cechCohomologyFunctor U n).obj ((Scheme.Modules.toSheaf Y).obj ((Coh.ι Y).obj F)))) : Module.Finite k ↑((linearCoherentH k Y n).obj F)

Finite-dimensionality transfers from the Čech complex to the interface group.

FiniteDimensionalCohomology asks for Module.Finite k ((moduleH i).obj F), and linearCoherentH is the realization that supplies moduleH. The Čech side is where a finite spanning set is actually available; this carries it across, and it is the k-linearity of the comparison -- not the additive equivalence alone -- that makes the transfer legitimate.