# Documentation

Mathlib.CategoryTheory.Sites.Sheafification

# Sheafification #

We construct the sheafification of a presheaf over a site C with values in D whenever D is a concrete category for which the forgetful functor preserves the appropriate (co)limits and reflects isomorphisms.

We generally follow the approach of https://stacks.math.columbia.edu/tag/00W1

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

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

Instances For
theorem CategoryTheory.Meq.ext {C : Type u} {D : Type w} [] {X : C} {P : } (x : ) (y : ) (h : ∀ (I : ), x I = y I) :
x = y
theorem CategoryTheory.Meq.condition {C : Type u} {D : Type w} [] {X : C} {P : } (x : ) :
↑(P.map I.g₁.op) () = ↑(P.map I.g₂.op) ()
def CategoryTheory.Meq.refine {C : Type u} {D : Type w} [] {X : C} {P : } (x : ) (e : S T) :

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

Instances For
@[simp]
theorem CategoryTheory.Meq.refine_apply {C : Type u} {D : Type w} [] {X : C} {P : } (x : ) (e : S T) :
↑() I = x { Y := I.Y, f := I.f, hf := (_ : ((fun a => a) T).arrows I.f) }
def CategoryTheory.Meq.pullback {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } (x : ) (f : Y X) :

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

Instances For
@[simp]
theorem CategoryTheory.Meq.pullback_apply {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } (x : ) (f : Y X) :
↑() I = x { Y := I.Y, f := , hf := (_ : ().arrows I.f) }
@[simp]
theorem CategoryTheory.Meq.pullback_refine {C : Type u} {D : Type w} [] {Y : C} {X : C} {P : } (h : S T) (f : Y X) (x : ) :
def CategoryTheory.Meq.mk {C : Type u} {D : Type w} [] {X : C} {P : } (x : ().obj (P.obj ())) :

Make a term of Meq P S.

Instances For
theorem CategoryTheory.Meq.mk_apply {C : Type u} {D : Type w} [] {X : C} {P : } (x : ().obj (P.obj ())) :
↑() I = ↑(P.map I.f.op) x
noncomputable def CategoryTheory.Meq.equiv {C : Type u} {D : Type w} [] {X : C} (P : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Meq.equiv_apply {C : Type u} {D : Type w} [] {X : C} {P : } :
↑(↑() x) I =
@[simp]
theorem CategoryTheory.Meq.equiv_symm_eq_apply {C : Type u} {D : Type w} [] {X : C} {P : } (x : ) :
↑() (().symm x) = x I
def CategoryTheory.GrothendieckTopology.Plus.mk {C : Type u} {D : Type w} [] [] [] {X : C} {P : } (x : ) :
().obj (().obj ())

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

Instances For
theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback {C : Type u} {D : Type w} [] [] [] {Y : C} {X : C} {P : } (x : ) (f : Y X) :
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk {C : Type u} {D : Type w} [] [] [] {X : C} {P : } (x : ().obj (P.obj ())) :
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply {C : Type u} {D : Type w} [] [] [] {X : C} {P : } (x : ) :
↑(().app (Opposite.op I.Y)) (x I) = ↑(().map I.f.op) ()
theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk {C : Type u} {D : Type w} [] [] [] {X : C} {P : } (x : ().obj (P.obj ())) :
theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep {C : Type u} {D : Type w} [] [] [] [] {X : C} {P : } (x : ().obj (().obj ())) :
theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists {C : Type u} {D : Type w} [] [] [] [] {X : C} {P : } (x : ) (y : ) :
theorem CategoryTheory.GrothendieckTopology.Plus.sep {C : Type u} {D : Type w} [] [] [] [] {X : C} (P : ) (x : ().obj (().obj ())) (y : ().obj (().obj ())) (h : ∀ (I : ), ↑(().map I.f.op) x = ↑(().map I.f.op) y) :
x = y

P⁺ is always separated.

theorem CategoryTheory.GrothendieckTopology.Plus.inj_of_sep {C : Type u} {D : Type w} [] [] [] [] (P : ) (hsep : ∀ (X : C) (S : ) (x y : ().obj (P.obj ())), (∀ (I : ), ↑(P.map I.f.op) x = ↑(P.map I.f.op) y) → x = y) (X : C) :
Function.Injective ↑(().app ())
def CategoryTheory.GrothendieckTopology.Plus.meqOfSep {C : Type u} {D : Type w} [] [] [] [] (P : ) (hsep : ∀ (X : C) (S : ) (x y : ().obj (P.obj ())), (∀ (I : ), ↑(P.map I.f.op) x = ↑(P.map I.f.op) y) → x = y) (X : C) (T : ) (t : ) (ht : ) :

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.

Instances For
theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep {C : Type u} {D : Type w} [] [] [] [] (P : ) (hsep : ∀ (X : C) (S : ) (x y : ().obj (P.obj ())), (∀ (I : ), ↑(P.map I.f.op) x = ↑(P.map I.f.op) y) → x = y) (X : C) :
t,
theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep {C : Type u} {D : Type w} [] [] [] [] (P : ) (hsep : ∀ (X : C) (S : ) (x y : ().obj (P.obj ())), (∀ (I : ), ↑(P.map I.f.op) x = ↑(P.map I.f.op) y) → x = y) :

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

P⁺⁺ is always a sheaf.

noncomputable def CategoryTheory.GrothendieckTopology.sheafify {C : Type u} {D : Type w} [] [] [] (P : ) :

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

Instances For
noncomputable def CategoryTheory.GrothendieckTopology.toSheafify {C : Type u} {D : Type w} [] [] [] (P : ) :

The canonical map from P to its sheafification.

Instances For
noncomputable def CategoryTheory.GrothendieckTopology.sheafifyMap {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) :

The canonical map on sheafifications induced by a morphism.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id {C : Type u} {D : Type w} [] [] [] (P : ) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp {C : Type u} {D : Type w} [] [] [] {P : } {Q : } {R : } (η : P Q) (γ : Q R) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) {Z : } (h : ) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) :
noncomputable def CategoryTheory.GrothendieckTopology.sheafification {C : Type u} (D : Type w) [] [] [] :

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

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafification_obj {C : Type u} (D : Type w) [] [] [] (P : ) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafification_map {C : Type u} (D : Type w) [] [] [] {P : } {Q : } (η : P Q) :
noncomputable def CategoryTheory.GrothendieckTopology.toSheafification {C : Type u} (D : Type w) [] [] [] :

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.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafification_app {C : Type u} (D : Type w) [] [] [] (P : ) :
theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify {C : Type u} {D : Type w} [] [] [] {P : } (hP : ) :
noncomputable def CategoryTheory.GrothendieckTopology.isoSheafify {C : Type u} {D : Type w} [] [] [] {P : } (hP : ) :

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

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom {C : Type u} {D : Type w} [] [] [] {P : } (hP : ) :
noncomputable def CategoryTheory.GrothendieckTopology.sheafifyLift {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) (hQ : ) :

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

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) (hQ : ) {Z : } (h : Q Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) (hQ : ) :
theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : P Q) (hQ : ) (γ : ) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv {C : Type u} {D : Type w} [] [] [] {P : } (hP : ) :
theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext {C : Type u} {D : Type w} [] [] [] {P : } {Q : } (η : ) (γ : ) (hQ : ) :
η = γ
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc {C : Type u} {D : Type w} [] [] [] {P : } {Q : } {R : } (η : P Q) (γ : Q R) (hR : ) {Z : } (h : R Z) :
@[simp]
theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift {C : Type u} {D : Type w} [] [] [] {P : } {Q : } {R : } (η : P Q) (γ : Q R) (hR : ) :
@[simp]
theorem CategoryTheory.presheafToSheaf_obj_val {C : Type u} (D : Type w) [] [] [] [] (P : ) :
(().obj P).val =
@[simp]
theorem CategoryTheory.presheafToSheaf_map_val {C : Type u} (D : Type w) [] [] [] [] :
∀ {X Y : } (η : X Y), (().map η).val =
noncomputable def CategoryTheory.presheafToSheaf {C : Type u} (D : Type w) [] [] [] [] :

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

Instances For
@[simp]
theorem CategoryTheory.sheafificationAdjunction_counit_app_val {C : Type u} (D : Type w) [] [] [] [] (Y : ) :
(().counit.app Y).val =
@[simp]
theorem CategoryTheory.sheafificationAdjunction_unit_app {C : Type u} (D : Type w) [] [] [] [] (X : ) :
noncomputable def CategoryTheory.sheafificationAdjunction {C : Type u} (D : Type w) [] [] [] [] :

The sheafification functor is left adjoint to the forgetful functor.

Instances For
noncomputable instance CategoryTheory.sheafToPresheafIsRightAdjoint {C : Type u} (D : Type w) [] [] [] [] :
instance CategoryTheory.presheaf_mono_of_mono {C : Type u} (D : Type w) [] [] [] [] {F : } {G : } (f : F G) :
theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono {C : Type u} (D : Type w) [] [] [] [] {F : } {G : } (f : F G) :
@[simp]
@[simp]
Instances For
@[simp]
theorem CategoryTheory.sheafificationIso_hom_val {C : Type u} {D : Type w} [] [] [] [] (P : ) :
().hom.val = ().hom
@[simp]
theorem CategoryTheory.sheafificationIso_inv_val {C : Type u} {D : Type w} [] [] [] [] (P : ) :
().inv.val = ().inv
noncomputable def CategoryTheory.sheafificationIso {C : Type u} {D : Type w} [] [] [] [] (P : ) :
P ().obj P.val

A sheaf P is isomorphic to its own sheafification.

Instances For
instance CategoryTheory.isIso_sheafificationAdjunction_counit {C : Type u} {D : Type w} [] [] [] [] (P : ) :
CategoryTheory.IsIso (().counit.app P)
instance CategoryTheory.sheafification_reflective {C : Type u} {D : Type w} [] [] [] [] :