mathlibdocumentation

category_theory.sites.limits

Limits and colimits of sheaves #

Limits #

We prove that the forgetful functor from Sheaf J D to presheaves creates limits. If the target category D has limits (of a certain shape), this then implies that Sheaf J D has limits of the same shape and that the forgetful functor preserves these limits.

Colimits #

Given a diagram F : K ⥤ Sheaf J D of sheaves, and a colimit cocone on the level of presheaves, we show that the cocone obtained by sheafifying the cocone point is a colimit cocone of sheaves.

This allows us to show that Sheaf J D has colimits (of a certain shape) as soon as D does.

noncomputable def category_theory.Sheaf.multifork_evaluation_cone {C : Type (max v u)} {D : Type w} {K : Type (max v u)} (F : K ) (X : C) (W : J.cover X) (S : category_theory.limits.multifork (W.index E.X)) :

An auxiliary definition to be used below.

Whenever E is a cone of shape K of sheaves, and S is the multifork associated to a covering W of an object X, with respect to the cone point E.X, this provides a cone of shape K of objects in D, with cone point S.X.

See is_limit_multifork_of_is_limit for more on how this definition is used.

Equations
noncomputable def category_theory.Sheaf.is_limit_multifork_of_is_limit {C : Type (max v u)} {D : Type w} {K : Type (max v u)} (F : K ) (X : C) (W : J.cover X) :

If E is a cone of shape K of sheaves, which is a limit on the level of presheves, this definition shows that the limit presheaf satisfies the multifork variant of the sheaf condition, at a given covering W.

This is used below in is_sheaf_of_is_limit to show that the limit presheaf is indeed a sheaf.

Equations
• = (λ (S : , _ _
theorem category_theory.Sheaf.is_sheaf_of_is_limit {C : Type (max v u)} {D : Type w} {K : Type (max v u)} (F : K )  :

If E is a cone which is a limit on the level of presheaves, then the limit presheaf is again a sheaf.

This is used to show that the forgetful functor from sheaves to presheaves creates limits.

@[protected, instance]
noncomputable def category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limit {C : Type (max v u)} {D : Type w} {K : Type (max v u)} (F : K ) :
Equations
@[protected, instance]
noncomputable def category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits_of_shape {C : Type (max v u)} {D : Type w} {K : Type (max v u)}  :
Equations
@[protected, instance]
def category_theory.Sheaf.category_theory.limits.has_limits_of_shape {C : Type (max v u)} {D : Type w} {K : Type (max v u)}  :
@[protected, instance]
noncomputable def category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits {C : Type (max v u)} {D : Type w}  :
Equations
@[protected, instance]
def category_theory.Sheaf.category_theory.limits.has_limits {C : Type (max v u)} {D : Type w}  :
noncomputable def category_theory.Sheaf.sheafify_cocone {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {F : K }  :

Construct a cocone by sheafifying a cocone point of a cocone E of presheaves over a functor which factors through sheaves. In is_colimit_sheafify_cocone, we show that this is a colimit cocone when E is a colimit.

Equations
@[simp]
theorem category_theory.Sheaf.sheafify_cocone_X_val {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {F : K }  :
@[simp]
theorem category_theory.Sheaf.sheafify_cocone_ι_app_val {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {F : K } (k : K) :
@[simp]
theorem category_theory.Sheaf.is_colimit_sheafify_cocone_desc_val {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {F : K }  :
= J.sheafify_lift (hE.desc S)) _
noncomputable def category_theory.Sheaf.is_colimit_sheafify_cocone {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {F : K }  :

If E is a colimit cocone of presheaves, over a diagram factoring through sheaves, then sheafify_cocone E is a colimit cocone.

Equations
@[protected, instance]
def category_theory.Sheaf.category_theory.limits.has_colimits_of_shape {C : Type (max v u)} {D : Type w} {K : Type (max v u)} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ]  :
@[protected, instance]
def category_theory.Sheaf.category_theory.limits.has_colimits {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ]  :