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

source
๐Ÿ”ธ coverage
def CategoryTheory.Meq {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} (P : Functor Cแต’แต– D) (S : J.Cover X) :
Type (max 0 (max t u) v)

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

Equations
    Instances For
      source
      ๐Ÿ”ธ coverage
      instance CategoryTheory.Meq.instCoeFunForallToTypeObjOppositeOpY {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} (P : Functor Cแต’แต– D) (S : J.Cover X) :
      CoeFun (Meq P S) fun (x : Meq P S) => (I : S.Arrow) โ†’ ToType (P.obj (Opposite.op I.Y))
      Equations
        source
        theorem CategoryTheory.Meq.congr_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) {Y : C} {f g : Y โŸถ X} (h : f = g) (hf : (โ†‘S).arrows f) :
        โ†‘x { Y := Y, f := f, hf := hf } = โ†‘x { Y := Y, f := g, hf := โ‹ฏ }
        source
        theorem CategoryTheory.Meq.ext {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x y : Meq P S) (h : โˆ€ (I : S.Arrow), โ†‘x I = โ†‘y I) :
        x = y
        source
        theorem CategoryTheory.Meq.ext_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} {x y : Meq P S} :
        x = y โ†” โˆ€ (I : S.Arrow), โ†‘x I = โ†‘y I
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.Meq.condition {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) (I : S.Relation) :
        (ConcreteCategory.hom (P.map I.r.gโ‚.op)) (โ†‘x (S.shape.fst I)) = (ConcreteCategory.hom (P.map I.r.gโ‚‚.op)) (โ†‘x (S.shape.snd I))
        source
        ๐Ÿ”ธ coverage
        def CategoryTheory.Meq.refine {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S T : J.Cover X} (x : Meq P T) (e : S โŸถ T) :
        Meq P S

        Refine a term of Meq P T with respect to a refinement S โŸถ T of covers.

        Equations
          Instances For
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem CategoryTheory.Meq.refine_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} {S T : J.Cover X} (x : Meq P T) (e : S โŸถ T) (I : S.Arrow) :
            โ†‘(x.refine e) I = โ†‘x { Y := I.Y, f := I.f, hf := โ‹ฏ }
            source
            ๐Ÿ”ธ coverage
            def CategoryTheory.Meq.pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {Y X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) (f : Y โŸถ X) :
            Meq P ((J.pullback f).obj S)

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

            Equations
              Instances For
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CategoryTheory.Meq.pullback_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {Y X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) (f : Y โŸถ X) (I : ((J.pullback f).obj S).Arrow) :
                โ†‘(x.pullback f) I = โ†‘x { Y := I.Y, f := CategoryStruct.comp I.f f, hf := โ‹ฏ }
                source
                ๐Ÿ“ coverage
                @[simp]
                theorem CategoryTheory.Meq.pullback_refine {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {Y X : C} {P : Functor Cแต’แต– D} {S T : J.Cover X} (h : S โŸถ T) (f : Y โŸถ X) (x : Meq P T) :
                (x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
                source
                ๐Ÿ”ธ coverage
                def CategoryTheory.Meq.mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} (S : J.Cover X) (x : ToType (P.obj (Opposite.op X))) :
                Meq P S

                Make a term of Meq P S.

                Equations
                  Instances For
                    source
                    ๐Ÿ“ coverage
                    theorem CategoryTheory.Meq.mk_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {X : C} {P : Functor Cแต’แต– D} (S : J.Cover X) (x : ToType (P.obj (Opposite.op X))) (I : S.Arrow) :
                    โ†‘(mk S x) I = (ConcreteCategory.hom (P.map I.f.op)) x
                    source
                    ๐Ÿ”ธ coverage
                    noncomputable def CategoryTheory.Meq.equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] {X : C} (P : Functor Cแต’แต– D) (S : J.Cover X) [Limits.HasMultiequalizer (S.index P)] :
                    ToType (Limits.multiequalizer (S.index P)) โ‰ƒ Meq P S

                    The equivalence between the type associated to multiequalizer (S.index P) and Meq P S.

                    Equations
                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[simp]
                        theorem CategoryTheory.Meq.equiv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} [Limits.HasMultiequalizer (S.index P)] (x : ToType (Limits.multiequalizer (S.index P))) (I : S.Arrow) :
                        โ†‘((equiv P S) x) I = (ConcreteCategory.hom (Limits.Multiequalizer.ฮน (S.index P) I)) x
                        source
                        ๐Ÿ“ coverage
                        theorem CategoryTheory.Meq.equiv_symm_eq_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} [Limits.HasMultiequalizer (S.index P)] (x : Meq P S) (I : S.Arrow) :
                        (ConcreteCategory.hom (Limits.Multiequalizer.ฮน (S.index P) I)) ((equiv P S).symm x) = โ†‘x I
                        source
                        ๐Ÿ”ธ coverage
                        def CategoryTheory.GrothendieckTopology.Plus.mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) :
                        ToType ((J.plusObj P).obj (Opposite.op X))

                        Make a term of (J.plusObj P).obj (op X) from x : Meq P S.

                        Equations
                          Instances For
                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {Y X : C} {P : Functor Cแต’แต– D} {S : J.Cover X} (x : Meq P S) (f : Y โŸถ X) :
                            (ConcreteCategory.hom ((J.plusObj P).map f.op)) (mk x) = mk (x.pullback f)
                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {X : C} {P : Functor Cแต’แต– D} (S : J.Cover X) (x : ToType (P.obj (Opposite.op X))) :
                            (ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x = mk (Meq.mk S x)
                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {X : C} {P : Functor Cแต’แต– D} (S : J.Cover X) (x : Meq P S) (I : S.Arrow) :
                            (ConcreteCategory.hom ((J.toPlus P).app (Opposite.op I.Y))) (โ†‘x I) = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (mk x)
                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {X : C} {P : Functor Cแต’แต– D} (x : ToType (P.obj (Opposite.op X))) :
                            (ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x = mk (Meq.mk โŠค x)
                            source
                            theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] {X : C} {P : Functor Cแต’แต– D} (x : ToType ((J.plusObj P).obj (Opposite.op X))) :
                            โˆƒ (S : J.Cover X) (y : Meq P S), x = mk y
                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] {X : C} {P : Functor Cแต’แต– D} {S T : J.Cover X} (x : Meq P S) (y : Meq P T) :
                            mk x = mk y โ†” โˆƒ (W : J.Cover X) (h1 : W โŸถ S) (h2 : W โŸถ T), x.refine h1 = y.refine h2
                            source
                            theorem CategoryTheory.GrothendieckTopology.Plus.sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] {X : C} (P : Functor Cแต’แต– D) (S : J.Cover X) (x y : ToType ((J.plusObj P).obj (Opposite.op X))) (h : โˆ€ (I : S.Arrow), (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y) :
                            x = y

                            Pโบ is always separated.

                            source
                            ๐Ÿ“ coverage
                            theorem CategoryTheory.GrothendieckTopology.Plus.inj_of_sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] (P : Functor Cแต’แต– D) (hsep : โˆ€ (X : C) (S : J.Cover X) (x y : ToType (P.obj (Opposite.op X))), (โˆ€ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) โ†’ x = y) (X : C) :
                            Function.Injective โ‡‘(ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X)))
                            source
                            ๐Ÿ”ธ coverage
                            def CategoryTheory.GrothendieckTopology.Plus.meqOfSep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] (P : Functor Cแต’แต– D) (hsep : โˆ€ (X : C) (S : J.Cover X) (x y : ToType (P.obj (Opposite.op X))), (โˆ€ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) โ†’ x = y) (X : C) (S : J.Cover X) (s : Meq (J.plusObj P) S) (T : (I : S.Arrow) โ†’ J.Cover I.Y) (t : (I : S.Arrow) โ†’ Meq P (T I)) (ht : โˆ€ (I : S.Arrow), โ†‘s I = mk (t I)) :
                            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
                                source
                                ๐Ÿ“ coverage
                                theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] (P : Functor Cแต’แต– D) (hsep : โˆ€ (X : C) (S : J.Cover X) (x y : ToType (P.obj (Opposite.op X))), (โˆ€ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) โ†’ x = y) (X : C) (S : J.Cover X) (s : Meq (J.plusObj P) S) :
                                โˆƒ (t : ToType ((J.plusObj P).obj (Opposite.op X))), Meq.mk S t = s
                                source
                                ๐Ÿ“ coverage
                                theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (P : Functor Cแต’แต– D) (hsep : โˆ€ (X : C) (S : J.Cover X) (x y : ToType (P.obj (Opposite.op X))), (โˆ€ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) โ†’ x = y) :
                                Presheaf.IsSheaf J (J.plusObj P)

                                If P is separated, then Pโบ is a sheaf.

                                source
                                ๐Ÿ“ coverage
                                theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (P : Functor Cแต’แต– D) :
                                Presheaf.IsSheaf J (J.plusObj (J.plusObj P))

                                Pโบโบ is always a sheaf.

                                source
                                ๐Ÿ”ธ coverage
                                noncomputable def CategoryTheory.GrothendieckTopology.sheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] (P : Functor Cแต’แต– D) :
                                Functor Cแต’แต– D

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

                                Equations
                                  Instances For
                                    source
                                    ๐Ÿ”ธ coverage
                                    noncomputable def CategoryTheory.GrothendieckTopology.toSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] (P : Functor Cแต’แต– D) :
                                    P โŸถ J.sheafify P

                                    The canonical map from P to its sheafification.

                                    Equations
                                      Instances For
                                        source
                                        ๐Ÿ”ธ coverage
                                        noncomputable def CategoryTheory.GrothendieckTopology.sheafifyMap {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) :
                                        J.sheafify P โŸถ J.sheafify Q

                                        The canonical map on sheafifications induced by a morphism.

                                        Equations
                                          Instances For
                                            source
                                            ๐Ÿ“ coverage
                                            @[simp]
                                            theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] (P : Functor Cแต’แต– D) :
                                            J.sheafifyMap (CategoryStruct.id P) = CategoryStruct.id (J.sheafify P)
                                            source
                                            ๐Ÿ“ coverage
                                            @[simp]
                                            theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q R : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (ฮณ : Q โŸถ R) :
                                            J.sheafifyMap (CategoryStruct.comp ฮท ฮณ) = CategoryStruct.comp (J.sheafifyMap ฮท) (J.sheafifyMap ฮณ)
                                            source
                                            ๐Ÿ“ coverage
                                            @[simp]
                                            theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) :
                                            CategoryStruct.comp ฮท (J.toSheafify Q) = CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap ฮท)
                                            source
                                            ๐Ÿ“ coverage
                                            @[simp]
                                            theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) {Z : Functor Cแต’แต– D} (h : J.sheafify Q โŸถ Z) :
                                            CategoryStruct.comp ฮท (CategoryStruct.comp (J.toSheafify Q) h) = CategoryStruct.comp (J.toSheafify P) (CategoryStruct.comp (J.sheafifyMap ฮท) h)
                                            source
                                            ๐Ÿ”ธ coverage
                                            noncomputable def CategoryTheory.GrothendieckTopology.sheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] :
                                            Functor (Functor Cแต’แต– D) (Functor Cแต’แต– D)

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

                                            Equations
                                              Instances For
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem CategoryTheory.GrothendieckTopology.sheafification_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] (P : Functor Cแต’แต– D) :
                                                (J.sheafification D).obj P = J.sheafify P
                                                source
                                                ๐Ÿ“ coverage
                                                @[simp]
                                                theorem CategoryTheory.GrothendieckTopology.sheafification_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) :
                                                (J.sheafification D).map ฮท = J.sheafifyMap ฮท
                                                source
                                                ๐Ÿ”ธ coverage
                                                noncomputable def CategoryTheory.GrothendieckTopology.toSheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] :
                                                Functor.id (Functor Cแต’แต– D) โŸถ J.sheafification D

                                                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
                                                    source
                                                    ๐Ÿ“ coverage
                                                    @[simp]
                                                    theorem CategoryTheory.GrothendieckTopology.toSheafification_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] (P : Functor Cแต’แต– D) :
                                                    (J.toSheafification D).app P = J.toSheafify P
                                                    source
                                                    ๐Ÿ“ coverage
                                                    theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P : Functor Cแต’แต– D} (hP : Presheaf.IsSheaf J P) :
                                                    IsIso (J.toSheafify P)
                                                    source
                                                    ๐Ÿ”ธ coverage
                                                    noncomputable def CategoryTheory.GrothendieckTopology.isoSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P : Functor Cแต’แต– D} (hP : Presheaf.IsSheaf J P) :
                                                    P โ‰… J.sheafify P

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

                                                    Equations
                                                      Instances For
                                                        source
                                                        ๐Ÿ“ coverage
                                                        @[simp]
                                                        theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P : Functor Cแต’แต– D} (hP : Presheaf.IsSheaf J P) :
                                                        (J.isoSheafify hP).hom = J.toSheafify P
                                                        source
                                                        ๐Ÿ”ธ coverage
                                                        noncomputable def CategoryTheory.GrothendieckTopology.sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (hQ : Presheaf.IsSheaf J Q) :
                                                        J.sheafify P โŸถ Q

                                                        Given a sheaf Q and a morphism P โŸถ Q, construct a morphism from J.sheafify P to Q.

                                                        Equations
                                                          Instances For
                                                            source
                                                            ๐Ÿ“ coverage
                                                            @[simp]
                                                            theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (hQ : Presheaf.IsSheaf J Q) :
                                                            CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift ฮท hQ) = ฮท
                                                            source
                                                            ๐Ÿ“ coverage
                                                            @[simp]
                                                            theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (hQ : Presheaf.IsSheaf J Q) {Z : Functor Cแต’แต– D} (h : Q โŸถ Z) :
                                                            CategoryStruct.comp (J.toSheafify P) (CategoryStruct.comp (J.sheafifyLift ฮท hQ) h) = CategoryStruct.comp ฮท h
                                                            source
                                                            ๐Ÿ“ coverage
                                                            theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (hQ : Presheaf.IsSheaf J Q) (ฮณ : J.sheafify P โŸถ Q) :
                                                            CategoryStruct.comp (J.toSheafify P) ฮณ = ฮท โ†’ ฮณ = J.sheafifyLift ฮท hQ
                                                            source
                                                            ๐Ÿ“ coverage
                                                            @[simp]
                                                            theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P : Functor Cแต’แต– D} (hP : Presheaf.IsSheaf J P) :
                                                            (J.isoSheafify hP).inv = J.sheafifyLift (CategoryStruct.id P) hP
                                                            source
                                                            theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q : Functor Cแต’แต– D} (ฮท ฮณ : J.sheafify P โŸถ Q) (hQ : Presheaf.IsSheaf J Q) (h : CategoryStruct.comp (J.toSheafify P) ฮท = CategoryStruct.comp (J.toSheafify P) ฮณ) :
                                                            ฮท = ฮณ
                                                            source
                                                            ๐Ÿ“ coverage
                                                            @[simp]
                                                            theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q R : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (ฮณ : Q โŸถ R) (hR : Presheaf.IsSheaf J R) :
                                                            CategoryStruct.comp (J.sheafifyMap ฮท) (J.sheafifyLift ฮณ hR) = J.sheafifyLift (CategoryStruct.comp ฮท ฮณ) hR
                                                            source
                                                            ๐Ÿ“ coverage
                                                            @[simp]
                                                            theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] {P Q R : Functor Cแต’แต– D} (ฮท : P โŸถ Q) (ฮณ : Q โŸถ R) (hR : Presheaf.IsSheaf J R) {Z : Functor Cแต’แต– D} (h : R โŸถ Z) :
                                                            CategoryStruct.comp (J.sheafifyMap ฮท) (CategoryStruct.comp (J.sheafifyLift ฮณ hR) h) = CategoryStruct.comp (J.sheafifyLift (CategoryStruct.comp ฮท ฮณ) hR) h
                                                            source
                                                            ๐Ÿ“ coverage
                                                            theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (P : Functor Cแต’แต– D) :
                                                            Presheaf.IsSheaf J (J.sheafify P)
                                                            source
                                                            ๐Ÿ”ธ coverage
                                                            noncomputable def CategoryTheory.plusPlusSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] :
                                                            Functor (Functor Cแต’แต– D) (Sheaf J D)

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

                                                            Equations
                                                              Instances For
                                                                source
                                                                ๐Ÿ“ coverage
                                                                @[simp]
                                                                theorem CategoryTheory.plusPlusSheaf_map_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] {Xโœ Yโœ : Functor Cแต’แต– D} (ฮท : Xโœ โŸถ Yโœ) :
                                                                ((plusPlusSheaf J D).map ฮท).val = J.sheafifyMap ฮท
                                                                source
                                                                ๐Ÿ“ coverage
                                                                @[simp]
                                                                theorem CategoryTheory.plusPlusSheaf_obj_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (P : Functor Cแต’แต– D) :
                                                                ((plusPlusSheaf J D).obj P).val = J.sheafify P
                                                                source
                                                                ๐Ÿ“ coverage
                                                                instance CategoryTheory.plusPlusSheaf_preservesZeroMorphisms {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] [Preadditive D] :
                                                                (plusPlusSheaf J D).PreservesZeroMorphisms
                                                                source
                                                                ๐Ÿ”ธ coverage
                                                                noncomputable def CategoryTheory.plusPlusAdjunction {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] :
                                                                plusPlusSheaf J D โŠฃ sheafToPresheaf J D

                                                                The sheafification functor is left adjoint to the forgetful functor.

                                                                Equations
                                                                  Instances For
                                                                    source
                                                                    ๐Ÿ“ coverage
                                                                    @[simp]
                                                                    theorem CategoryTheory.plusPlusAdjunction_counit_app_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (Y : Sheaf J D) :
                                                                    ((plusPlusAdjunction J D).counit.app Y).val = J.sheafifyLift (CategoryStruct.id Y.val) โ‹ฏ
                                                                    source
                                                                    ๐Ÿ“ coverage
                                                                    @[simp]
                                                                    theorem CategoryTheory.plusPlusAdjunction_unit_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] (X : Functor Cแต’แต– D) :
                                                                    (plusPlusAdjunction J D).unit.app X = J.toSheafify X
                                                                    source
                                                                    ๐Ÿ“ coverage
                                                                    instance CategoryTheory.sheafToPresheaf_isRightAdjoint {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] :
                                                                    (sheafToPresheaf J D).IsRightAdjoint
                                                                    source
                                                                    ๐Ÿ“ coverage
                                                                    instance CategoryTheory.presheaf_mono_of_mono {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] {F G : Sheaf J D} (f : F โŸถ G) [Mono f] :
                                                                    Mono f.val
                                                                    source
                                                                    ๐Ÿ“ coverage
                                                                    theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{w', w} D] {FD : D โ†’ D โ†’ Type u_1} {CD : D โ†’ Type t} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [instCC : ConcreteCategory D FD] [โˆ€ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [โˆ€ (P : Functor Cแต’แต– D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [โˆ€ (X : C), Limits.HasColimitsOfShape (J.Cover X)แต’แต– D] [โˆ€ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)แต’แต– (forget D)] [(forget D).ReflectsIsomorphisms] {F G : Sheaf J D} (f : F โŸถ G) :
                                                                    Mono f โ†” Mono f.val