Long exact sequence for sheaf cohomology

We obtain the long exact sequence on sheaf cohomology coming from a short exact sequence of sheaves. We also show it is functorial. In practice, it is often best to work with cohomology as a Type (the long sequence necessarily takes values in the category AddCommGrpCat, so the objects in it are really AddCommGrpCat.of (H F n)). To do this, you can use the lemmas CategoryTheory.Sheaf.H.longSequence_exact₁, CategoryTheory.Sheaf.H.longSequence_exact₂ and CategoryTheory.Sheaf.H.longSequence_exact₃

Main definitions

• CategoryTheory.Sheaf.H.δ: Given a short exact sequence of sheaves S, this is the connecting homomorphism Hⁿ(S.X₃) ⟶ Hⁿ⁺¹(S.X₁).

• CategoryTheory.Sheaf.H.longSequence: Given a short exact sequence of sheaves S, this is the long exact sequence: Hⁿ(S.X₁) ⟶ Hⁿ(S.X₂) ⟶ Hⁿ(S.X₃) ⟶ Hⁿ⁺¹(S.X₁) ⟶ Hⁿ⁺¹(S.X₂) ⟶ Hⁿ⁺¹(S.X₃)

• CategoryTheory.Sheaf.H.longSequenceHom: Given a morphism of short exact sequences of sheaves f : S₁ ⟶ S₂, this is the induced morphism between their long exact sequences. On each object, it is just CategoryTheory.Sheaf.H.map applied to the corresponding morphism in f. E.g. the first morphism is H.map applied to f.τ₁.

• CategoryTheory.Sheaf.H.longSequenceFunctor: This is the functor that sends a short exact sequence to its long exact sequence on cohomology and sends morphisms to longSequenceHom.

noncomputable def CategoryTheory.Sheaf.H.δ {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₁) : S.X₃.H n₀ →+ S.X₁.H n₁

Given a short exact sequence of sheaves S, this is the connecting homomorphism Hⁿ(S.X₃) ⟶ Hⁿ⁺¹(S.X₁).

Equations

• CategoryTheory.Sheaf.H.δ hS n₀ n₁ h = hS.extClass.postcomp ((CategoryTheory.constantSheaf J AddCommGrpCat).obj ↧(ULift.{?u.3, 0} ℤ)) h

theorem CategoryTheory.Sheaf.H.δ_naturality {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) (x : S₁.X₃.H n₀) : (δ h₂ n₀ n₁ h) ((map f.τ₃ n₀) x) = (map f.τ₁ n₁) ((δ h₁ n₀ n₁ h) x)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.H.longSequence {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₁ := by lia) : ComposableArrows AddCommGrpCat 5

This is the long exact sequence: Hⁿ(S.X₁) ⟶ Hⁿ(S.X₂) ⟶ Hⁿ(S.X₃) ⟶ Hⁿ⁺¹(S.X₁) ⟶ Hⁿ⁺¹(S.X₂) ⟶ Hⁿ⁺¹(S.X₃).

Equations

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

theorem CategoryTheory.Sheaf.H.longSequence_exact {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₁) : (longSequence hS n₀ n₁ h).Exact

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.H.longSequenceHom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) (h : n₀ + 1 = n₁ := by lia) : longSequence h₁ n₀ n₁ h ⟶ longSequence h₂ n₀ n₁ h

The induced homomorphism of long exact equences obtained by applying H.map everywhere.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.H.longSequenceHom_id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) {S₁ : ShortComplex (Sheaf J AddCommGrpCat)} (h₁ : S₁.ShortExact) (h : n₀ + 1 = n₁ := by lia) : longSequenceHom n₀ n₁ h₁ h₁ (CategoryStruct.id S₁) h = CategoryStruct.id (longSequence h₁ n₀ n₁ h)

@[simp]

theorem CategoryTheory.Sheaf.H.longSequenceHom_comp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) {S₃ : ShortComplex (Sheaf J AddCommGrpCat)} (h₃ : S₃.ShortExact) (g : S₂ ⟶ S₃) (h : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (longSequenceHom n₀ n₁ h₁ h₂ f h) (longSequenceHom n₀ n₁ h₂ h₃ g h) = longSequenceHom n₀ n₁ h₁ h₃ (CategoryStruct.comp f g) h

@[implicit_reducible]

noncomputable def CategoryTheory.Sheaf.H.longSequenceFunctor {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : Functor (ShortExactSequence (Sheaf J AddCommGrpCat)) (ComposableArrows AddCommGrpCat 5)

The long exact sequence of cohomology is functorial

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.H.longSequenceFunctor_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (S : ShortExactSequence (Sheaf J AddCommGrpCat)) : (longSequenceFunctor n₀ n₁ h).obj S = longSequence ⋯ n₀ n₁ h

@[simp]

theorem CategoryTheory.Sheaf.H.longSequenceFunctor_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {S₁ S₂ : ShortExactSequence (Sheaf J AddCommGrpCat)} (f : S₁ ⟶ S₂) : (longSequenceFunctor n₀ n₁ h).map f = longSequenceHom n₀ n₁ ⋯ ⋯ f.hom h

theorem CategoryTheory.Sheaf.H.longSequence_exact₁' {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₁ := by lia) : { X₁ := ↧(S.X₃.H n₀), X₂ := ↧(S.X₁.H n₁), X₃ := ↧(S.X₂.H n₁), f := AddCommGrpCat.ofHom (δ hS n₀ n₁ h), g := AddCommGrpCat.ofHom (map S.f n₁), zero := ⋯ }.Exact

theorem CategoryTheory.Sheaf.H.longSequence_exact₂' {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 : ℕ) : { X₁ := ↧(S.X₁.H n), X₂ := ↧(S.X₂.H n), X₃ := ↧(S.X₃.H n), f := AddCommGrpCat.ofHom (map S.f n), g := AddCommGrpCat.ofHom (map S.g n), zero := ⋯ }.Exact

theorem CategoryTheory.Sheaf.H.longSequence_exact₃' {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₁ := by lia) : { X₁ := ↧(S.X₂.H n₀), X₂ := ↧(S.X₃.H n₀), X₃ := ↧(S.X₁.H n₁), f := AddCommGrpCat.ofHom (map S.g n₀), g := AddCommGrpCat.ofHom (δ hS n₀ n₁ h), zero := ⋯ }.Exact

theorem CategoryTheory.Sheaf.H.longSequence_exact₁ {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₁ : ℕ} (x₁ : S.X₁.H n₁) (hx₁ : (map S.f n₁) x₁ = 0) {n₀ : ℕ} (h : n₀ + 1 = n₁) : ∃ (x₃ : S.X₃.H n₀), (δ hS n₀ n₁ h) x₃ = x₁

theorem CategoryTheory.Sheaf.H.longSequence_exact₂ {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 : ℕ} (x₂ : S.X₂.H n) (hx₂ : (map S.g n) x₂ = 0) : ∃ (x₁ : S.X₁.H n), (map S.f n) x₁ = x₂

theorem CategoryTheory.Sheaf.H.longSequence_exact₃ {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₀ : ℕ} (x₃ : S.X₃.H n₀) {n₁ : ℕ} (h : n₀ + 1 = n₁) (hx₃ : (δ hS n₀ n₁ h) x₃ = 0) : ∃ (x₂ : S.X₂.H n₀), (map S.g n₀) x₂ = x₃

theorem CategoryTheory.Sheaf.H.longSequence_equiv₀_exact₃ {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) {T : C} (hT : Limits.IsTerminal T) (x₃ : ↑(S.X₃.obj.obj (Opposite.op T))) (hx₃ : (δ hS 0 1 ⋯) ((equiv₀ S.X₃ hT).symm x₃) = 0) : ∃ (x₂ : ↑(S.X₂.obj.obj (Opposite.op T))), (ConcreteCategory.hom (S.g.hom.app (Opposite.op T))) x₂ = x₃