Documentation

Mathlib.CategoryTheory.Sites.ConcreteSheafification

Sheafification #

We construct the sheafification of a presheaf over a site C with values in D whenever D is a concrete category for which the forgetful functor preserves the appropriate (co)limits and reflects isomorphisms.

We generally follow the approach of https://stacks.math.columbia.edu/tag/00W1

A concrete version of the multiequalizer, to be used below.

Equations
Instances For
    theorem CategoryTheory.Meq.congr_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) {Y : C} {f : Y X} {g : Y X} (h : f = g) (hf : (↑S).arrows f) :
    x { Y := Y, f := f, hf := hf } = x { Y := Y, f := g, hf := }
    theorem CategoryTheory.Meq.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (I : S.Relation) :
    (P.map I.r.g₁.op) (x ((S.index P).fstTo I)) = (P.map I.r.g₂.op) (x ((S.index P).sndTo I))

    Refine a term of Meq P T with respect to a refinement S ⟶ T of covers.

    Equations
    • x.refine e = fun (I : S.Arrow) => x { Y := I.Y, f := I.f, hf := },
    Instances For
      @[simp]
      theorem CategoryTheory.Meq.refine_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} {T : J.Cover X} (x : CategoryTheory.Meq P T) (e : S T) (I : S.Arrow) :
      (x.refine e) I = x { Y := I.Y, f := I.f, hf := }

      Pull back a term of Meq P S with respect to a morphism f : Y ⟶ X in C.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Meq.pullback_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (f : Y X) (I : ((J.pullback f).obj S).Arrow) :
        (x.pullback f) I = x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := }
        @[simp]
        theorem CategoryTheory.Meq.pullback_refine {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} {T : J.Cover X} (h : S T) (f : Y X) (x : CategoryTheory.Meq P T) :
        (x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f

        Make a term of Meq P S.

        Equations
        Instances For
          theorem CategoryTheory.GrothendieckTopology.Plus.sep {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X) (x : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))) (y : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))) (h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y) :
          x = y

          P⁺ is always separated.

          theorem CategoryTheory.GrothendieckTopology.Plus.inj_of_sep {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y)x = y) (X : C) :
          Function.Injective ((J.toPlus P).app (Opposite.op X))
          def CategoryTheory.GrothendieckTopology.Plus.meqOfSep {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y)x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) (T : (I : S.Arrow) → J.Cover I.Y) (t : (I : S.Arrow) → CategoryTheory.Meq P (T I)) (ht : ∀ (I : S.Arrow), s I = CategoryTheory.GrothendieckTopology.Plus.mk (t I)) :
          CategoryTheory.Meq P (S.bind T)

          An auxiliary definition to be used in the proof of exists_of_sep below. Given a compatible family of local sections for P⁺, and representatives of said sections, construct a compatible family of local sections of P over the combination of the covers associated to the representatives. The separatedness condition is used to prove compatibility among these local sections of P.

          Equations
          Instances For
            theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y)x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) :
            ∃ (t : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))), CategoryTheory.Meq.mk S t = s

            If P is separated, then P⁺ is a sheaf.

            The sheafification of a presheaf P. NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!

            Equations
            • J.sheafify P = J.plusObj (J.plusObj P)
            Instances For

              The canonical map from P to its sheafification.

              Equations
              Instances For

                The canonical map on sheafifications induced by a morphism.

                Equations
                • J.sheafifyMap η = J.plusMap (J.plusMap η)
                Instances For

                  The sheafification of a presheaf P, as a functor. NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!

                  Equations
                  • J.sheafification D = (J.plusFunctor D).comp (J.plusFunctor D)
                  Instances For

                    The canonical map from P to its sheafification, as a natural transformation. Note: We only show this is a sheaf under additional hypotheses on D.

                    Equations
                    Instances For

                      If P is a sheaf, then P is isomorphic to J.sheafify P.

                      Equations
                      Instances For

                        Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from J.sheafify P to Q.

                        Equations
                        • J.sheafifyLift η hQ = J.plusLift (J.plusLift η hQ) hQ
                        Instances For

                          The sheafification functor, as a functor taking values in Sheaf.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            The sheafification functor is left adjoint to the forgetful functor.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For