@[simp]
theorem
category_theory.limits.limit.lift_π_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(H : J ⥤ K ⥤ C)
[category_theory.limits.has_limit H]
(c : category_theory.limits.cone H)
(j : J)
(k : K) :
(category_theory.limits.limit.lift H c).app k ≫ (category_theory.limits.limit.π H j).app k = (c.π.app j).app k
@[simp]
theorem
category_theory.limits.limit.lift_π_app_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(H : J ⥤ K ⥤ C)
[category_theory.limits.has_limit H]
(c : category_theory.limits.cone H)
(j : J)
(k : K)
{X' : C}
(f' : (H.obj j).obj k ⟶ X') :
@[simp]
theorem
category_theory.limits.colimit.ι_desc_app_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(H : J ⥤ K ⥤ C)
[category_theory.limits.has_colimit H]
(c : category_theory.limits.cocone H)
(j : J)
(k : K)
{X' : C}
(f' : c.X.obj k ⟶ X') :
@[simp]
theorem
category_theory.limits.colimit.ι_desc_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(H : J ⥤ K ⥤ C)
[category_theory.limits.has_colimit H]
(c : category_theory.limits.cocone H)
(j : J)
(k : K) :
(category_theory.limits.colimit.ι H j).app k ≫ (category_theory.limits.colimit.desc H c).app k = (c.ι.app j).app k
def
category_theory.limits.evaluation_jointly_reflects_limits
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
{F : J ⥤ K ⥤ C}
(c : category_theory.limits.cone F)
(t : Π (k : K), category_theory.limits.is_limit (((category_theory.evaluation K C).obj k).map_cone c)) :
The evaluation functors jointly reflect limits: that is, to show a cone is a limit of F
it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is
limiting you can show it's pointwise limiting.
Equations
- category_theory.limits.evaluation_jointly_reflects_limits c t = {lift := λ (s : category_theory.limits.cone F), {app := λ (k : K), (t k).lift {X := s.X.obj k, π := category_theory.whisker_right s.π ((category_theory.evaluation K C).obj k)}, naturality' := _}, fac' := _, uniq' := _}
def
category_theory.limits.combine_cones
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k)) :
Given a functor F and a collection of limit cones for each diagram X ↦ F X k, we can stitch
them together to give a cone for the diagram F.
combined_is_limit shows that the new cone is limiting, and eval_combined shows it is
(essentially) made up of the original cones.
Equations
- category_theory.limits.combine_cones F c = {X := {obj := λ (k : K), (c k).cone.X, map := λ (k₁ k₂ : K) (f : k₁ ⟶ k₂), (c k₂).is_limit.lift {X := (c k₁).cone.X, π := (c k₁).cone.π ≫ F.flip.map f}, map_id' := _, map_comp' := _}, π := {app := λ (j : J), {app := λ (k : K), (c k).cone.π.app j, naturality' := _}, naturality' := _}}
@[simp]
theorem
category_theory.limits.combine_cones_X_obj
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k))
(k : K) :
@[simp]
theorem
category_theory.limits.combine_cones_π_app_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k))
(j : J)
(k : K) :
@[simp]
theorem
category_theory.limits.combine_cones_X_map
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k))
(k₁ k₂ : K)
(f : k₁ ⟶ k₂) :
def
category_theory.limits.evaluate_combined_cones
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k))
(k : K) :
((category_theory.evaluation K C).obj k).map_cone (category_theory.limits.combine_cones F c) ≅ (c k).cone
The stitched together cones each project down to the original given cones (up to iso).
Equations
def
category_theory.limits.combined_is_limit
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.limit_cone (F.flip.obj k)) :
Stitching together limiting cones gives a limiting cone.
Equations
def
category_theory.limits.evaluation_jointly_reflects_colimits
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
{F : J ⥤ K ⥤ C}
(c : category_theory.limits.cocone F)
(t : Π (k : K), category_theory.limits.is_colimit (((category_theory.evaluation K C).obj k).map_cocone c)) :
The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of F
it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is
colimiting you can show it's pointwise colimiting.
Equations
- category_theory.limits.evaluation_jointly_reflects_colimits c t = {desc := λ (s : category_theory.limits.cocone F), {app := λ (k : K), (t k).desc {X := s.X.obj k, ι := category_theory.whisker_right s.ι ((category_theory.evaluation K C).obj k)}, naturality' := _}, fac' := _, uniq' := _}
def
category_theory.limits.combine_cocones
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k)) :
Given a functor F and a collection of colimit cocones for each diagram X ↦ F X k, we can stitch
them together to give a cocone for the diagram F.
combined_is_colimit shows that the new cocone is colimiting, and eval_combined shows it is
(essentially) made up of the original cocones.
Equations
- category_theory.limits.combine_cocones F c = {X := {obj := λ (k : K), (c k).cocone.X, map := λ (k₁ k₂ : K) (f : k₁ ⟶ k₂), (c k₁).is_colimit.desc {X := (c k₂).cocone.X, ι := F.flip.map f ≫ (c k₂).cocone.ι}, map_id' := _, map_comp' := _}, ι := {app := λ (j : J), {app := λ (k : K), (c k).cocone.ι.app j, naturality' := _}, naturality' := _}}
@[simp]
theorem
category_theory.limits.combine_cocones_X_obj
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k))
(k : K) :
@[simp]
theorem
category_theory.limits.combine_cocones_X_map
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k))
(k₁ k₂ : K)
(f : k₁ ⟶ k₂) :
@[simp]
theorem
category_theory.limits.combine_cocones_ι_app_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k))
(j : J)
(k : K) :
def
category_theory.limits.evaluate_combined_cocones
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k))
(k : K) :
((category_theory.evaluation K C).obj k).map_cocone (category_theory.limits.combine_cocones F c) ≅ (c k).cocone
The stitched together cocones each project down to the original given cocones (up to iso).
def
category_theory.limits.combined_is_colimit
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
(F : J ⥤ K ⥤ C)
(c : Π (k : K), category_theory.limits.colimit_cocone (F.flip.obj k)) :
Stitching together colimiting cocones gives a colimiting cocone.
Equations
@[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.category K]
[category_theory.limits.has_limits_of_shape J C] :
@[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.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.category K]
[category_theory.limits.has_limits C] :
@[instance]
def
category_theory.limits.functor_category_has_colimits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.category K]
[category_theory.limits.has_colimits C] :
@[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.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.combined_is_limit F (λ (k : K), category_theory.limits.get_limit_cone (F ⋙ (category_theory.evaluation K C).obj k))) ((category_theory.limits.limit.is_limit (F ⋙ (category_theory.evaluation K C).obj k)).of_iso_limit (category_theory.limits.evaluate_combined_cones F (λ (k : K), category_theory.limits.get_limit_cone (F ⋙ (category_theory.evaluation K C).obj k)) k).symm)}
def
category_theory.limits.limit_obj_iso_limit_comp_evaluation
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(k : K) :
(category_theory.limits.limit F).obj k ≅ category_theory.limits.limit (F ⋙ (category_theory.evaluation K C).obj k)
If F : J ⥤ K ⥤ C is a functor into a functor category which has a limit,
then the evaluation of that limit at k is the limit of the evaluations of F.obj j at k.
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_hom_π_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K)
{X' : C}
(f' : (F ⋙ (category_theory.evaluation K C).obj k).obj j ⟶ X') :
(category_theory.limits.limit_obj_iso_limit_comp_evaluation F k).hom ≫ category_theory.limits.limit.π (F ⋙ (category_theory.evaluation K C).obj k) j ≫ f' = (category_theory.limits.limit.π F j).app k ≫ f'
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_hom_π
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K)
{X' : C}
(f' : (F.obj j).obj k ⟶ X') :
(category_theory.limits.limit_obj_iso_limit_comp_evaluation F k).inv ≫ (category_theory.limits.limit.π F j).app k ≫ f' = category_theory.limits.limit.π (F ⋙ (category_theory.evaluation K C).obj k) j ≫ f'
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_π_app
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
@[ext]
theorem
category_theory.limits.limit_obj_ext
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
{H : J ⥤ K ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{k : K}
{W : C}
{f g : W ⟶ (category_theory.limits.limit H).obj k}
(w : ∀ (j : J), f ≫ (category_theory.limits.limit.π H j).app k = g ≫ (category_theory.limits.limit.π H j).app k) :
f = g
@[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.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.combined_is_colimit F (λ (k : K), category_theory.limits.get_colimit_cocone (F ⋙ (category_theory.evaluation K C).obj k))) ((category_theory.limits.colimit.is_colimit (F ⋙ (category_theory.evaluation K C).obj k)).of_iso_colimit (category_theory.limits.evaluate_combined_cocones F (λ (k : K), category_theory.limits.get_colimit_cocone (F ⋙ (category_theory.evaluation K C).obj k)) k).symm)}
def
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(k : K) :
(category_theory.limits.colimit F).obj k ≅ category_theory.limits.colimit (F ⋙ (category_theory.evaluation K C).obj k)
If F : J ⥤ K ⥤ C is a functor into a functor category which has a colimit,
then the evaluation of that colimit at k is the colimit of the evaluations of F.obj j at k.
@[simp]
theorem
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_inv_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K)
{X' : C}
(f' : (category_theory.limits.colimit F).obj k ⟶ X') :
category_theory.limits.colimit.ι (F ⋙ (category_theory.evaluation K C).obj k) j ≫ (category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F k).inv ≫ f' = (category_theory.limits.colimit.ι F j).app k ≫ f'
@[simp]
theorem
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_inv
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
@[simp]
theorem
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_app_hom_assoc
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K)
{X' : C}
(f' : category_theory.limits.colimit (F ⋙ (category_theory.evaluation K C).obj k) ⟶ X') :
(category_theory.limits.colimit.ι F j).app k ≫ (category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F k).hom ≫ f' = category_theory.limits.colimit.ι (F ⋙ (category_theory.evaluation K C).obj k) j ≫ f'
@[simp]
theorem
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_ι_app_hom
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(j : J)
(k : K) :
@[ext]
theorem
category_theory.limits.colimit_obj_ext
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.category K]
{H : J ⥤ K ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{k : K}
{W : C}
{f g : (category_theory.limits.colimit H).obj k ⟶ W}
(w : ∀ (j : J), (category_theory.limits.colimit.ι H j).app k ≫ f = (category_theory.limits.colimit.ι H j).app k ≫ g) :
f = g
@[instance]
def
category_theory.limits.evaluation_preserves_limits
{C : Type u}
[category_theory.category C]
{K : Type v}
[category_theory.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.category K]
[category_theory.limits.has_colimits C]
(k : K) :