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 #

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

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.

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
    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
          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]

          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.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
            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