mathlib3 documentation

topology.sheaves.limits

Presheaves in C have limits and colimits when C does. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def Top.presheaf.category_theory.limits.has_limits {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] (X : Top) :
category_theory.limits.has_limits (Top.presheaf C X)
source
@[protected, instance]
def Top.presheaf.category_theory.limits.has_colimits_of_size {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] (X : Top) :
category_theory.limits.has_colimits_of_size (Top.presheaf C X)
source
@[protected, instance]
noncomputable def Top.sheaf.forget.category_theory.creates_limits {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] (X : Top) :
category_theory.creates_limits (Top.sheaf.forget C X)
Equations
source
@[protected, instance]
def Top.sheaf.category_theory.limits.has_limits_of_size {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] (X : Top) :
category_theory.limits.has_limits_of_size (Top.sheaf C X)
source
theorem Top.is_sheaf_of_is_limit {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] [category_theory.limits.has_limits C] {X : Top} (F : J ⥤ Top.presheaf C X) (H : ∀ (j : J), (F.obj j).is_sheaf) {c : category_theory.limits.cone F} (hc : category_theory.limits.is_limit c) :
c.X.is_sheaf
source
theorem Top.limit_is_sheaf {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] [category_theory.limits.has_limits C] {X : Top} (F : J ⥤ Top.presheaf C X) (H : ∀ (j : J), (F.obj j).is_sheaf) :
(category_theory.limits.limit F).is_sheaf