Documentation

Mathlib.CategoryTheory.Sites.MayerVietorisSquare

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

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

Instances For

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

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 := ⋯ }

Instances For

@[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_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 ⋯

Instances For

@[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

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) :

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

Instances For

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

Instances For

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⟩

Instances For

@[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

noncomputable def CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrp)

The short complex of abelian sheaves ℤ[S.X₁] ⟶ ℤ[S.X₂] ⊞ ℤ[S.X₃] ⟶ ℤ[S.X₄] where the left map is a difference and the right map a sum.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.X₁ = (CategoryTheory.presheafToSheaf J AddCommGrp).obj ((CategoryTheory.yoneda.obj S.X₁).comp AddCommGrp.free)

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.X₂ = ((CategoryTheory.presheafToSheaf J AddCommGrp).obj ((CategoryTheory.yoneda.obj S.X₂).comp AddCommGrp.free) ⊞ (CategoryTheory.presheafToSheaf J AddCommGrp).obj ((CategoryTheory.yoneda.obj S.X₃).comp AddCommGrp.free))

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.f = CategoryTheory.Limits.biprod.lift ((CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₁₂) AddCommGrp.free)) (-(CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₁₃) AddCommGrp.free))

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.X₃ = (CategoryTheory.presheafToSheaf J AddCommGrp).obj ((CategoryTheory.yoneda.obj S.X₄).comp AddCommGrp.free)

@[simp]

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.g = CategoryTheory.Limits.biprod.desc ((CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₂₄) AddCommGrp.free)) ((CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₃₄) AddCommGrp.free))

instance CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpFShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

CategoryTheory.Mono S.shortComplex.f

Equations

⋯ = ⋯

instance CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpGShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

CategoryTheory.Epi S.shortComplex.g

Equations

⋯ = ⋯

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.Exact

theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) :

S.shortComplex.ShortExact