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} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {X : C} (P : Functor Cᵒᵖ D) (S : J.Cover X) : Type (max 0 u v)

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

Equations

• CategoryTheory.Meq P S = { x : (I : S.Arrow) → (CategoryTheory.forget D).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) }

instance CategoryTheory.Meq.instCoeFunForallObjForgetOppositeOpY {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {X : C} (P : Functor Cᵒᵖ D) (S : J.Cover X) : CoeFun (Meq P S) fun (x : Meq P S) => (I : S.Arrow) → (forget D).obj (P.obj (Opposite.op I.Y))

Equations

• CategoryTheory.Meq.instCoeFunForallObjForgetOppositeOpY P S = { coe := fun (x : CategoryTheory.Meq P S) => ↑x }

theorem CategoryTheory.Meq.congr_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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 := ⋯ }

theorem CategoryTheory.Meq.ext {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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

theorem CategoryTheory.Meq.condition {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {X : C} {P : Functor Cᵒᵖ D} {S : J.Cover X} (x : 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))

def CategoryTheory.Meq.refine {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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

• x.refine e = ⟨fun (I : S.Arrow) => ↑x { Y := I.Y, f := I.f, hf := ⋯ }, ⋯⟩

@[simp]

theorem CategoryTheory.Meq.refine_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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 := ⋯ }

def CategoryTheory.Meq.pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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

• x.pullback f = ⟨fun (I : ((J.pullback f).obj S).Arrow) => ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }, ⋯⟩

@[simp]

theorem CategoryTheory.Meq.pullback_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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 := ⋯ }

@[simp]

theorem CategoryTheory.Meq.pullback_refine {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {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

def CategoryTheory.Meq.mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {X : C} {P : Functor Cᵒᵖ D} (S : J.Cover X) (x : (forget D).obj (P.obj (Opposite.op X))) : Meq P S

Make a term of Meq P S.

Equations

• CategoryTheory.Meq.mk S x = ⟨fun (I : S.Arrow) => (P.map I.f.op) x, ⋯⟩

theorem CategoryTheory.Meq.mk_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] {X : C} {P : Functor Cᵒᵖ D} (S : J.Cover X) (x : (forget D).obj (P.obj (Opposite.op X))) (I : S.Arrow) : ↑(mk S x) I = (P.map I.f.op) x

noncomputable def CategoryTheory.Meq.equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (forget D)] {X : C} (P : Functor Cᵒᵖ D) (S : J.Cover X) [Limits.HasMultiequalizer (S.index P)] : (forget D).obj (Limits.multiequalizer (S.index P)) ≃ Meq P S

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

Equations

• CategoryTheory.Meq.equiv P S = CategoryTheory.Limits.Concrete.multiequalizerEquiv (S.index P)

@[simp]

theorem CategoryTheory.Meq.equiv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (forget D)] {X : C} {P : Functor Cᵒᵖ D} {S : J.Cover X} [Limits.HasMultiequalizer (S.index P)] (x : (forget D).obj (Limits.multiequalizer (S.index P))) (I : S.Arrow) : ↑((equiv P S) x) I = (Limits.Multiequalizer.ι (S.index P) I) x

theorem CategoryTheory.Meq.equiv_symm_eq_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (forget D)] {X : C} {P : Functor Cᵒᵖ D} {S : J.Cover X} [Limits.HasMultiequalizer (S.index P)] (x : Meq P S) (I : S.Arrow) : (Limits.Multiequalizer.ι (S.index P) I) ((equiv P S).symm x) = ↑x I

def CategoryTheory.GrothendieckTopology.Plus.mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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) : (forget D).obj ((J.plusObj P).obj (Opposite.op X))

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

Equations

• CategoryTheory.GrothendieckTopology.Plus.mk x = (CategoryTheory.Limits.colimit.ι (J.diagram P X) (Opposite.op S)) ((CategoryTheory.Meq.equiv P S).symm x)

theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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) : ((J.plusObj P).map f.op) (mk x) = mk (x.pullback f)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (forget D).obj (P.obj (Opposite.op X))) : ((J.toPlus P).app (Opposite.op X)) x = mk (Meq.mk S x)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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) : ((J.toPlus P).app (Opposite.op I.Y)) (↑x I) = ((J.plusObj P).map I.f.op) (mk x)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (forget D).obj (P.obj (Opposite.op X))) : ((J.toPlus P).app (Opposite.op X)) x = mk (Meq.mk ⊤ x)

theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (forget D).obj ((J.plusObj P).obj (Opposite.op X))) : ∃ (S : J.Cover X) (y : Meq P S), x = mk y

theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

theorem CategoryTheory.GrothendieckTopology.Plus.sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (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} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (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} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (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 : 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

• CategoryTheory.GrothendieckTopology.Plus.meqOfSep P hsep X S s T t ht = ⟨fun (I : (S.bind T).Arrow) => ↑(t I.fromMiddle) I.toMiddle, ⋯⟩

theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (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 : Meq (J.plusObj P) S) : ∃ (t : (forget D).obj ((J.plusObj P).obj (Opposite.op X))), Meq.mk S t = s

theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 : (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) : Presheaf.IsSheaf J (J.plusObj P)

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

theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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.

noncomputable def CategoryTheory.GrothendieckTopology.sheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

• J.sheafify P = J.plusObj (J.plusObj P)

noncomputable def CategoryTheory.GrothendieckTopology.toSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

• J.toSheafify P = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap (J.toPlus P))

noncomputable def CategoryTheory.GrothendieckTopology.sheafifyMap {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

• J.sheafifyMap η = J.plusMap (J.plusMap η)

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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)

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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 γ)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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 η)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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)

noncomputable def CategoryTheory.GrothendieckTopology.sheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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

• J.sheafification D = (J.plusFunctor D).comp (J.plusFunctor D)

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafification_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafification_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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 η

noncomputable def CategoryTheory.GrothendieckTopology.toSheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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

• J.toSheafification D = CategoryTheory.CategoryStruct.comp (J.toPlusNatTrans D) (CategoryTheory.whiskerRight (J.toPlusNatTrans D) (J.plusFunctor D))

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafification_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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

theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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)

noncomputable def CategoryTheory.GrothendieckTopology.isoSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

• J.isoSheafify hP = CategoryTheory.asIso (J.toSheafify P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

noncomputable def CategoryTheory.GrothendieckTopology.sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

• J.sheafifyLift η hQ = J.plusLift (J.plusLift η hQ) hQ

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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) = η

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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) γ) : η = γ

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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

theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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)

noncomputable def CategoryTheory.plusPlusSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

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

@[simp]

theorem CategoryTheory.plusPlusSheaf_map_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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 η

@[simp]

theorem CategoryTheory.plusPlusSheaf_obj_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

instance CategoryTheory.plusPlusSheaf_preservesZeroMorphisms {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

noncomputable def CategoryTheory.plusPlusAdjunction {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

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

@[simp]

theorem CategoryTheory.plusPlusAdjunction_unit_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

@[simp]

theorem CategoryTheory.plusPlusAdjunction_counit_app_val {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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) ⋯

instance CategoryTheory.sheafToPresheaf_isRightAdjoint {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

instance CategoryTheory.presheaf_mono_of_mono {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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

theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [HasForget D] [Limits.PreservesLimits (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