@[simp]
theorem
category_theory.limits.cone.functor_w
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{F : J ⥤ K ⥤ C}
(c : category_theory.limits.cone F)
{j j' : J}
(f : j ⟶ j')
(k : K) :
@[simp]
theorem
category_theory.limits.cocone.functor_w
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{F : J ⥤ K ⥤ C}
(c : category_theory.limits.cocone F)
{j j' : J}
(f : j ⟶ j')
(k : K) :
@[simp]
theorem
category_theory.limits.functor_category_limit_cone_X
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C) :
@[simp]
theorem
category_theory.limits.functor_category_limit_cone_π_app_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
((category_theory.limits.functor_category_limit_cone F).π.app j).app k = category_theory.limits.limit.π (F.flip.obj k) j
def
category_theory.limits.functor_category_limit_cone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C) :
Equations
- category_theory.limits.functor_category_limit_cone F = {X := F.flip ⋙ category_theory.limits.lim, π := {app := λ (j : J), {app := λ (k : K), category_theory.limits.limit.π (F.flip.obj k) j, naturality' := _}, naturality' := _}}
@[simp]
theorem
category_theory.limits.functor_category_colimit_cocone_ι_app_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
def
category_theory.limits.functor_category_colimit_cocone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C) :
Equations
- category_theory.limits.functor_category_colimit_cocone F = {X := F.flip ⋙ category_theory.limits.colim, ι := {app := λ (j : J), {app := λ (k : K), category_theory.limits.colimit.ι (F.flip.obj k) j, naturality' := _}, naturality' := _}}
@[simp]
theorem
category_theory.limits.functor_category_colimit_cocone_X
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C) :
@[simp]
def
category_theory.limits.evaluate_functor_category_limit_cone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(k : K) :
@[simp]
def
category_theory.limits.evaluate_functor_category_colimit_cocone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(k : K) :
def
category_theory.limits.functor_category_is_limit_cone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C) :
Equations
- category_theory.limits.functor_category_is_limit_cone F = {lift := λ (s : category_theory.limits.cone F), {app := λ (k : K), category_theory.limits.limit.lift (F.flip.obj k) (((category_theory.evaluation K C).obj k).map_cone s), naturality' := _}, fac' := _, uniq' := _}
def
category_theory.limits.functor_category_is_colimit_cocone
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C) :
Equations
- category_theory.limits.functor_category_is_colimit_cocone F = {desc := λ (s : category_theory.limits.cocone F), {app := λ (k : K), category_theory.limits.colimit.desc (F.flip.obj k) (((category_theory.evaluation K C).obj k).map_cocone s), naturality' := _}, fac' := _, uniq' := _}
@[instance]
def
category_theory.limits.functor_category_has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C] :
Equations
@[instance]
def
category_theory.limits.functor_category_has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C] :
@[instance]
def
category_theory.limits.functor_category_has_limits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.small_category K]
[category_theory.limits.has_limits C] :
Equations
@[instance]
def
category_theory.limits.functor_category_has_colimits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.small_category K]
[category_theory.limits.has_colimits C] :
Equations
@[instance]
def
category_theory.limits.evaluation_preserves_limits_of_shape
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_limits_of_shape J C]
(k : K) :
Equations
- category_theory.limits.evaluation_preserves_limits_of_shape k = {preserves_limit := λ (F : J ⥤ K ⥤ C), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) ((category_theory.limits.limit.is_limit (F ⋙ (category_theory.evaluation K C).obj k)).of_iso_limit (category_theory.limits.evaluate_functor_category_limit_cone F k).symm)}
@[instance]
def
category_theory.limits.evaluation_preserves_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.limits.has_colimits_of_shape J C]
(k : K) :
Equations
- category_theory.limits.evaluation_preserves_colimits_of_shape k = {preserves_colimit := λ (F : J ⥤ K ⥤ C), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.colimit.is_colimit F) ((category_theory.limits.colimit.is_colimit (F ⋙ (category_theory.evaluation K C).obj k)).of_iso_colimit (category_theory.limits.evaluate_functor_category_colimit_cocone F k).symm)}
@[instance]
def
category_theory.limits.evaluation_preserves_limits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.small_category K]
[category_theory.limits.has_limits C]
(k : K) :
Equations
@[instance]
def
category_theory.limits.evaluation_preserves_colimits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.small_category K]
[category_theory.limits.has_colimits C]
(k : K) :