Limits and colimits of sheaves #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
(F : K ⥤ category_theory.Sheaf J D)
(E : category_theory.limits.cone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(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
- category_theory.Sheaf.multifork_evaluation_cone F E X W S = {X := S.X, π := {app := λ (k : K), (category_theory.presheaf.is_limit_of_is_sheaf J (F.obj k).val W _).lift (category_theory.limits.multifork.of_ι (W.index (F.obj k).val) S.X (λ (i : (W.index (F.obj k).val).L), S.ι i ≫ (E.π.app k).app (opposite.op i.Y)) _), naturality' := _}}
noncomputable
def
category_theory.Sheaf.is_limit_multifork_of_is_limit
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape K D]
(F : K ⥤ category_theory.Sheaf J D)
(E : category_theory.limits.cone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(hE : category_theory.limits.is_limit E)
(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
- category_theory.Sheaf.is_limit_multifork_of_is_limit F E hE X W = category_theory.limits.multifork.is_limit.mk (W.multifork E.X) (λ (S : category_theory.limits.multifork (W.index E.X)), (category_theory.limits.is_limit_of_preserves ((category_theory.evaluation Cᵒᵖ D).obj (opposite.op X)) hE).lift (category_theory.Sheaf.multifork_evaluation_cone F E X W S)) _ _
theorem
category_theory.Sheaf.is_sheaf_of_is_limit
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape K D]
(F : K ⥤ category_theory.Sheaf J D)
(E : category_theory.limits.cone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(hE : category_theory.limits.is_limit E) :
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 u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape K D]
(F : K ⥤ category_theory.Sheaf J D) :
Equations
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (E : category_theory.limits.cone (F ⋙ category_theory.Sheaf_to_presheaf J D)) (hE : category_theory.limits.is_limit E), {to_liftable_cone := {lifted_cone := {X := {val := E.X, cond := _}, π := {app := λ (t : K), {val := E.π.app t}, naturality' := _}}, valid_lift := category_theory.limits.cones.ext (category_theory.eq_to_iso _) _}, makes_limit := {lift := λ (S : category_theory.limits.cone F), {val := hE.lift ((category_theory.Sheaf_to_presheaf J D).map_cone S)}, fac' := _, uniq' := _}})
@[protected, instance]
noncomputable
def
category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape K D] :
@[protected, instance]
def
category_theory.Sheaf.category_theory.limits.has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type z}
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape K D] :
@[protected, instance]
noncomputable
def
category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
[category_theory.limits.has_limits D] :
@[protected, instance]
noncomputable
def
category_theory.Sheaf.sheafify_cocone
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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 : K ⥤ category_theory.Sheaf J D}
(E : category_theory.limits.cocone (F ⋙ category_theory.Sheaf_to_presheaf J D)) :
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.
@[simp]
theorem
category_theory.Sheaf.sheafify_cocone_X_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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 : K ⥤ category_theory.Sheaf J D}
(E : category_theory.limits.cocone (F ⋙ category_theory.Sheaf_to_presheaf J D)) :
@[simp]
theorem
category_theory.Sheaf.sheafify_cocone_ι_app_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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 : K ⥤ category_theory.Sheaf J D}
(E : category_theory.limits.cocone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(k : K) :
((category_theory.Sheaf.sheafify_cocone E).ι.app k).val = E.ι.app k ≫ J.to_sheafify E.X
@[simp]
theorem
category_theory.Sheaf.is_colimit_sheafify_cocone_desc_val
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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 : K ⥤ category_theory.Sheaf J D}
(E : category_theory.limits.cocone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(hE : category_theory.limits.is_colimit E)
(S : category_theory.limits.cocone F) :
((category_theory.Sheaf.is_colimit_sheafify_cocone E hE).desc S).val = J.sheafify_lift (hE.desc ((category_theory.Sheaf_to_presheaf J D).map_cocone S)) _
noncomputable
def
category_theory.Sheaf.is_colimit_sheafify_cocone
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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 : K ⥤ category_theory.Sheaf J D}
(E : category_theory.limits.cocone (F ⋙ category_theory.Sheaf_to_presheaf J D))
(hE : category_theory.limits.is_colimit E) :
If E is a colimit cocone of presheaves, over a diagram factoring through sheaves,
then sheafify_cocone E is a colimit cocone.
Equations
- category_theory.Sheaf.is_colimit_sheafify_cocone E hE = {desc := λ (S : category_theory.limits.cocone F), {val := J.sheafify_lift (hE.desc ((category_theory.Sheaf_to_presheaf J D).map_cocone S)) _}, fac' := _, uniq' := _}
@[protected, instance]
def
category_theory.Sheaf.category_theory.limits.has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{D : Type w}
[category_theory.category D]
{K : Type (max v u)}
[category_theory.small_category K]
[category_theory.concrete_category D]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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.limits.has_colimits_of_shape K D] :
@[protected, instance]
def
category_theory.Sheaf.category_theory.limits.has_colimits
{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]
[∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[∀ (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.limits.has_colimits D] :