Additivity of the geometric Euler characteristic

This file proves that the finite coherent-cohomology Euler characteristic is additive in short exact sequences. Mathlib supplies the additive Ext long exact sequence. The only additional datum requested here is that its connecting homomorphisms are linear over the base field; LinearConnectingMaps records precisely that compatibility and no exactness axiom.

The result is then descended explicitly to the Grothendieck group of coherent sheaves.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Cohomology.coherentSheafShortComplex {X : Scheme} (S : CategoryTheory.ShortComplex (Coh X)) : CategoryTheory.ShortComplex (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat)

The short exact sequence of abelian sheaves underlying a short exact sequence of coherent sheaves.

Equations

• AlgebraicGeometry.Cohomology.coherentSheafShortComplex S = (S.map (AlgebraicGeometry.Coh.ι X)).map (AlgebraicGeometry.Scheme.Modules.toSheaf X)

theorem AlgebraicGeometry.Cohomology.coherentSheafShortComplex_shortExact {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) : (coherentSheafShortComplex S).ShortExact

Exactness survives both forgetful functors from coherent module sheaves to abelian sheaves.

noncomputable def AlgebraicGeometry.Cohomology.coherentConnectingMap {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) (i : ℕ) : (coherentH X i).obj S.X₃ ⟶ (coherentH X (i + 1)).obj S.X₁

The additive connecting homomorphism in the Ext long exact sequence underlying coherent sheaf cohomology.

Equations

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

structure AlgebraicGeometry.Cohomology.FiniteCohomology.LinearConnectingMaps {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) : Type (u + 1)

A linear lift of the connecting maps in the actual Ext long exact sequence.

Mathlib currently exposes the connecting morphisms only as additive group homomorphisms. The compatibility field says that δ forgets to exactly that morphism. Exactness is proved below from Abelian.Ext.covariant_sequence_exact₁/₂/₃; it is not stored here.

• δ (i : ℕ) : (D.moduleH i).obj S.X₃ ⟶ (D.moduleH (i + 1)).obj S.X₁

  The degree-i linear connecting morphism.

• commutes (i : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (ModuleCat k) AddCommGrpCat).map (self.δ i)) ((D.comparison (i + 1)).hom.app S.X₁) = CategoryTheory.CategoryStruct.comp ((D.comparison i).hom.app S.X₃) (coherentConnectingMap S hS i)

  After forgetting scalars and applying comparison, δ is the Ext connecting map.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.exact₂ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) (i : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom ((D.moduleH i).map S.f)) ⇑(CategoryTheory.ConcreteCategory.hom ((D.moduleH i).map S.g))

Exactness at the middle cohomology group in each degree, transported from Mathlib's Ext long exact sequence.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.LinearConnectingMaps.exact₃ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex (Coh X)} {hS : S.ShortExact} (L : D.LinearConnectingMaps S hS) (i : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom ((D.moduleH i).map S.g)) ⇑(CategoryTheory.ConcreteCategory.hom (L.δ i))

Exactness between the quotient map in degree i and the connecting morphism.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.LinearConnectingMaps.exact₁ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex (Coh X)} {hS : S.ShortExact} (L : D.LinearConnectingMaps S hS) (i : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (L.δ i)) ⇑(CategoryTheory.ConcreteCategory.hom ((D.moduleH (i + 1)).map S.f))

Exactness between the connecting morphism out of degree i and the inclusion map in degree i + 1.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.injective_map_f_zero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((D.moduleH 0).map S.f))

The first map of the long exact sequence is injective in degree zero.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic_additive {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex (Coh X)} {hS : S.ShortExact} (L : D.LinearConnectingMaps S hS) : D.eulerCharacteristic S.X₂ = D.eulerCharacteristic S.X₁ + D.eulerCharacteristic S.X₃

The geometric Euler characteristic is additive on a short exact sequence of coherent sheaves, provided the additive Ext connecting maps have the stated linear lifts.

def AlgebraicGeometry.Cohomology.FiniteCohomology.coherentShortComplex {X : Scheme} (S : CategoryTheory.ShortComplex X.Modules) (h₁ : Scheme.Modules.IsCoherent X S.X₁) (h₂ : Scheme.Modules.IsCoherent X S.X₂) (h₃ : Scheme.Modules.IsCoherent X S.X₃) : CategoryTheory.ShortComplex (Coh X)

Regard a short complex of module sheaves with coherent terms as a short complex in Coh X.

Equations

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

@[simp]

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.coherentShortComplex_map_inclusion {X : Scheme} (S : CategoryTheory.ShortComplex X.Modules) (h₁ : Scheme.Modules.IsCoherent X S.X₁) (h₂ : Scheme.Modules.IsCoherent X S.X₂) (h₃ : Scheme.Modules.IsCoherent X S.X₃) : (coherentShortComplex S h₁ h₂ h₃).map (Coh.ι X) = S

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.coherentShortComplex_shortExact {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (h₁ : Scheme.Modules.IsCoherent X S.X₁) (h₂ : Scheme.Modules.IsCoherent X S.X₂) (h₃ : Scheme.Modules.IsCoherent X S.X₃) : (coherentShortComplex S h₁ h₂ h₃).ShortExact

Exactness of a module-sheaf short complex reflects to the coherent full subcategory.

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.eulerCharacteristic_additive_modules {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (h₁ : Scheme.Modules.IsCoherent X S.X₁) (h₂ : Scheme.Modules.IsCoherent X S.X₂) (h₃ : Scheme.Modules.IsCoherent X S.X₃) (L : D.LinearConnectingMaps (coherentShortComplex S h₁ h₂ h₃) ⋯) : D.eulerCharacteristic { obj := S.X₂, property := h₂ } = D.eulerCharacteristic { obj := S.X₁, property := h₁ } + D.eulerCharacteristic { obj := S.X₃, property := h₃ }

X.Modules-level form of Euler additivity: coherent hypotheses on the three terms are enough to apply the coherent-sheaf theorem.

@[reducible, inline]

abbrev AlgebraicGeometry.Cohomology.FiniteCohomology.LinearConnectingSystem {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) : Type (u + 1)

Linear connecting maps, compatible with Ext, chosen for every short exact sequence. This is the precise temporary input needed for a global Grothendieck-group factorization.

Equations

• D.LinearConnectingSystem = ((S : CategoryTheory.ShortComplex (AlgebraicGeometry.Coh X)) → (hS : S.ShortExact) → D.LinearConnectingMaps S hS)

The Euler homomorphism on K₀(Coh X)

Coh X is abelian for every a variety over k, so its Grothendieck group is K₀Ab. This file used to build a second one by hand -- generators, a relation subgroup, a quotient, a class map and a bespoke universal property -- none of which was needed. The iso generator it carried was redundant too: K₀Ab.of_iso is a theorem, derived from the short exact sequence X ≅ Y ⟶ 0.

noncomputable def AlgebraicGeometry.Cohomology.FiniteCohomology.grothendieckEulerHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (L : D.LinearConnectingSystem) : CategoryTheory.K₀Ab (Coh X) →+ ℤ

The Euler characteristic as a homomorphism K₀(Coh X) → ℤ.

K₀Ab.liftOf wants additivity and nothing else: map_zero and map_iso follow from of_isZero and of_iso, which are theorems. The old route to this hom went through FreeAbelianGroup.lift, an AddSubgroup.closure_le argument and QuotientAddGroup.lift, all of which are now K₀Ab's.

Equations

• D.grothendieckEulerHom L = CategoryTheory.K₀Ab.liftOf D.eulerCharacteristic ⋯

@[simp]

theorem AlgebraicGeometry.Cohomology.FiniteCohomology.grothendieckEulerHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : FiniteCohomology k X) (L : D.LinearConnectingSystem) (F : Coh X) : (D.grothendieckEulerHom L) (CategoryTheory.K₀Ab.of F) = D.eulerCharacteristic F