# mathlibdocumentation

category_theory.sites.sheafification

# 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} {D : Type w} {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} {D : Type w} {X : C} (P : Cᵒᵖ D) (S : J.cover X) :
(λ (x : , Π (I : S.arrow), (P.obj (opposite.op I.Y)))
Equations
@[ext]
theorem category_theory.meq.ext {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} {S : J.cover X} (x y : S) (h : (I : S.arrow), x I = y I) :
x = y
theorem category_theory.meq.condition {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) (I : S.relation) :
(P.map I.g₁.op) (x ((S.index P).fst_to I)) = (P.map I.g₂.op) (x ((S.index P).snd_to I))
def category_theory.meq.refine {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} {S T : J.cover X} (x : T) (e : S T) :

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

Equations
@[simp]
theorem category_theory.meq.refine_apply {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} {S T : J.cover X} (x : T) (e : S T) (I : S.arrow) :
(x.refine e) I = x {Y := I.Y, f := I.f, hf := _}
def category_theory.meq.pullback {C : Type u} {D : Type w} {Y X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) (f : Y X) :
((J.pullback f).obj S)

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

Equations
@[simp]
theorem category_theory.meq.pullback_apply {C : Type u} {D : Type w} {Y X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) (f : Y X) (I : ((J.pullback f).obj S).arrow) :
(x.pullback f) I = x {Y := I.Y, f := I.f f, hf := _}
@[simp]
theorem category_theory.meq.pullback_refine {C : Type u} {D : Type w} {Y X : C} {P : Cᵒᵖ D} {S T : J.cover X} (h : S T) (f : Y X) (x : T) :
(x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
def category_theory.meq.mk {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} (S : J.cover X) (x : (P.obj (opposite.op X))) :

Make a term of `meq P S`.

Equations
theorem category_theory.meq.mk_apply {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} (S : J.cover X) (x : (P.obj (opposite.op X))) (I : S.arrow) :
I = (P.map I.f.op) x
noncomputable def category_theory.meq.equiv {C : Type u} {D : Type w} {X : C} (P : Cᵒᵖ D) (S : J.cover X)  :

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} {D : Type w} {X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : ) (I : S.arrow) :
( x) I = x
@[simp]
theorem category_theory.meq.equiv_symm_eq_apply {C : Type u} {D : Type w} {X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) (I : S.arrow) :
(.symm) x) = x I
noncomputable def category_theory.grothendieck_topology.plus.mk {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) :

Make a term of `(J.plus_obj P).obj (op X)` from `x : meq P S`.

Equations
theorem category_theory.grothendieck_topology.plus.res_mk_eq_mk_pullback {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {Y X : C} {P : Cᵒᵖ D} {S : J.cover X} (x : S) (f : Y X) :
theorem category_theory.grothendieck_topology.plus.to_plus_mk {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {P : Cᵒᵖ D} (S : J.cover X) (x : (P.obj (opposite.op X))) :
((J.to_plus P).app (opposite.op X)) x =
theorem category_theory.grothendieck_topology.plus.to_plus_apply {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {P : Cᵒᵖ D} (S : J.cover X) (x : S) (I : S.arrow) :
((J.to_plus P).app (opposite.op I.Y)) (x I) = ((J.plus_obj P).map I.f.op)
theorem category_theory.grothendieck_topology.plus.to_plus_eq_mk {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {P : Cᵒᵖ D} (x : (P.obj (opposite.op X))) :
theorem category_theory.grothendieck_topology.plus.exists_rep {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] {X : C} {P : Cᵒᵖ D} (x : ((J.plus_obj P).obj (opposite.op X))) :
(S : J.cover X) (y : ,
theorem category_theory.grothendieck_topology.plus.eq_mk_iff_exists {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] {X : C} {P : Cᵒᵖ D} {S T : J.cover X} (x : S) (y : T) :
(W : J.cover X) (h1 : W S) (h2 : W T), x.refine h1 = y.refine h2
theorem category_theory.grothendieck_topology.plus.sep {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] {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} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] (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) :
noncomputable def category_theory.grothendieck_topology.plus.meq_of_sep {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] (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 : S) (T : Π (I : S.arrow), J.cover I.Y) (t : Π (I : S.arrow), (T I)) (ht : (I : S.arrow), ) :
(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
theorem category_theory.grothendieck_topology.plus.exists_of_sep {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] (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 : S) :
(t : ((J.plus_obj P).obj (opposite.op X))),
theorem category_theory.grothendieck_topology.plus.is_sheaf_of_sep {C : Type u} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] (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} {D : Type w} [ (X : C), ] [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [Π (X : C), ] (P : Cᵒᵖ D) :
(J.plus_obj (J.plus_obj P))

`P⁺⁺` is always a sheaf.

noncomputable def category_theory.grothendieck_topology.sheafify {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] (P : Cᵒᵖ D) :

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

Equations
noncomputable def category_theory.grothendieck_topology.to_sheafify {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] (P : Cᵒᵖ D) :

The canonical map from `P` to its sheafification.

Equations
noncomputable def category_theory.grothendieck_topology.sheafify_map {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) :

The canonical map on sheafifications induced by a morphism.

Equations
@[simp]
theorem category_theory.grothendieck_topology.sheafify_map_id {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] (P : Cᵒᵖ D) :
@[simp]
theorem category_theory.grothendieck_topology.sheafify_map_comp {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q R : Cᵒᵖ D} (η : P Q) (γ : Q R) :
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_naturality_assoc {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) {X' : Cᵒᵖ D} (f' : J.sheafify Q X') :
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_naturality {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) :
noncomputable def category_theory.grothendieck_topology.sheafification {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] :

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

Equations
Instances for `category_theory.grothendieck_topology.sheafification`
@[simp]
theorem category_theory.grothendieck_topology.sheafification_obj {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] (P : Cᵒᵖ D) :
@[simp]
theorem category_theory.grothendieck_topology.sheafification_map {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) :
noncomputable def category_theory.grothendieck_topology.to_sheafification {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] :

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
@[simp]
theorem category_theory.grothendieck_topology.to_sheafification_app {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] (P : Cᵒᵖ D) :
theorem category_theory.grothendieck_topology.is_iso_to_sheafify {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P : Cᵒᵖ D} (hP : P) :
noncomputable def category_theory.grothendieck_topology.iso_sheafify {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P : Cᵒᵖ D} (hP : P) :

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

Equations
@[simp]
theorem category_theory.grothendieck_topology.iso_sheafify_hom {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P : Cᵒᵖ D} (hP : P) :
noncomputable def category_theory.grothendieck_topology.sheafify_lift {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) (hQ : Q) :

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

Equations
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_sheafify_lift_assoc {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) (hQ : Q) {X' : Cᵒᵖ D} (f' : Q X') :
J.to_sheafify P hQ f' = η f'
@[simp]
theorem category_theory.grothendieck_topology.to_sheafify_sheafify_lift {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) (hQ : Q) :
J.to_sheafify P hQ = η
theorem category_theory.grothendieck_topology.sheafify_lift_unique {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) (hQ : Q) (γ : J.sheafify P Q) :
J.to_sheafify P γ = η γ = hQ
@[simp]
theorem category_theory.grothendieck_topology.iso_sheafify_inv {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P : Cᵒᵖ D} (hP : P) :
theorem category_theory.grothendieck_topology.sheafify_hom_ext {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q : Cᵒᵖ D} (η γ : J.sheafify P Q) (hQ : Q) (h : J.to_sheafify P η = J.to_sheafify P γ) :
η = γ
@[simp]
theorem category_theory.grothendieck_topology.sheafify_map_sheafify_lift {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q R : Cᵒᵖ D} (η : P Q) (γ : Q R) (hR : R) :
J.sheafify_map η hR = J.sheafify_lift γ) hR
@[simp]
theorem category_theory.grothendieck_topology.sheafify_map_sheafify_lift_assoc {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] {P Q R : Cᵒᵖ D} (η : P Q) (γ : Q R) (hR : R) {X' : Cᵒᵖ D} (f' : R X') :
J.sheafify_map η hR f' = J.sheafify_lift γ) hR f'
theorem category_theory.grothendieck_topology.sheafify_is_sheaf {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : Cᵒᵖ D) :
@[simp]
theorem category_theory.presheaf_to_Sheaf_map_val {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P Q : Cᵒᵖ D) (η : P Q) :
η).val = J.sheafify_map η
@[simp]
theorem category_theory.presheaf_to_Sheaf_obj_val {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : Cᵒᵖ D) :
P).val = J.sheafify P
noncomputable def category_theory.presheaf_to_Sheaf {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ]  :
(Cᵒᵖ D)

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

Equations
Instances for `category_theory.presheaf_to_Sheaf`
@[protected, instance]
def category_theory.presheaf_to_Sheaf_preserves_zero_morphisms {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ]  :
@[simp]
theorem category_theory.sheafification_adjunction_counit_app_val {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (Y : D) :
@[simp]
theorem category_theory.sheafification_adjunction_unit_app {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (X : Cᵒᵖ D) :
noncomputable def category_theory.sheafification_adjunction {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ]  :

The sheafification functor is left adjoint to the forgetful functor.

Equations
@[protected, instance]
noncomputable def category_theory.Sheaf_to_presheaf_is_right_adjoint {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ]  :
Equations
@[protected, instance]
def category_theory.presheaf_mono_of_mono {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] {F G : D} (f : F G)  :
theorem category_theory.Sheaf.hom.mono_iff_presheaf_mono {C : Type u} (D : Type w) [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] {F G : D} (f : F G) :
@[simp]
theorem category_theory.sheafification_iso_inv_val {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : D) :
@[simp]
theorem category_theory.sheafification_iso_hom_val {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : D) :
noncomputable def category_theory.sheafification_iso {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : D) :
P

A sheaf `P` is isomorphic to its own sheafification.

Equations
@[protected, instance]
def category_theory.is_iso_sheafification_adjunction_counit {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ] (P : D) :
@[protected, instance]
def category_theory.sheafification_reflective {C : Type u} {D : Type w} [ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [ (X : C), ] [Π (X : C), ]  :