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

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

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

theorem CategoryTheory.Meq.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (y : CategoryTheory.Meq P S) (h : ∀ (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S), ↑x I = ↑y I) : x = y

theorem CategoryTheory.Meq.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : ↑(P.map I.g₁.op) (↑x (CategoryTheory.Limits.MulticospanIndex.fstTo (CategoryTheory.GrothendieckTopology.Cover.index S P) I)) = ↑(P.map I.g₂.op) (↑x (CategoryTheory.Limits.MulticospanIndex.sndTo (CategoryTheory.GrothendieckTopology.Cover.index S P) I))

def CategoryTheory.Meq.refine {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P T) (e : S ⟶ T) : CategoryTheory.Meq P S

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

@[simp]

theorem CategoryTheory.Meq.refine_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P T) (e : S ⟶ T) (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) : ↑(CategoryTheory.Meq.refine x e) I = ↑x { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) T).arrows I.f) }

def CategoryTheory.Meq.pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X) : CategoryTheory.Meq P ((CategoryTheory.GrothendieckTopology.pullback J f).obj S)

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

@[simp]

theorem CategoryTheory.Meq.pullback_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X) (I : CategoryTheory.GrothendieckTopology.Cover.Arrow ((CategoryTheory.GrothendieckTopology.pullback J f).obj S)) : ↑(CategoryTheory.Meq.pullback x f) I = ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := (_ : (CategoryTheory.GrothendieckTopology.Cover.sieve ((CategoryTheory.GrothendieckTopology.pullback J f).obj S)).arrows I.f) }

@[simp]

theorem CategoryTheory.Meq.pullback_refine {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (h : S ⟶ T) (f : Y ⟶ X) (x : CategoryTheory.Meq P T) : CategoryTheory.Meq.refine (CategoryTheory.Meq.pullback x f) ((CategoryTheory.GrothendieckTopology.pullback J f).map h) = CategoryTheory.Meq.pullback (CategoryTheory.Meq.refine x h) f

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

Make a term of Meq P S.

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

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.GrothendieckTopology.Plus.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) : (CategoryTheory.forget D).obj ((CategoryTheory.GrothendieckTopology.plusObj J P).obj (Opposite.op X))

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

theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {Y : C} {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X) : ↑((CategoryTheory.GrothendieckTopology.plusObj J P).map f.op) (CategoryTheory.GrothendieckTopology.Plus.mk x) = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.pullback x f)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : CategoryTheory.GrothendieckTopology.Cover J X) (x : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))) : ↑((CategoryTheory.GrothendieckTopology.toPlus J P).app (Opposite.op X)) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk S x)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : CategoryTheory.GrothendieckTopology.Cover J X) (x : CategoryTheory.Meq P S) (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) : ↑((CategoryTheory.GrothendieckTopology.toPlus J P).app (Opposite.op I.Y)) (↑x I) = ↑((CategoryTheory.GrothendieckTopology.plusObj J P).map I.f.op) (CategoryTheory.GrothendieckTopology.Plus.mk x)

theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (x : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))) : ↑((CategoryTheory.GrothendieckTopology.toPlus J P).app (Opposite.op X)) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk ⊤ x)

theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (x : (CategoryTheory.forget D).obj ((CategoryTheory.GrothendieckTopology.plusObj J P).obj (Opposite.op X))) : ∃ S y, x = CategoryTheory.GrothendieckTopology.Plus.mk y

theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (x : CategoryTheory.Meq P S) (y : CategoryTheory.Meq P T) : CategoryTheory.GrothendieckTopology.Plus.mk x = CategoryTheory.GrothendieckTopology.Plus.mk y ↔ ∃ W h1 h2, CategoryTheory.Meq.refine x h1 = CategoryTheory.Meq.refine y h2

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

P⁺ is always separated.

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

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

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

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

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

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

P⁺⁺ is always a sheaf.

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

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

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

The canonical map from P to its sheafification.

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

The canonical map on sheafifications induced by a morphism.

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.sheafifyMap J (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (CategoryTheory.GrothendieckTopology.sheafify J P)

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : CategoryTheory.GrothendieckTopology.sheafifyMap J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyMap J η) (CategoryTheory.GrothendieckTopology.sheafifyMap J γ)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.GrothendieckTopology.sheafify J Q ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J Q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyMap J η) h)

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.GrothendieckTopology.toSheafify J Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) (CategoryTheory.GrothendieckTopology.sheafifyMap J η)

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafification_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.sheafification J D).obj P = CategoryTheory.GrothendieckTopology.sheafify J P

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafification_map {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : (CategoryTheory.GrothendieckTopology.sheafification J D).map η = CategoryTheory.GrothendieckTopology.sheafifyMap J η

noncomputable def CategoryTheory.GrothendieckTopology.toSheafification {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] : CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ CategoryTheory.GrothendieckTopology.sheafification J 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.

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafification_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.toSheafification J D).app P = CategoryTheory.GrothendieckTopology.toSheafify J P

theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.toSheafify J P)

noncomputable def CategoryTheory.GrothendieckTopology.isoSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ CategoryTheory.GrothendieckTopology.sheafify J P

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : (CategoryTheory.GrothendieckTopology.isoSheafify J hP).hom = CategoryTheory.GrothendieckTopology.toSheafify J P

noncomputable def CategoryTheory.GrothendieckTopology.sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.GrothendieckTopology.sheafify J P ⟶ Q

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyLift J η hQ) h) = CategoryTheory.CategoryStruct.comp η h

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) (CategoryTheory.GrothendieckTopology.sheafifyLift J η hQ) = η

theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : CategoryTheory.GrothendieckTopology.sheafify J P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) γ = η → γ = CategoryTheory.GrothendieckTopology.sheafifyLift J η hQ

@[simp]

theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : (CategoryTheory.GrothendieckTopology.isoSheafify J hP).inv = CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP

theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : CategoryTheory.GrothendieckTopology.sheafify J P ⟶ Q) (γ : CategoryTheory.GrothendieckTopology.sheafify J P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J P) γ) : η = γ

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyMap J η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyLift J γ hR) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyMap J η) (CategoryTheory.GrothendieckTopology.sheafifyLift J γ hR) = CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR

theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.GrothendieckTopology.sheafify J P)

@[simp]

theorem CategoryTheory.presheafToSheaf_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) : ((CategoryTheory.presheafToSheaf J D).obj P).val = CategoryTheory.GrothendieckTopology.sheafify J P

@[simp]

theorem CategoryTheory.presheafToSheaf_map_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : ∀ {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y), ((CategoryTheory.presheafToSheaf J D).map η).val = CategoryTheory.GrothendieckTopology.sheafifyMap J η

noncomputable def CategoryTheory.presheafToSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Sheaf J D)

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

instance CategoryTheory.presheafToSheaf_preservesZeroMorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Preadditive D] : CategoryTheory.Functor.PreservesZeroMorphisms (CategoryTheory.presheafToSheaf J D)

@[simp]

theorem CategoryTheory.sheafificationAdjunction_counit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationAdjunction J D).counit.app Y).val = CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.CategoryStruct.id Y.val) (_ : CategoryTheory.Presheaf.IsSheaf J Y.val)

@[simp]

theorem CategoryTheory.sheafificationAdjunction_unit_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (X : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafificationAdjunction J D).unit.app X = CategoryTheory.GrothendieckTopology.toSheafify J X

noncomputable def CategoryTheory.sheafificationAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.presheafToSheaf J D ⊣ CategoryTheory.sheafToPresheaf J D

The sheafification functor is left adjoint to the forgetful functor.

noncomputable instance CategoryTheory.sheafToPresheafIsRightAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.IsRightAdjoint (CategoryTheory.sheafToPresheaf J D)

instance CategoryTheory.presheaf_mono_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Sheaf J D} {G : CategoryTheory.Sheaf J D} (f : F ⟶ G) [CategoryTheory.Mono f] : CategoryTheory.Mono f.val

theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Sheaf J D} {G : CategoryTheory.Sheaf J D} (f : F ⟶ G) : CategoryTheory.Mono f ↔ CategoryTheory.Mono f.val

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (X : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf J D).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.GrothendieckTopology.sheafify J X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (X : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf J D).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.GrothendieckTopology.sheafify J X)

noncomputable def CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.GrothendieckTopology.sheafification J D ≅ CategoryTheory.Functor.comp (CategoryTheory.presheafToSheaf J D) (CategoryTheory.sheafToPresheaf J D)

@[simp]

theorem CategoryTheory.sheafificationIso_hom_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Sheaf J D) : (CategoryTheory.sheafificationIso P).hom.val = (CategoryTheory.GrothendieckTopology.isoSheafify J (_ : CategoryTheory.Presheaf.IsSheaf J P.val)).hom

@[simp]

theorem CategoryTheory.sheafificationIso_inv_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Sheaf J D) : (CategoryTheory.sheafificationIso P).inv.val = (CategoryTheory.GrothendieckTopology.isoSheafify J (_ : CategoryTheory.Presheaf.IsSheaf J P.val)).inv

noncomputable def CategoryTheory.sheafificationIso {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Sheaf J D) : P ≅ (CategoryTheory.presheafToSheaf J D).obj P.val

A sheaf P is isomorphic to its own sheafification.

instance CategoryTheory.isIso_sheafificationAdjunction_counit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (P : CategoryTheory.Sheaf J D) : CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P)

instance CategoryTheory.sheafification_reflective {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.IsIso (CategoryTheory.sheafificationAdjunction J D).counit