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 #
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
the square becomes a pushout square in the category of sheaves of types
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
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
Instances For
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
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
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⟩