@[simp]
theorem
category_theory.functor.to_cocone_ι_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
(j : J) :
@[simp]
theorem
category_theory.functor.to_cocone_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X) :
def
category_theory.functor.to_cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X) :
@[simp]
theorem
category_theory.functor.to_cone_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X) :
def
category_theory.functor.to_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X) :
@[simp]
theorem
category_theory.functor.to_cone_π_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
(j : J) :
@[simp]
theorem
category_theory.over.colimit_ι_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)]
(j : J) :
@[simp]
theorem
category_theory.over.colimit_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)] :
def
category_theory.over.colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)] :
Equations
- category_theory.over.colimit F = {X := category_theory.over.mk (category_theory.limits.colimit.desc (F ⋙ category_theory.over.forget) F.to_cocone), ι := {app := λ (j : J), category_theory.over.hom_mk (category_theory.limits.colimit.ι (F ⋙ category_theory.over.forget) j) _, naturality' := _}}
def
category_theory.over.forget_colimit_is_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.over X)
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)] :
@[instance]
def
category_theory.over.category_theory.limits.reflects_colimits
{C : Type u}
[category_theory.category C]
{X : C} :
Equations
- category_theory.over.category_theory.limits.reflects_colimits = {reflects_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_colimit := λ (F : J ⥤ category_theory.over X), {reflects := λ (t : category_theory.limits.cocone F) (ht : category_theory.limits.is_colimit (category_theory.over.forget.map_cocone t)), {desc := λ (s : category_theory.limits.cocone F), category_theory.over.hom_mk (ht.desc (category_theory.over.forget.map_cocone s)) _, fac' := _, uniq' := _}}}}
@[instance]
def
category_theory.over.has_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
{F : J ⥤ category_theory.over X}
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)] :
@[instance]
def
category_theory.over.has_colimits_of_shape
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_colimits_of_shape J C] :
Equations
@[instance]
def
category_theory.over.has_colimits
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_colimits C] :
Equations
- category_theory.over.has_colimits = {has_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), category_theory.over.has_colimits_of_shape}
@[instance]
def
category_theory.over.forget_preserves_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
{F : J ⥤ category_theory.over X}
[category_theory.limits.has_colimit (F ⋙ category_theory.over.forget)] :
@[instance]
def
category_theory.over.forget_preserves_colimits_of_shape
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
{X : C} :
@[instance]
def
category_theory.over.forget_preserves_colimits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : C} :
Equations
@[simp]
theorem
category_theory.under.limit_π_app
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
[category_theory.limits.has_limit (F ⋙ category_theory.under.forget)]
(j : J) :
@[simp]
theorem
category_theory.under.limit_X
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
[category_theory.limits.has_limit (F ⋙ category_theory.under.forget)] :
def
category_theory.under.limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
[category_theory.limits.has_limit (F ⋙ category_theory.under.forget)] :
Equations
- category_theory.under.limit F = {X := category_theory.under.mk (category_theory.limits.limit.lift (F ⋙ category_theory.under.forget) F.to_cone), π := {app := λ (j : J), category_theory.under.hom_mk (category_theory.limits.limit.π (F ⋙ category_theory.under.forget) j) _, naturality' := _}}
def
category_theory.under.forget_limit_is_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
(F : J ⥤ category_theory.under X)
[category_theory.limits.has_limit (F ⋙ category_theory.under.forget)] :
@[instance]
def
category_theory.under.category_theory.limits.reflects_limits
{C : Type u}
[category_theory.category C]
{X : C} :
Equations
- category_theory.under.category_theory.limits.reflects_limits = {reflects_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_limit := λ (F : J ⥤ category_theory.under X), {reflects := λ (t : category_theory.limits.cone F) (ht : category_theory.limits.is_limit (category_theory.under.forget.map_cone t)), {lift := λ (s : category_theory.limits.cone F), category_theory.under.hom_mk (ht.lift (category_theory.under.forget.map_cone s)) _, fac' := _, uniq' := _}}}}
@[instance]
def
category_theory.under.has_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
{F : J ⥤ category_theory.under X}
[category_theory.limits.has_limit (F ⋙ category_theory.under.forget)] :
@[instance]
def
category_theory.under.has_limits_of_shape
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_limits_of_shape J C] :
Equations
@[instance]
def
category_theory.under.has_limits
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_limits C] :
Equations
- category_theory.under.has_limits = {has_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), category_theory.under.has_limits_of_shape}
@[instance]
def
category_theory.under.forget_preserves_limits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
{X : C} :
Equations
- category_theory.under.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ category_theory.under X), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.under.forget_limit_is_limit F)}}