The connecting map of coherent cohomology is base-field linear

coherentConnectingMap is Mathlib's Ext connecting homomorphism, an additive map. The base field acts on Hⁱ(X, F) through the endomorphism of F that a scalar induces (coherentHModule), and the connecting map commutes with that action because the scalar endomorphisms of the three terms of a short exact sequence form a morphism of short exact sequences, and extClass_naturality says the extension class is natural in such morphisms.

So the canonical linear realization linearCoherentH carries a linear connecting map, and the covariant Ext long exact sequence is exact as a sequence of k-vector spaces. This is the input the dévissage on projective space needs: Hⁱ(G) → Hⁱ(F) → Hⁱ⁺¹(K) exact and linear, with the outer terms finite-dimensional, forces Hⁱ(F) finite-dimensional. An additive exact sequence would not do: an additive injection into a finite-dimensional space bounds nothing over an infinite field.

EulerCharacteristic/Additivity.lean records the same exactness for an arbitrary FiniteCohomology realization whose connecting maps are supplied as LinearConnectingMaps. Here nothing is supplied: the realization is the canonical one and the connecting map is coherentConnectingMap itself, shown linear.

noncomputable def AlgebraicGeometry.Cohomology.coherentScalarShortComplexHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (S : CategoryTheory.ShortComplex (Coh X)) (r : k) : S ⟶ S

A scalar acts on a short complex of coherent sheaves by a morphism of short complexes. The three components are the scalar endomorphisms, and they commute with the differentials by coherentScalarAction_naturality.

Equations

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

theorem AlgebraicGeometry.Cohomology.coherentConnectingMap_smul {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsLocallyNoetherian X] (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) (i : ℕ) (r : k) (x : ↑((coherentH X i).obj S.X₃)) : (CategoryTheory.ConcreteCategory.hom (coherentConnectingMap S hS i)) (r • x) = r • (CategoryTheory.ConcreteCategory.hom (coherentConnectingMap S hS i)) x

The connecting map commutes with the base-field action.

Both sides are Ext composites: r • x is x postcomposed with the scalar endomorphism, and the connecting map is postcomposition with the extension class. Associativity moves the two postcompositions together and extClass_naturality, applied to the morphism of short exact sequences the scalar defines, swaps their order.

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

The linear connecting map of the canonical realization.

Equations

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

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

Exactness at the middle cohomology group in each degree, for the canonical realization.

theorem AlgebraicGeometry.Cohomology.linearCoherentH_exact₃ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsLocallyNoetherian X] (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) (i : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom ((linearCoherentH k X i).map S.g)) ⇑(CategoryTheory.ConcreteCategory.hom (linearCoherentConnectingMap S hS i))

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

theorem AlgebraicGeometry.Cohomology.linearCoherentH_exact₁ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsLocallyNoetherian X] (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) (i : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (linearCoherentConnectingMap S hS i)) ⇑(CategoryTheory.ConcreteCategory.hom ((linearCoherentH k X (i + 1)).map S.f))

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

instance AlgebraicGeometry.Cohomology.linearCoherentH_additive {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (i : ℕ) : (linearCoherentH k X i).Additive

The canonical realization is additive: forgetting scalars is faithful and additive, and the composite is coherentH, which is additive.