mathlib documentation

category_theory.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

@[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
@[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) :
(P.map I.g₁.op) (x ((S.index P).fst_to I)) = (P.map I.g₂.op) (x ((S.index P).snd_to I))

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} [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) :
(x.refine e) I = x {Y := I.Y, f := I.f, hf := _}

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} [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) :
(x.pullback f) I = x {Y := I.Y, f := I.f f, hf := _}
@[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) :
(x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f

Make a term of meq P S.

Equations

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

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

Equations

The canonical map from P to its sheafification.

Equations

The canonical map on sheafifications induced by a morphism.

Equations

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

Equations

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

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

Equations

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

Equations