Consequences of the long exact cohomology sequence of abelian sheaves

Mathlib's CategoryTheory.Sheaf.H.longSequence is the long exact cohomology sequence

⋯ ⟶ Hⁿ⁰(F₁) ⟶ Hⁿ⁰(F₂) ⟶ Hⁿ⁰(F₃) ⟶ Hⁿ¹(F₁) ⟶ Hⁿ¹(F₂) ⟶ Hⁿ¹(F₃) ⟶ ⋯

of a short exact sequence 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 of abelian sheaves on a site (C, J), as a ComposableArrows in AddCommGrpCat. This file repackages the exactness of the three consecutive pairs as Function.Exact statements about the underlying additive maps, which is the form in which the sequence is used, and records the injectivity and vanishing consequences that follow from it.

Main declarations

• CategoryTheory.Sheaf.H.map_injective, the injectivity of H⁰(F₁) →+ H⁰(F₂), which is where the sequence starts;
• CategoryTheory.Sheaf.H.exact_map_map, H.exact_map_δ and H.exact_δ_map, the exactness of the sequence at Hⁿ(F₂), at Hⁿ⁰(F₃) and at Hⁿ¹(F₁);
• CategoryTheory.Sheaf.H.map_g_surjective, H.subsingleton_X₂, H.subsingleton_X₃ and H.subsingleton_X₁, the vanishing consequences that the sequence is normally used for.

The underlying exactness statements are Mathlib's CategoryTheory.Sheaf.H.longSequence_exact₁', longSequence_exact₂' and longSequence_exact₃'. Sheaf cohomology on the small Zariski site of a scheme is the cohomology of a sheaf of modules; the module-level form of the sequence is in TauCeti.AlgebraicGeometry.Cohomology.LongExactSequence.

theorem CategoryTheory.Sheaf.H.map_injective {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) [Mono f] : Function.Injective ⇑(map f 0)

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

theorem CategoryTheory.Sheaf.H.exact_map_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n : ℕ) : Function.Exact ⇑(map S.f n) ⇑(map S.g n)

The long exact cohomology sequence is exact at Hⁿ(F₂).

theorem CategoryTheory.Sheaf.H.exact_map_δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Function.Exact ⇑(map S.g n₀) ⇑(δ hS n₀ n₁ h)

The long exact cohomology sequence is exact at Hⁿ⁰(F₃).

theorem CategoryTheory.Sheaf.H.exact_δ_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Function.Exact ⇑(δ hS n₀ n₁ h) ⇑(map S.f n₁)

The long exact cohomology sequence is exact at Hⁿ¹(F₁).

theorem CategoryTheory.Sheaf.H.map_g_surjective {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₁ : Subsingleton (S.X₁.H n₁)) : Function.Surjective ⇑(map S.g n₀)

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

theorem CategoryTheory.Sheaf.H.subsingleton_X₂ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n : ℕ) (h₁ : Subsingleton (S.X₁.H n)) (h₃ : Subsingleton (S.X₃.H n)) : Subsingleton (S.X₂.H n)

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

theorem CategoryTheory.Sheaf.H.subsingleton_X₃ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₂ : Subsingleton (S.X₂.H n₀)) (h₁ : Subsingleton (S.X₁.H n₁)) : Subsingleton (S.X₃.H n₀)

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

theorem CategoryTheory.Sheaf.H.subsingleton_X₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {S : ShortComplex (Sheaf J AddCommGrpCat)} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (h₃ : Subsingleton (S.X₃.H n₀)) (h₂ : Subsingleton (S.X₂.H n₁)) : Subsingleton (S.X₁.H n₁)

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