# 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

def CategoryTheory.Meq {C : Type u} {D : Type w} [] {X : C} (P : ) (S : J.Cover X) :
Type (max 0 u v)

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

Equations
• = { x : (I : S.Arrow) → .obj (P.obj (Opposite.op I.Y)) // ∀ (I : S.Relation), (P.map I.r.g₁.op) (x I.fst) = (P.map I.r.g₂.op) (x I.snd) }
Instances For
instance CategoryTheory.Meq.instCoeFunForallObjForgetOppositeOpY {C : Type u} {D : Type w} [] {X : C} (P : ) (S : J.Cover X) :
CoeFun () fun (x : ) => (I : S.Arrow) → .obj (P.obj (Opposite.op I.Y))
Equations
• = { coe := fun (x : ) => x }
theorem CategoryTheory.Meq.congr_apply {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} (x : ) {Y : C} {f : Y X} {g : Y X} (h : f = g) (hf : S.sieve.arrows f) :
x { Y := Y, f := f, hf := hf } = x { Y := Y, f := g, hf := }
theorem CategoryTheory.Meq.ext {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} (x : ) (y : ) (h : ∀ (I : S.Arrow), x I = y I) :
x = y
theorem CategoryTheory.Meq.condition {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} (x : ) (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))
def CategoryTheory.Meq.refine {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} {T : J.Cover X} (x : ) (e : S T) :

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} {D : Type w} [] {X : C} {P : } {S : J.Cover X} {T : J.Cover X} (x : ) (e : S T) (I : S.Arrow) :
(x.refine e) I = x { Y := I.Y, f := I.f, hf := }
def CategoryTheory.Meq.pullback {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } {S : J.Cover X} (x : ) (f : Y X) :
CategoryTheory.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
• x.pullback f = fun (I : ((J.pullback f).obj S).Arrow) => x { Y := I.Y, f := , hf := },
Instances For
@[simp]
theorem CategoryTheory.Meq.pullback_apply {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } {S : J.Cover X} (x : ) (f : Y X) (I : ((J.pullback f).obj S).Arrow) :
(x.pullback f) I = x { Y := I.Y, f := , hf := }
@[simp]
theorem CategoryTheory.Meq.pullback_refine {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } {S : J.Cover X} {T : J.Cover X} (h : S T) (f : Y X) (x : ) :
(x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
def CategoryTheory.Meq.mk {C : Type u} {D : Type w} [] {X : C} {P : } (S : J.Cover X) (x : .obj (P.obj ())) :

Make a term of Meq P S.

Equations
• = fun (I : S.Arrow) => (P.map I.f.op) x,
Instances For
theorem CategoryTheory.Meq.mk_apply {C : Type u} {D : Type w} [] {X : C} {P : } (S : J.Cover X) (x : .obj (P.obj ())) (I : S.Arrow) :
() I = (P.map I.f.op) x
noncomputable def CategoryTheory.Meq.equiv {C : Type u} {D : Type w} [] {X : C} (P : ) (S : J.Cover X) [CategoryTheory.Limits.HasMultiequalizer (S.index P)] :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Meq.equiv_apply {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : .obj (CategoryTheory.Limits.multiequalizer (S.index P))) (I : S.Arrow) :
(() x) I = (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I) x
theorem CategoryTheory.Meq.equiv_symm_eq_apply {C : Type u} {D : Type w} [] {X : C} {P : } {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : ) (I : S.Arrow) :
(CategoryTheory.Limits.Multiequalizer.ι (S.index P) I) (().symm x) = x I
def CategoryTheory.GrothendieckTopology.Plus.mk {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : } {S : J.Cover X} (x : ) :
.obj ((J.plusObj P).obj ())

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

Equations
Instances For
theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {Y : C} {X : C} {P : } {S : J.Cover X} (x : ) (f : Y X) :
((J.plusObj P).map f.op) = CategoryTheory.GrothendieckTopology.Plus.mk (x.pullback f)
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : } (S : J.Cover X) (x : .obj (P.obj ())) :
((J.toPlus P).app ()) x =
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : } (S : J.Cover X) (x : ) (I : S.Arrow) :
((J.toPlus P).app (Opposite.op I.Y)) (x I) = ((J.plusObj P).map I.f.op)
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : } (x : .obj (P.obj ())) :
((J.toPlus P).app ()) x =
theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] {X : C} {P : } (x : .obj ((J.plusObj P).obj ())) :
∃ (S : J.Cover X) (y : ),
theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] {X : C} {P : } {S : J.Cover X} {T : J.Cover X} (x : ) (y : ) :
∃ (W : J.Cover X) (h1 : W S) (h2 : W T), x.refine h1 = y.refine h2
theorem CategoryTheory.GrothendieckTopology.Plus.sep {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] {X : C} (P : ) (S : J.Cover X) (x : .obj ((J.plusObj P).obj ())) (y : .obj ((J.plusObj P).obj ())) (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} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] (P : ) (hsep : ∀ (X : C) (S : J.Cover X) (x y : .obj (P.obj ())), (∀ (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 ())
def CategoryTheory.GrothendieckTopology.Plus.meqOfSep {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] (P : ) (hsep : ∀ (X : C) (S : J.Cover X) (x y : .obj (P.obj ())), (∀ (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), ) :
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
• = fun (I : (S.bind T).Arrow) => (t I.fromMiddle) I.toMiddle,
Instances For
theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] (P : ) (hsep : ∀ (X : C) (S : J.Cover X) (x y : .obj (P.obj ())), (∀ (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 : .obj ((J.plusObj P).obj ())),
theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] [.ReflectsIsomorphisms] (P : ) (hsep : ∀ (X : C) (S : J.Cover X) (x y : .obj (P.obj ())), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y)x = y) :

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

theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus {C : Type u} {D : Type w} [] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [(X : C) → ] [.ReflectsIsomorphisms] (P : ) :
CategoryTheory.Presheaf.IsSheaf J (J.plusObj (J.plusObj P))

P⁺⁺ is always a sheaf.

noncomputable def CategoryTheory.GrothendieckTopology.sheafify {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : ) :

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
noncomputable def CategoryTheory.GrothendieckTopology.toSheafify {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : ) :
P J.sheafify P

The canonical map from P to its sheafification.

Equations
Instances For
noncomputable def CategoryTheory.GrothendieckTopology.sheafifyMap {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) :
J.sheafify P J.sheafify Q

The canonical map on sheafifications induced by a morphism.

Equations
• J.sheafifyMap η = J.plusMap (J.plusMap η)
Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : ) :
J.sheafifyMap = CategoryTheory.CategoryStruct.id (J.sheafify P)
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } {R : } (η : P Q) (γ : Q R) :
J.sheafifyMap = CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyMap γ)
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) {Z : } (h : J.sheafify Q Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) :
CategoryTheory.CategoryStruct.comp η (J.toSheafify Q) = CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap η)
noncomputable def CategoryTheory.GrothendieckTopology.sheafification {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ 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
• J.sheafification D = (J.plusFunctor D).comp (J.plusFunctor D)
Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafification_obj {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : ) :
(J.sheafification D).obj P = J.sheafify P
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafification_map {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) :
(J.sheafification D).map η = J.sheafifyMap η
noncomputable def CategoryTheory.GrothendieckTopology.toSheafification {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ 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
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafification_app {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : ) :
(J.toSheafification D).app P = J.toSheafify P
theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } (hP : ) :
CategoryTheory.IsIso (J.toSheafify P)
noncomputable def CategoryTheory.GrothendieckTopology.isoSheafify {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } (hP : ) :
P J.sheafify P

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

Equations
Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } (hP : ) :
(J.isoSheafify hP).hom = J.toSheafify P
noncomputable def CategoryTheory.GrothendieckTopology.sheafifyLift {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) (hQ : ) :
J.sheafify P Q

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
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) (hQ : ) {Z : } (h : Q Z) :
CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift η hQ) h) =
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) (hQ : ) :
CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : P Q) (hQ : ) (γ : J.sheafify P Q) :
CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ = ηγ = J.sheafifyLift η hQ
@[simp]
theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } (hP : ) :
(J.isoSheafify hP).inv = J.sheafifyLift hP
theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } (η : J.sheafify P Q) (γ : J.sheafify P Q) (hQ : ) (h : CategoryTheory.CategoryStruct.comp (J.toSheafify P) η = CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ) :
η = γ
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } {R : } (η : P Q) (γ : Q R) (hR : ) {Z : } (h : R Z) :
CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift γ hR) h) = CategoryTheory.CategoryStruct.comp (J.sheafifyLift hR) h
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : } {Q : } {R : } (η : P Q) (γ : Q R) (hR : ) :
CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyLift γ hR) = J.sheafifyLift hR
theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf {C : Type u} {D : Type w} [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (P : ) :
@[simp]
theorem CategoryTheory.plusPlusSheaf_map_val {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :
∀ {X Y : } (η : X Y), (.map η).val = J.sheafifyMap η
@[simp]
theorem CategoryTheory.plusPlusSheaf_obj_val {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (P : ) :
(.obj P).val = J.sheafify P
noncomputable def CategoryTheory.plusPlusSheaf {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :

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
instance CategoryTheory.plusPlusSheaf_preservesZeroMorphisms {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :
.PreservesZeroMorphisms
Equations
• =
@[simp]
theorem CategoryTheory.plusPlusAdjunction_counit_app_val {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (Y : ) :
(.counit.app Y).val = J.sheafifyLift ()
@[simp]
theorem CategoryTheory.plusPlusAdjunction_unit_app {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (X : ) :
.unit.app X = J.toSheafify X
noncomputable def CategoryTheory.plusPlusAdjunction {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :

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
instance CategoryTheory.sheafToPresheaf_isRightAdjoint {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :
Equations
• =
instance CategoryTheory.presheaf_mono_of_mono {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] {F : } {G : } (f : F G) :
Equations
• =
theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] {F : } {G : } (f : F G) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf_inv_app {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (X : ) :
(J.sheafificationIsoPresheafToSheafCompSheafToPreasheaf D).inv.app X = CategoryTheory.CategoryStruct.id (J.sheafify X)
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf_hom_app {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] (X : ) :
(J.sheafificationIsoPresheafToSheafCompSheafToPreasheaf D).hom.app X = CategoryTheory.CategoryStruct.id (J.sheafify X)
noncomputable def CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf {C : Type u} (D : Type w) [] [∀ (P : ) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [(X : C) → ] [.ReflectsIsomorphisms] :
J.sheafification D .comp
Equations
Instances For