Finite-dimensional coherent cohomology data

This file defines the output interface for the projective finiteness theorem independently of eventual cohomological vanishing. The separation matters mathematically and for the issue graph:

• finite-dimensionality of each Hⁱ(X, F) is the content of #29;
• a bound above which the groups vanish is the separate content of #30.

Mathlib currently exposes Sheaf.H only as an abelian group. This file constructs its canonical functorial k-linear lift from the central action of global functions and proves the natural comparison after forgetting scalars. LinearCohomology records that lift, while FiniteDimensionalCohomology adds exactly the still-geometric degreewise Module.Finite conclusion. These are structures carrying explicit proof data, not global existence axioms.

noncomputable def AlgebraicGeometry.Cohomology.coherentH (X : Scheme) (i : ℕ) : CategoryTheory.Functor (Coh X) AddCommGrpCat

The existing abelian-group-valued degree-i cohomology functor on coherent sheaves.

The explicit HasExt instance is required by the current Sheaf.H API.

Equations

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

structure AlgebraicGeometry.Cohomology.LinearCohomology (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] : Type (u + 2)

A functorial base-field-linear realization of Mathlib's coherent sheaf cohomology.

The natural comparison rules out an unrelated family of vector spaces with the desired dimensions: after forgetting scalars these are the actual Sheaf.H groups and maps.

• moduleH : ℕ → CategoryTheory.Functor (Coh X) (ModuleCat k)

  The base-field vector spaces Hⁱ(X, F), functorial in the coherent sheaf F.

• comparison (i : ℕ) : (self.moduleH i).comp (CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat) ≅ coherentH X i

  Forgetting the vector-space structure recovers derived-functor sheaf cohomology.

structure AlgebraicGeometry.Cohomology.FiniteDimensionalCohomology (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] extends AlgebraicGeometry.Cohomology.LinearCohomology k X : Type (u + 2)

Degreewise finite-dimensional coherent cohomology, with no eventual-vanishing claim.

This is the exact output interface for #29. A later boundedness result can extend it without re-proving or repackaging the linear comparison.

• moduleH : ℕ → CategoryTheory.Functor (Coh X) (ModuleCat k)
• comparison (i : ℕ) : (self.moduleH i).comp (CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat) ≅ coherentH X i
• finite (i : ℕ) (F : Coh X) : Module.Finite k ↑((self.moduleH i).obj F)

  Every coherent cohomology vector space is finite-dimensional.

noncomputable def AlgebraicGeometry.Cohomology.globalSectionSmul {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : M ⟶ M

Multiplication by a global function as an endomorphism of a sheaf of modules.

Equations

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

@[simp]

theorem AlgebraicGeometry.Cohomology.globalSectionSmul_app {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (U : X.Opens) (m : ↑(M.presheaf.obj (Opposite.op U))) : (ModuleCat.Hom.hom ((globalSectionSmul M r).val.app (Opposite.op U))) m = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) r • m

Evaluation of multiplication by a global function on an open set.

noncomputable def AlgebraicGeometry.Cohomology.globalSectionAction {X : Scheme} (M : X.Modules) : ↑(X.presheaf.obj (Opposite.op ⊤)) →+* CategoryTheory.End M

The ring action of global functions on a sheaf of modules.

Equations

• AlgebraicGeometry.Cohomology.globalSectionAction M = { toFun := AlgebraicGeometry.Cohomology.globalSectionSmul M, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicGeometry.Cohomology.globalSectionSmul_naturality {X : Scheme} {M N : X.Modules} (f : M ⟶ N) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.CategoryStruct.comp (globalSectionSmul M r) f = CategoryTheory.CategoryStruct.comp f (globalSectionSmul N r)

Multiplication by a global function commutes with every morphism of module sheaves.

noncomputable def AlgebraicGeometry.Cohomology.baseFieldToGlobalSections {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] : k →+* ↑(Y.presheaf.obj (Opposite.op ⊤))

The structure morphism realizes base-field scalars as global functions on a variety.

Equations

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

noncomputable def AlgebraicGeometry.Cohomology.varietyScalarAction {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) : k →+* CategoryTheory.End M

The canonical base-field action on a module sheaf over a variety.

Equations

• AlgebraicGeometry.Cohomology.varietyScalarAction Y M = (AlgebraicGeometry.Cohomology.globalSectionAction M).comp (AlgebraicGeometry.Cohomology.baseFieldToGlobalSections Y)

theorem AlgebraicGeometry.Cohomology.varietyScalarAction_naturality {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] {M N : Y.Modules} (f : M ⟶ N) (r : k) : CategoryTheory.CategoryStruct.comp ((varietyScalarAction Y M) r) f = CategoryTheory.CategoryStruct.comp f ((varietyScalarAction Y N) r)

The canonical base-field action is central on morphisms of module sheaves.

noncomputable def AlgebraicGeometry.Cohomology.coherentScalarAction {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (F : Coh Y) : k →+* CategoryTheory.End F

The canonical base-field action on a coherent sheaf.

Equations

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

theorem AlgebraicGeometry.Cohomology.coherentScalarAction_naturality {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] {F G : Coh Y} (f : F ⟶ G) (r : k) : CategoryTheory.CategoryStruct.comp ((coherentScalarAction Y F) r) f = CategoryTheory.CategoryStruct.comp f ((coherentScalarAction Y G) r)

The canonical base-field action is central on coherent-sheaf morphisms.

noncomputable def AlgebraicGeometry.Cohomology.additiveMapEndRingHom {C : Type u} {D : Type v} [CategoryTheory.Category.{w, u} C] [CategoryTheory.Category.{x, v} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [H.Additive] (A : C) : CategoryTheory.End A →+* CategoryTheory.End (H.obj A)

An additive functor induces a ring homomorphism on endomorphism rings.

Equations

• AlgebraicGeometry.Cohomology.additiveMapEndRingHom H A = { toMonoidHom := CategoryTheory.Functor.mapEnd A H, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AlgebraicGeometry.Cohomology.addCommGrpEndRingHom (A : AddCommGrpCat) : CategoryTheory.End A →+* AddMonoid.End ↑A

Endomorphisms of an abelian group in AddCommGrpCat are additive-monoid endomorphisms.

Equations

• AlgebraicGeometry.Cohomology.addCommGrpEndRingHom A = { toFun := fun (f : CategoryTheory.End A) => AddCommGrpCat.Hom.hom f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance AlgebraicGeometry.Cohomology.coherentH_additive (Y : Scheme) (i : ℕ) : (coherentH Y i).Additive

Derived coherent cohomology is additive, on any scheme.

noncomputable def AlgebraicGeometry.Cohomology.coherentHScalarAction (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (i : ℕ) (F : Coh Y) : k →+* AddMonoid.End ↑((coherentH Y i).obj F)

The base-field action induced on a derived coherent cohomology group.

Equations

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

@[reducible]

noncomputable def AlgebraicGeometry.Cohomology.coherentHModule (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (i : ℕ) (F : Coh Y) : Module k ↑((coherentH Y i).obj F)

The canonical base-field module structure on a derived coherent cohomology group.

Equations

• AlgebraicGeometry.Cohomology.coherentHModule k Y i F = Module.compHom (↑((AlgebraicGeometry.Cohomology.coherentH Y i).obj F)) (AlgebraicGeometry.Cohomology.coherentHScalarAction k Y i F)

theorem AlgebraicGeometry.Cohomology.coherentH_map_smul {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (i : ℕ) {F G : Coh Y} (f : F ⟶ G) (r : k) (x : ↑((coherentH Y i).obj F)) : (CategoryTheory.ConcreteCategory.hom ((coherentH Y i).map f)) (r • x) = r • (CategoryTheory.ConcreteCategory.hom ((coherentH Y i).map f)) x

Every derived coherent cohomology map respects the canonical base-field action.

noncomputable def AlgebraicGeometry.Cohomology.linearCoherentH (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (i : ℕ) : CategoryTheory.Functor (Coh Y) (ModuleCat k)

Coherent sheaf cohomology with its canonical functorial base-field module structure.

Equations

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

noncomputable def AlgebraicGeometry.Cohomology.linearCoherentHComparison (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (i : ℕ) : (linearCoherentH k Y i).comp (CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat) ≅ coherentH Y i

Forgetting scalars from linearCoherentH recovers Mathlib's derived cohomology functor.

Equations

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

noncomputable def AlgebraicGeometry.Cohomology.canonicalLinearCohomology {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] [IsVariety k Y] : LinearCohomology k Y

The canonical functorial linear realization of coherent sheaf cohomology on a variety.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Cohomology.FiniteDimensionalCohomology.dimension {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteDimensionalCohomology k X) (F : Coh X) (i : ℕ) : ℕ

The dimension of degree-i coherent cohomology.

Equations

• D.dimension F i = Module.finrank k ↑((D.moduleH i).obj F)

theorem AlgebraicGeometry.Cohomology.FiniteDimensionalCohomology.dimension_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteDimensionalCohomology k X) {F G : Coh X} (e : F ≅ G) (i : ℕ) : D.dimension F i = D.dimension G i

Isomorphic coherent sheaves have equal cohomology dimensions in every degree.