Sheafification #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
@[nolint]
def
category_theory.meq
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
(P : Cᵒᵖ ⥤ D)
(S : J.cover X) :
Type (max (max u v) v u)
A concrete version of the multiequalizer, to be used below.
Equations
Instances for category_theory.meq
@[protected, instance]
def
category_theory.meq.has_coe_to_fun
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
(P : Cᵒᵖ ⥤ D)
(S : J.cover X) :
has_coe_to_fun (category_theory.meq P S) (λ (x : category_theory.meq P S), Π (I : S.arrow), ↥(P.obj (opposite.op I.Y)))
Equations
- category_theory.meq.has_coe_to_fun P S = {coe := λ (x : category_theory.meq P S), x.val}
@[ext]
theorem
category_theory.meq.ext
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x y : category_theory.meq P S)
(h : ∀ (I : S.arrow), ⇑x I = ⇑y I) :
x = y
theorem
category_theory.meq.condition
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x : category_theory.meq P S)
(I : S.relation) :
def
category_theory.meq.refine
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S T : J.cover X}
(x : category_theory.meq P T)
(e : S ⟶ T) :
Refine a term of meq P T with respect to a refinement S ⟶ T of covers.
@[simp]
theorem
category_theory.meq.refine_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S T : J.cover X}
(x : category_theory.meq P T)
(e : S ⟶ T)
(I : S.arrow) :
def
category_theory.meq.pullback
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{Y X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x : category_theory.meq P S)
(f : Y ⟶ X) :
category_theory.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.
@[simp]
theorem
category_theory.meq.pullback_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{Y X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x : category_theory.meq P S)
(f : Y ⟶ X)
(I : ((J.pullback f).obj S).arrow) :
@[simp]
theorem
category_theory.meq.pullback_refine
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{Y X : C}
{P : Cᵒᵖ ⥤ D}
{S T : J.cover X}
(h : S ⟶ T)
(f : Y ⟶ X)
(x : category_theory.meq P T) :
def
category_theory.meq.mk
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
(S : J.cover X)
(x : ↥(P.obj (opposite.op X))) :
Make a term of meq P S.
theorem
category_theory.meq.mk_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
{X : C}
{P : Cᵒᵖ ⥤ D}
(S : J.cover X)
(x : ↥(P.obj (opposite.op X)))
(I : S.arrow) :
noncomputable
def
category_theory.meq.equiv
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
{X : C}
(P : Cᵒᵖ ⥤ D)
(S : J.cover X)
[category_theory.limits.has_multiequalizer (S.index P)] :
The equivalence between the type associated to multiequalizer (S.index P) and meq P S.
Equations
@[simp]
theorem
category_theory.meq.equiv_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
[category_theory.limits.has_multiequalizer (S.index P)]
(x : ↥(category_theory.limits.multiequalizer (S.index P)))
(I : S.arrow) :
⇑(⇑(category_theory.meq.equiv P S) x) I = ⇑(category_theory.limits.multiequalizer.ι (S.index P) I) x
@[simp]
theorem
category_theory.meq.equiv_symm_eq_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
[category_theory.limits.has_multiequalizer (S.index P)]
(x : category_theory.meq P S)
(I : S.arrow) :
⇑(category_theory.limits.multiequalizer.ι (S.index P) I) (⇑((category_theory.meq.equiv P S).symm) x) = ⇑x I
noncomputable
def
category_theory.grothendieck_topology.plus.mk
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x : category_theory.meq P S) :
↥((J.plus_obj P).obj (opposite.op X))
Make a term of (J.plus_obj P).obj (op X) from x : meq P S.
Equations
- category_theory.grothendieck_topology.plus.mk x = ⇑(category_theory.limits.colimit.ι (J.diagram P X) (opposite.op S)) (⇑((category_theory.meq.equiv P S).symm) x)
theorem
category_theory.grothendieck_topology.plus.res_mk_eq_mk_pullback
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
{Y X : C}
{P : Cᵒᵖ ⥤ D}
{S : J.cover X}
(x : category_theory.meq P S)
(f : Y ⟶ X) :
theorem
category_theory.grothendieck_topology.plus.to_plus_mk
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
{X : C}
{P : Cᵒᵖ ⥤ D}
(S : J.cover X)
(x : ↥(P.obj (opposite.op X))) :
⇑((J.to_plus P).app (opposite.op X)) x = category_theory.grothendieck_topology.plus.mk (category_theory.meq.mk S x)
theorem
category_theory.grothendieck_topology.plus.to_plus_apply
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
{X : C}
{P : Cᵒᵖ ⥤ D}
(S : J.cover X)
(x : category_theory.meq P S)
(I : S.arrow) :
theorem
category_theory.grothendieck_topology.plus.to_plus_eq_mk
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
{X : C}
{P : Cᵒᵖ ⥤ D}
(x : ↥(P.obj (opposite.op X))) :
⇑((J.to_plus P).app (opposite.op X)) x = category_theory.grothendieck_topology.plus.mk (category_theory.meq.mk ⊤ x)
theorem
category_theory.grothendieck_topology.plus.exists_rep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
{X : C}
{P : Cᵒᵖ ⥤ D}
(x : ↥((J.plus_obj P).obj (opposite.op X))) :
∃ (S : J.cover X) (y : category_theory.meq P S), x = category_theory.grothendieck_topology.plus.mk y
theorem
category_theory.grothendieck_topology.plus.eq_mk_iff_exists
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
{X : C}
{P : Cᵒᵖ ⥤ D}
{S T : J.cover X}
(x : category_theory.meq P S)
(y : category_theory.meq P T) :
theorem
category_theory.grothendieck_topology.plus.sep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
{X : C}
(P : Cᵒᵖ ⥤ D)
(S : J.cover X)
(x y : ↥((J.plus_obj P).obj (opposite.op X)))
(h : ∀ (I : S.arrow), ⇑((J.plus_obj P).map I.f.op) x = ⇑((J.plus_obj P).map I.f.op) y) :
x = y
P⁺ is always separated.
theorem
category_theory.grothendieck_topology.plus.inj_of_sep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D)
(hsep : ∀ (X : C) (S : J.cover X) (x y : ↥(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.to_plus P).app (opposite.op X))
noncomputable
def
category_theory.grothendieck_topology.plus.meq_of_sep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D)
(hsep : ∀ (X : C) (S : J.cover X) (x y : ↥(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 : category_theory.meq (J.plus_obj P) S)
(T : Π (I : S.arrow), J.cover I.Y)
(t : Π (I : S.arrow), category_theory.meq P (T I))
(ht : ∀ (I : S.arrow), ⇑s I = category_theory.grothendieck_topology.plus.mk (t I)) :
category_theory.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
- category_theory.grothendieck_topology.plus.meq_of_sep P hsep X S s T t ht = ⟨λ (I : (S.bind T).arrow), ⇑(t I.from_middle) I.to_middle, _⟩
theorem
category_theory.grothendieck_topology.plus.exists_of_sep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D)
(hsep : ∀ (X : C) (S : J.cover X) (x y : ↥(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 : category_theory.meq (J.plus_obj P) S) :
∃ (t : ↥((J.plus_obj P).obj (opposite.op X))), category_theory.meq.mk S t = s
theorem
category_theory.grothendieck_topology.plus.is_sheaf_of_sep
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D)
(hsep : ∀ (X : C) (S : J.cover X) (x y : ↥(P.obj (opposite.op X))), (∀ (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
category_theory.grothendieck_topology.plus.is_sheaf_plus_plus
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D) :
category_theory.presheaf.is_sheaf J (J.plus_obj (J.plus_obj P))
P⁺⁺ is always a sheaf.
noncomputable
def
category_theory.grothendieck_topology.sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
(P : Cᵒᵖ ⥤ D) :
The sheafification of a presheaf P.
NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!
noncomputable
def
category_theory.grothendieck_topology.to_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
(P : Cᵒᵖ ⥤ D) :
The canonical map from P to its sheafification.
noncomputable
def
category_theory.grothendieck_topology.sheafify_map
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q) :
The canonical map on sheafifications induced by a morphism.
Equations
- J.sheafify_map η = J.plus_map (J.plus_map η)
@[simp]
theorem
category_theory.grothendieck_topology.sheafify_map_id
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
(P : Cᵒᵖ ⥤ D) :
J.sheafify_map (𝟙 P) = 𝟙 (J.sheafify P)
@[simp]
theorem
category_theory.grothendieck_topology.sheafify_map_comp
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q R : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(γ : Q ⟶ R) :
J.sheafify_map (η ≫ γ) = J.sheafify_map η ≫ J.sheafify_map γ
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_naturality_assoc
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
{X' : Cᵒᵖ ⥤ D}
(f' : J.sheafify Q ⟶ X') :
η ≫ J.to_sheafify Q ≫ f' = J.to_sheafify P ≫ J.sheafify_map η ≫ f'
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_naturality
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q) :
η ≫ J.to_sheafify Q = J.to_sheafify P ≫ J.sheafify_map η
noncomputable
def
category_theory.grothendieck_topology.sheafification
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (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.plus_functor D ⋙ J.plus_functor D
Instances for category_theory.grothendieck_topology.sheafification
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_obj
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
(P : Cᵒᵖ ⥤ D) :
(J.sheafification D).obj P = J.sheafify P
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_map
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q) :
(J.sheafification D).map η = J.sheafify_map η
noncomputable
def
category_theory.grothendieck_topology.to_sheafification
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :
𝟭 (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.to_sheafification D = J.to_plus_nat_trans D ≫ category_theory.whisker_right (J.to_plus_nat_trans D) (J.plus_functor D)
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafification_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
(P : Cᵒᵖ ⥤ D) :
(J.to_sheafification D).app P = J.to_sheafify P
theorem
category_theory.grothendieck_topology.is_iso_to_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P : Cᵒᵖ ⥤ D}
(hP : category_theory.presheaf.is_sheaf J P) :
noncomputable
def
category_theory.grothendieck_topology.iso_sheafify
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P : Cᵒᵖ ⥤ D}
(hP : category_theory.presheaf.is_sheaf J P) :
If P is a sheaf, then P is isomorphic to J.sheafify P.
Equations
- J.iso_sheafify hP = let _inst : category_theory.is_iso (J.to_sheafify P) := _ in category_theory.as_iso (J.to_sheafify P)
@[simp]
theorem
category_theory.grothendieck_topology.iso_sheafify_hom
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P : Cᵒᵖ ⥤ D}
(hP : category_theory.presheaf.is_sheaf J P) :
(J.iso_sheafify hP).hom = J.to_sheafify P
noncomputable
def
category_theory.grothendieck_topology.sheafify_lift
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(hQ : category_theory.presheaf.is_sheaf J Q) :
Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from
J.sheafifcation P to Q.
Equations
- J.sheafify_lift η hQ = J.plus_lift (J.plus_lift η hQ) hQ
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_sheafify_lift_assoc
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(hQ : category_theory.presheaf.is_sheaf J Q)
{X' : Cᵒᵖ ⥤ D}
(f' : Q ⟶ X') :
J.to_sheafify P ≫ J.sheafify_lift η hQ ≫ f' = η ≫ f'
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_sheafify_lift
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(hQ : category_theory.presheaf.is_sheaf J Q) :
J.to_sheafify P ≫ J.sheafify_lift η hQ = η
theorem
category_theory.grothendieck_topology.sheafify_lift_unique
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(hQ : category_theory.presheaf.is_sheaf J Q)
(γ : J.sheafify P ⟶ Q) :
J.to_sheafify P ≫ γ = η → γ = J.sheafify_lift η hQ
@[simp]
theorem
category_theory.grothendieck_topology.iso_sheafify_inv
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P : Cᵒᵖ ⥤ D}
(hP : category_theory.presheaf.is_sheaf J P) :
(J.iso_sheafify hP).inv = J.sheafify_lift (𝟙 P) hP
theorem
category_theory.grothendieck_topology.sheafify_hom_ext
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q : Cᵒᵖ ⥤ D}
(η γ : J.sheafify P ⟶ Q)
(hQ : category_theory.presheaf.is_sheaf J Q)
(h : J.to_sheafify P ≫ η = J.to_sheafify P ≫ γ) :
η = γ
@[simp]
theorem
category_theory.grothendieck_topology.sheafify_map_sheafify_lift
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q R : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(γ : Q ⟶ R)
(hR : category_theory.presheaf.is_sheaf J R) :
J.sheafify_map η ≫ J.sheafify_lift γ hR = J.sheafify_lift (η ≫ γ) hR
@[simp]
theorem
category_theory.grothendieck_topology.sheafify_map_sheafify_lift_assoc
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
{P Q R : Cᵒᵖ ⥤ D}
(η : P ⟶ Q)
(γ : Q ⟶ R)
(hR : category_theory.presheaf.is_sheaf J R)
{X' : Cᵒᵖ ⥤ D}
(f' : R ⟶ X') :
J.sheafify_map η ≫ J.sheafify_lift γ hR ≫ f' = J.sheafify_lift (η ≫ γ) hR ≫ f'
theorem
category_theory.grothendieck_topology.sheafify_is_sheaf
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D) :
@[simp]
theorem
category_theory.presheaf_to_Sheaf_map_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P Q : Cᵒᵖ ⥤ D)
(η : P ⟶ Q) :
((category_theory.presheaf_to_Sheaf J D).map η).val = J.sheafify_map η
@[simp]
theorem
category_theory.presheaf_to_Sheaf_obj_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : Cᵒᵖ ⥤ D) :
((category_theory.presheaf_to_Sheaf J D).obj P).val = J.sheafify P
noncomputable
def
category_theory.presheaf_to_Sheaf
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)] :
(Cᵒᵖ ⥤ D) ⥤ category_theory.Sheaf J D
The sheafification functor, as a functor taking values in Sheaf.
Equations
@[protected, instance]
def
category_theory.presheaf_to_Sheaf_preserves_zero_morphisms
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
[category_theory.preadditive D] :
@[simp]
theorem
category_theory.sheafification_adjunction_counit_app_val
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(Y : category_theory.Sheaf J D) :
((category_theory.sheafification_adjunction J D).counit.app Y).val = J.sheafify_lift (𝟙 Y.val) _
@[simp]
theorem
category_theory.sheafification_adjunction_unit_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(X : Cᵒᵖ ⥤ D) :
(category_theory.sheafification_adjunction J D).unit.app X = J.to_sheafify X
noncomputable
def
category_theory.sheafification_adjunction
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)] :
The sheafification functor is left adjoint to the forgetful functor.
Equations
- category_theory.sheafification_adjunction J D = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (P : Cᵒᵖ ⥤ D) (Q : category_theory.Sheaf J D), {to_fun := λ (e : (category_theory.presheaf_to_Sheaf J D).obj P ⟶ Q), J.to_sheafify P ≫ e.val, inv_fun := λ (e : P ⟶ (category_theory.Sheaf_to_presheaf J D).obj Q), {val := J.sheafify_lift e _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
@[protected, instance]
noncomputable
def
category_theory.Sheaf_to_presheaf_is_right_adjoint
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)] :
Equations
- category_theory.Sheaf_to_presheaf_is_right_adjoint J D = {left := category_theory.presheaf_to_Sheaf J D _inst_8, adj := category_theory.sheafification_adjunction J D _inst_8}
@[protected, instance]
def
category_theory.presheaf_mono_of_mono
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
{F G : category_theory.Sheaf J D}
(f : F ⟶ G)
[category_theory.mono f] :
theorem
category_theory.Sheaf.hom.mono_iff_presheaf_mono
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(D : Type w)
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
{F G : category_theory.Sheaf J D}
(f : F ⟶ G) :
@[simp]
theorem
category_theory.sheafification_iso_inv_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : category_theory.Sheaf J D) :
(category_theory.sheafification_iso P).inv.val = (J.iso_sheafify _).inv
@[simp]
theorem
category_theory.sheafification_iso_hom_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : category_theory.Sheaf J D) :
(category_theory.sheafification_iso P).hom.val = (J.iso_sheafify _).hom
noncomputable
def
category_theory.sheafification_iso
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : category_theory.Sheaf J D) :
P ≅ (category_theory.presheaf_to_Sheaf J D).obj P.val
A sheaf P is isomorphic to its own sheafification.
Equations
- category_theory.sheafification_iso P = {hom := {val := (J.iso_sheafify _).hom}, inv := {val := (J.iso_sheafify _).inv}, hom_inv_id' := _, inv_hom_id' := _}
@[protected, instance]
def
category_theory.is_iso_sheafification_adjunction_counit
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)]
(P : category_theory.Sheaf J D) :
@[protected, instance]
def
category_theory.sheafification_reflective
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)] :