Mayer-Vietoris squares

The purpose of this file is to allow the formalization of long exact Mayer-Vietoris sequences in sheaf cohomology. If X₄ is an open subset of a topological space that is covered by two open subsets X₂ and X₃, it is known that there is a long exact sequence ... ⟶ H^q(X₄) ⟶ H^q(X₂) ⊞ H^q(X₃) ⟶ H^q(X₁) ⟶ H^{q+1}(X₄) ⟶ ... where X₁ is the intersection of X₂ and X₃, and H^q are the cohomology groups with values in an abelian sheaf.

In this file, we introduce a structure GrothendieckTopology.MayerVietorisSquare which extends Squace C, and asserts properties which shall imply the existence of long exact Mayer-Vietoris sequences in sheaf cohomology (TODO). We require that the map X₁ ⟶ X₃ is a monomorphism and that the square in C becomes a pushout square in the category of sheaves after the application of the functor yoneda ⋙ presheafToSheaf J _. Note that in the standard case of a covering by two open subsets, all the morphisms in the square would be monomorphisms, but this dissymetry allows the example of Nisnevich distinguished squares in the case of the Nisnevich topology on schemes (in which case f₂₄ : X₂ ⟶ X₄ shall be an open immersion and f₃₄ : X₃ ⟶ X₄ an étale map that is an isomorphism over the closed (reduced) subscheme X₄ - X₂, and X₁ shall be the pullback of f₂₄ and f₃₄.).

TODO

• show that when "evaluating" a sheaf on a Mayer-Vietoris square, one obtains a pullback square
• provide constructors for MayerVietorisSquare

References

• https://stacks.math.columbia.edu/tag/08GL

structure CategoryTheory.GrothendieckTopology.MayerVietorisSquare {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J (Type v)] extends CategoryTheory.Square : Type (max u v)

A Mayer-Vietoris square in a category C equipped with a Grothendieck topology consists of a commutative square f₁₂ ≫ f₂₄ = f₁₃ ≫ f₃₄ in C such that f₁₃ is a monomorphism and that the square becomes a pushout square in the category of sheaves of sets.

• X₁ : C
• X₂ : C
• X₃ : C
• X₄ : C
• f₁₂ : self.X₁ ⟶ self.X₂
• f₁₃ : self.X₁ ⟶ self.X₃
• f₂₄ : self.X₂ ⟶ self.X₄
• f₃₄ : self.X₃ ⟶ self.X₄
• fac : CategoryTheory.CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryTheory.CategoryStruct.comp self.f₁₃ self.f₃₄
• mono_f₁₃ : CategoryTheory.Mono self.f₁₃
• isPushout : (self.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout

  the square becomes a pushout square in the category of sheaves of types

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (self : J.MayerVietorisSquare) : CategoryTheory.Mono self.f₁₃

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (self : J.MayerVietorisSquare) : (self.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout

the square becomes a pushout square in the category of sheaves of types