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 Square 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₃₄.).

Given a Mayer-Vietoris square S and a presheaf P on C, we introduce a sheaf condition S.SheafCondition P and show that it is indeed satisfied by sheaves.

References

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

@[simp]

theorem CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (F : CategoryTheory.Sheaf J (Type v)) (sq : CategoryTheory.Square C) : (sq.op.map ((CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v))).op.comp (CategoryTheory.yoneda.obj F))).IsPullback ↔ (sq.op.map F.val).IsPullback

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk'_toSquare {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₁₃] (H : ∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.val).IsPullback) : (CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' sq H).toSquare = sq

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₁₃] (H : ∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.val).IsPullback) : J.MayerVietorisSquare

Constructor for Mayer-Vietoris squares taking as an input a square sq such that sq.f₂₄ is a mono and that for every sheaf of types F, the square sq.op.map F.val is a pullback square.

Equations

• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' sq H = { toSquare := sq, mono_f₁₃ := ⋯, isPushout := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback_toSquare {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₂₄] [CategoryTheory.Mono sq.f₃₄] (h₁ : sq.IsPullback) (h₂ : CategoryTheory.Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄) : (CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback sq h₁ h₂).toSquare = sq

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₂₄] [CategoryTheory.Mono sq.f₃₄] (h₁ : sq.IsPullback) (h₂ : CategoryTheory.Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄) : J.MayerVietorisSquare

Constructor for Mayer-Vietoris squares taking as an input a pullback square sq such that sq.f₂₄ and sq.f₃₄ are two monomorphisms which form a covering of S.X₄.

Equations

• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback sq h₁ h₂ = CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' sq ⋯

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) [CategoryTheory.HasWeakSheafify J AddCommGrp] : (S.map (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringRight Cᵒᵖ (Type v) AddCommGrp).obj AddCommGrp.free).comp (CategoryTheory.presheafToSheaf J AddCommGrp)))).IsPushout

def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) {A : Type u'} [CategoryTheory.Category.{v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A) : Prop

The condition that a Mayer-Vietoris square becomes a pullback square when we evaluate a presheaf on it. -

Equations

• S.SheafCondition P = (S.op.map P).IsPullback

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_comp_coyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) {A : Type u'} [CategoryTheory.Category.{v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A) : S.SheafCondition P ↔ ∀ (X : Aᵒᵖ), S.SheafCondition (P.comp (CategoryTheory.coyoneda.obj X))

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toPullbackObj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) (P : CategoryTheory.Functor Cᵒᵖ (Type v')) : P.obj (Opposite.op S.X₄) → CategoryTheory.Limits.Types.PullbackObj (P.map S.f₁₂.op) (P.map S.f₁₃.op)

Given a Mayer-Vietoris square S and a presheaf of types, this is the map from P.obj (op S.X₄) to the explicit fibre product of P.map S.f₁₂.op and P.map S.f₁₃.op.

Equations

• S.toPullbackObj P = (S.op.map P).pullbackCone.toPullbackObj

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) (P : CategoryTheory.Functor Cᵒᵖ (Type v')) : S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare} {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) : Function.Bijective (S.toPullbackObj P)

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare} {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) {x : P.obj (Opposite.op S.X₄)} {y : P.obj (Opposite.op S.X₄)} (h₁ : P.map S.f₂₄.op x = P.map S.f₂₄.op y) (h₂ : P.map S.f₃₄.op x = P.map S.f₃₄.op y) : x = y

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.glue {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare} {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) (u : P.obj (Opposite.op S.X₂)) (v : P.obj (Opposite.op S.X₃)) (huv : P.map S.f₁₂.op u = P.map S.f₁₃.op v) : P.obj (Opposite.op S.X₄)

If S is a Mayer-Vietoris square, and P is a presheaf which satisfies the sheaf condition with respect to S, then elements of P over S.X₂ and S.X₃ can be glued if the coincide over S.X₁.

Equations

• h.glue u v huv = (CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj (CategoryTheory.Square.IsPullback.isLimit h)).symm ⟨(u, v), huv⟩

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₂₄_op_glue {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare} {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) (u : P.obj (Opposite.op S.X₂)) (v : P.obj (Opposite.op S.X₃)) (huv : P.map S.f₁₂.op u = P.map S.f₁₃.op v) : P.map S.f₂₄.op (h.glue u v huv) = u

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₃₄_op_glue {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare} {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) (u : P.obj (Opposite.op S.X₂)) (v : P.obj (Opposite.op S.X₃)) (huv : P.map S.f₁₂.op u = P.map S.f₁₃.op v) : P.map S.f₃₄.op (h.glue u v huv) = v

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_of_sheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) {A : Type u'} [CategoryTheory.Category.{v, u'} A] (F : CategoryTheory.Sheaf J A) : S.SheafCondition F.val