The Mayer-Vietoris exact sequence in sheaf cohomology

Let C be a category equipped with a Grothendieck topology J. Let S : J.MayerVietorisSquare be a Mayer-Vietoris square for J. Let F be an abelian sheaf on (C, J).

In this file, we obtain a long exact Mayer-Vietoris sequence:

... ⟶ H^n(S.X₄, F) ⟶ H^n(S.X₂, F) ⊞ H^n(S.X₃, F) ⟶ H^n(S.X₁, F) ⟶ H^{n + 1}(S.X₄, F) ⟶ ...

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n : ℕ) : F.H' n S.X₄ ⟶ F.H' n S.X₂ ⊞ F.H' n S.X₃

The sum of two restriction maps in sheaf cohomology.

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) {n : ℕ} (y : ↑(F.H' n S.X₄)) : (ConcreteCategory.hom (S.toBiprod F n)) y = (ConcreteCategory.hom (((F.cohomologyPresheaf n).obj (Opposite.op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (Opposite.op S.X₃))).inv) ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y, (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y)

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n : ℕ) : F.H' n S.X₂ ⊞ F.H' n S.X₃ ⟶ F.H' n S.X₁

The difference of two restriction maps in sheaf cohomology.

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n : ℕ) : CategoryStruct.comp (S.toBiprod F n) (S.fromBiprod F n) = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n : ℕ) {Z : AddCommGrpCat} (h : F.H' n S.X₁ ⟶ Z) : CategoryStruct.comp (S.toBiprod F n) (CategoryStruct.comp (S.fromBiprod F n) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) {n : ℕ} (y₁ : ↑(F.H' n S.X₂)) (y₂ : ↑(F.H' n S.X₃)) : (ConcreteCategory.hom (S.fromBiprod F n)) ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (y₁, y₂)) = (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₂.op)) y₁ - (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₃.op)) y₂

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) {n : ℕ} (x : ↑(F.H' n S.X₄)) : Abelian.Ext.biprodAddEquiv.symm ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom) ((ConcreteCategory.hom (S.toBiprod F n)) x)) = (Abelian.Ext.mk₀ S.shortComplex.g).comp x ⋯

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) {n : ℕ} (x : ↑(F.H' n S.X₂ ⊞ F.H' n S.X₃)) : (Abelian.Ext.mk₀ S.shortComplex.f).comp (Abelian.Ext.biprodAddEquiv.symm ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom) x)) ⋯ = (ConcreteCategory.hom (S.fromBiprod F n)) x

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : F.H' n₀ S.X₁ ⟶ F.H' n₁ S.X₄

The connecting homomorphism of the Mayer-Vietoris long exact sequence in sheaf cohomology.

@[reducible, inline]

noncomputable abbrev CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : ComposableArrows AddCommGrpCat 5

The Mayer-Vietoris long exact sequence of an abelian sheaf F : Sheaf J AddCommGrpCat for a Mayer-Vietoris square S : J.MayerVietorisSquare.

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequenceIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : S.sequence F n₀ n₁ h ≅ Abelian.Ext.contravariantSequence ⋯ F n₀ n₁ ⋯

Comparison isomorphism from the Mayer-Vietoris sequence and the contravariant sequence of Ext-groups.

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : (S.sequence F n₀ n₁ h).Exact

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : CategoryStruct.comp (S.δ F n₀ n₁ h) (S.toBiprod F n₁) = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {Z : AddCommGrpCat} (h✝ : F.H' n₁ S.X₂ ⊞ F.H' n₁ S.X₃ ⟶ Z) : CategoryStruct.comp (S.δ F n₀ n₁ h) (CategoryStruct.comp (S.toBiprod F n₁) h✝) = CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : CategoryStruct.comp (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) = 0

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasWeakSheafify J (Type v)] [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) {Z : AddCommGrpCat} (h✝ : F.H' n₁ S.X₄ ⟶ Z) : CategoryStruct.comp (S.fromBiprod F n₀) (CategoryStruct.comp (S.δ F n₀ n₁ h) h✝) = CategoryStruct.comp 0 h✝