Degree-zero cohomology and linear global sections

For a scheme over a field, global sections of a module sheaf carry the canonical base-field action obtained from the structure morphism. This file packages that module and proves that Mathlib's derived-functor H⁰ comparison is linear for the canonical cohomology action.

The resulting linear equivalence is the transport step needed to turn finite-dimensional coherent H⁰ into finite-dimensional global sections. It assumes no projectivity, coherence, or finiteness theorem itself.

Main results

• linearGlobalSectionsObj packages sections over ⊤ as a k-module;
• coherentHZeroSectionsLinearEquiv is the canonical linear H⁰/sections comparison;
• module_finite_linearGlobalSectionsObj transports module-finiteness across it.

@[reducible]

noncomputable def AlgebraicGeometry.Cohomology.globalSectionsModule {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) : Module k ↑(M.presheaf.obj (Opposite.op ⊤))

The base-field module structure on global sections induced by the structure morphism.

Equations

• AlgebraicGeometry.Cohomology.globalSectionsModule Y M = Module.compHom (↑(M.presheaf.obj (Opposite.op ⊤))) (AlgebraicGeometry.Cohomology.baseFieldToGlobalSections Y)

noncomputable def AlgebraicGeometry.Cohomology.linearGlobalSectionsObj {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) : ModuleCat k

Global sections over ⊤, packaged with their canonical base-field module structure.

Equations

• AlgebraicGeometry.Cohomology.linearGlobalSectionsObj Y M = ModuleCat.of k ↑(M.presheaf.obj (Opposite.op ⊤))

noncomputable def AlgebraicGeometry.Cohomology.coherentHZeroSectionsAddEquiv (Y : Scheme) (F : Coh Y) : ↑((coherentH Y 0).obj F) ≃+ ↑(F.obj.presheaf.obj (Opposite.op ⊤))

The canonical additive equivalence between coherent H⁰ and sections over ⊤.

Equations

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

theorem AlgebraicGeometry.Cohomology.coherentHZeroSectionsAddEquiv_naturality (Y : Scheme) {F G : Coh Y} (f : F ⟶ G) (x : ↑((coherentH Y 0).obj F)) : (ModuleCat.Hom.hom (((Coh.ι Y).map f).val.app (Opposite.op ⊤))) ((coherentHZeroSectionsAddEquiv Y F) x) = (coherentHZeroSectionsAddEquiv Y G) ((CategoryTheory.ConcreteCategory.hom ((coherentH Y 0).map f)) x)

The degree-zero cohomology/sections comparison is natural in the coherent sheaf.

theorem AlgebraicGeometry.Cohomology.coherentHZeroSectionsAddEquiv_smul {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) (r : k) (x : ↑((linearCoherentH k Y 0).obj F)) : (have this := (coherentHZeroSectionsAddEquiv Y F) (r • x); this) = r • have this := (coherentHZeroSectionsAddEquiv Y F) x; this

The degree-zero cohomology/sections comparison respects the canonical base-field actions.

noncomputable def AlgebraicGeometry.Cohomology.coherentHZeroSectionsLinearEquiv {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) : ↑((linearCoherentH k Y 0).obj F) ≃ₗ[k] ↑(linearGlobalSectionsObj Y ((Coh.ι Y).obj F))

The canonical H⁰/global-sections comparison as a base-field linear equivalence.

Equations

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

theorem AlgebraicGeometry.Cohomology.module_finite_linearGlobalSectionsObj {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) (h : Module.Finite k ↑((linearCoherentH k Y 0).obj F)) : Module.Finite k ↑(linearGlobalSectionsObj Y ((Coh.ι Y).obj F))

Finite-dimensional coherent H⁰ implies finite-dimensional global sections.