The long exact cohomology sequence of a short exact sequence of sheaves of modules

TauCeti/AlgebraicGeometry/Cohomology/Basic.lean defines the cohomology Hⁿ(X, M) of a sheaf of modules on a scheme. This file adds the long exact sequence attached to a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of 𝒪_X-modules,

0 ⟶ H⁰(X, M₁) ⟶ H⁰(X, M₂) ⟶ H⁰(X, M₃) ⟶ H¹(X, M₁) ⟶ H¹(X, M₂) ⟶ ⋯

together with its consequences for global sections. Where TauCeti/AlgebraicGeometry/Cohomology/MayerVietoris.lean varies the open subset, this file varies the coefficients.

Main declarations

• Scheme.Modules.cohomologyMap, a morphism of sheaves of modules as a map on cohomology;
• Scheme.Modules.cohomologyδ, the connecting map Hⁿ⁰(X, M₃) ⟶ Hⁿ¹(X, M₁), together with the three exactness statements Scheme.Modules.exact_cohomologyMap_cohomologyMap, Scheme.Modules.exact_cohomologyMap_cohomologyδ and Scheme.Modules.exact_cohomologyδ_cohomologyMap;
• Scheme.Modules.cohomologyMap_injective, the injectivity in degree zero at which the sequence starts, and Scheme.Modules.cohomologyMap_surjective, the surjectivity it gives when the next cohomology group of M₁ vanishes;
• Scheme.Modules.subsingleton_cohomology_X₂, Scheme.Modules.subsingleton_cohomology_X₃ and Scheme.Modules.subsingleton_cohomology_X₁, the vanishing consequences;
• Scheme.Modules.finiteDimensional_cohomology_X₂: in a short exact sequence, Hⁱ(X, M₂) is finite-dimensional when Hⁱ(X, M₁) and Hⁱ(X, M₃) are, and Scheme.Modules.finiteDimensional_cohomology_X₁: Hⁱ⁺¹(X, M₁) is finite-dimensional when Hⁱ(X, M₃) and Hⁱ⁺¹(X, M₂) are;
• Scheme.Modules.exact_sections and Scheme.Modules.sections_injective: global sections are left exact, and Scheme.Modules.sections_surjective: they are exact on the right as soon as H¹(X, M₁) vanishes. This last statement is the form in which the sequence is normally used;
• Scheme.Modules.cohomologyδ_naturality, the naturality of the connecting map in the short exact sequence, and the linearity it gives: Scheme.Modules.cohomologyδLinear over the ring of global functions and Scheme.Modules.cohomologyδBaseLinear over the base ring of a scheme over a commutative ring. The maps induced by morphisms of sheaves are already linear, so this makes the whole long exact sequence one of modules; a dimension count in it needs that.

Additivity of the Euler characteristic, and with it Riemann-Roch, rest on this sequence. The sequence itself is Mathlib's CategoryTheory.Sheaf.H.longSequence, repackaged in TauCeti.CategoryTheory.Sites.SheafCohomology.LongExactSequence; exactness of forgetting the module structures is in TauCeti.AlgebraicGeometry.Modules.Sheaf, and the comparison of degree-zero cohomology with global sections is Scheme.Modules.cohomologyZeroEquiv.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyMap {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) (n : ℕ) : Cohomology M n →+ Cohomology N n

A morphism of sheaves of modules on a scheme, as a map on degree-n cohomology.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyMap f n = CategoryTheory.Sheaf.H.map ((TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf X).map f) n

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor_map {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) (n : ℕ) : (cohomologyFunctor X n).map f = AddCommGrpCat.ofHom (cohomologyMap f n)

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv_cohomologyMap {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) (x : Cohomology M 0) : (cohomologyZeroEquiv N) ((cohomologyMap f 0) x) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app f ⊤)) ((cohomologyZeroEquiv M) x)

Under the identification of degree-zero cohomology with global sections, the map induced on cohomology by a morphism of sheaves of modules is the map induced on global sections.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδ {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Cohomology S.X₃ n₀ →+ Cohomology S.X₁ n₁

The connecting map Hⁿ⁰(X, M₃) →+ Hⁿ¹(X, M₁) of the long exact cohomology sequence of a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of sheaves of modules.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδ hS n₀ n₁ h = CategoryTheory.Sheaf.H.δ ⋯ n₀ n₁ h

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.exact_cohomologyMap_cohomologyMap {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n : ℕ) : Function.Exact ⇑(cohomologyMap S.f n) ⇑(cohomologyMap S.g n)

The long exact cohomology sequence is exact at Hⁿ(X, M₂).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.exact_cohomologyMap_cohomologyδ {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Function.Exact ⇑(cohomologyMap S.g n₀) ⇑(cohomologyδ hS n₀ n₁ h)

The long exact cohomology sequence is exact at Hⁿ⁰(X, M₃).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.exact_cohomologyδ_cohomologyMap {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Function.Exact ⇑(cohomologyδ hS n₀ n₁ h) ⇑(cohomologyMap S.f n₁)

The long exact cohomology sequence is exact at Hⁿ¹(X, M₁).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyMap_injective {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) [CategoryTheory.Mono f] : Function.Injective ⇑(cohomologyMap f 0)

A monomorphism of sheaves of modules is injective on cohomology in degree zero.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyMap_surjective {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₁ : Subsingleton (Cohomology S.X₁ n₁)) : Function.Surjective ⇑(cohomologyMap S.g n₀)

If Hⁿ¹(X, M₁) vanishes, then Hⁿ⁰(X, M₂) →+ Hⁿ⁰(X, M₃) is surjective.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_X₂ {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n : ℕ) (h₁ : Subsingleton (Cohomology S.X₁ n)) (h₃ : Subsingleton (Cohomology S.X₃ n)) : Subsingleton (Cohomology S.X₂ n)

If Hⁿ(X, M₁) and Hⁿ(X, M₃) vanish, then so does Hⁿ(X, M₂).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_X₃ {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₂ : Subsingleton (Cohomology S.X₂ n₀)) (h₁ : Subsingleton (Cohomology S.X₁ n₁)) : Subsingleton (Cohomology S.X₃ n₀)

If Hⁿ⁰(X, M₂) and Hⁿ¹(X, M₁) vanish, then so does Hⁿ⁰(X, M₃).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_X₁ {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₃ : Subsingleton (Cohomology S.X₃ n₀)) (h₂ : Subsingleton (Cohomology S.X₂ n₁)) : Subsingleton (Cohomology S.X₁ n₁)

If Hⁿ⁰(X, M₃) and Hⁿ¹(X, M₂) vanish, then so does Hⁿ¹(X, M₁).

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.exact_sections {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app S.f ⊤)) ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app S.g ⊤))

Global sections are left exact: the sections of M₁ are exactly the sections of M₂ that die in M₃.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.sections_injective {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) [CategoryTheory.Mono f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app f ⊤))

Global sections are left exact: a monomorphism of sheaves of modules is injective on global sections.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.sections_surjective {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (h₁ : Subsingleton (Cohomology S.X₁ 1)) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app S.g ⊤))

If H¹(X, M₁) vanishes, then every global section of M₃ lifts to a global section of M₂. This is the form in which the long exact sequence is normally used.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.cohomologyMap_globalSectionsSmul_apply {X : Scheme} (M : X.Modules) (i : ℕ) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) : (TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyMap (M.globalSectionsSmul r) i) x = r • x

Multiplication by a global function on cohomology is the map induced by multiplication by that function on the coefficient sheaf.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδ_naturality {X : AlgebraicGeometry.Scheme} {S₁ S₂ : CategoryTheory.ShortComplex X.Modules} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (x : Cohomology S₁.X₃ n₀) : (cohomologyMap φ.τ₁ n₁) ((cohomologyδ h₁ n₀ n₁ h) x) = (cohomologyδ h₂ n₀ n₁ h) ((cohomologyMap φ.τ₃ n₀) x)

The connecting map is natural in the short exact sequence: a morphism φ : S₁ ⟶ S₂ of short exact sequences of sheaves of modules makes the square formed by the two connecting maps and the maps induced by φ.τ₃ and φ.τ₁ commute.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδLinear {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Cohomology S.X₃ n₀ →ₗ[↑(X.presheaf.obj (Opposite.op ⊤))] Cohomology S.X₁ n₁

The connecting map of the long exact cohomology sequence is linear over the ring of global functions.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδLinear hS n₀ n₁ h = { toFun := ⇑(TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδ hS n₀ n₁ h), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδLinear_apply {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (x : Cohomology S.X₃ n₀) : (cohomologyδLinear hS n₀ n₁ h) x = (cohomologyδ hS n₀ n₁ h) x

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδBaseLinear (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Cohomology S.X₃ n₀ →ₗ[R] Cohomology S.X₁ n₁

For a scheme over a commutative ring, the connecting map of the long exact cohomology sequence is linear over the base ring.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδBaseLinear R X hS n₀ n₁ h = { toFun := ⇑(TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδ hS n₀ n₁ h), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyδBaseLinear_apply (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (x : Cohomology S.X₃ n₀) : (cohomologyδBaseLinear R X hS n₀ n₁ h) x = (cohomologyδ hS n₀ n₁ h) x

theorem AlgebraicGeometry.Scheme.Modules.finiteDimensional_cohomology_X₂ (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (i : ℕ) [FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₁ i)] [FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₃ i)] : FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₂ i)

Hⁱ(X, M₂) is squeezed by the exact sequence between Hⁱ(X, M₁) and Hⁱ(X, M₃), so it is finite-dimensional as soon as those two are.

theorem AlgebraicGeometry.Scheme.Modules.finiteDimensional_cohomology_X₁ (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] {S : CategoryTheory.ShortComplex X.Modules} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) [FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₃ n₀)] [FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₂ n₁)] : FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology S.X₁ n₁)

Hⁿ¹(X, M₁) is squeezed by the exact sequence between Hⁿ⁰(X, M₃) and Hⁿ¹(X, M₂), where n₀ + 1 = n₁, so it is finite-dimensional as soon as those two are.