(Co)limits in functor categories. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We show that if D has limits, then the functor category C ⥤ D also has limits
(category_theory.limits.functor_category_has_limits),
and the evaluation functors preserve limits
(category_theory.limits.evaluation_preserves_limits)
(and similarly for colimits).
We also show that F : D ⥤ K ⥤ C preserves (co)limits if it does so for each k : K
(category_theory.limits.preserves_limits_of_evaluation and
category_theory.limits.preserves_colimits_of_evaluation).
@[simp]
theorem
category_theory.limits.limit.lift_π_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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
@[protected, instance]
def
category_theory.limits.functor_category_has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C] :
@[protected, instance]
def
category_theory.limits.functor_category_has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.limits.evaluation_preserves_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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)}
noncomputable
def
category_theory.limits.limit_obj_iso_limit_comp_evaluation
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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_map_limit_obj_iso_limit_comp_evaluation_hom_assoc
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
{i j : K}
(F : J ⥤ K ⥤ C)
(f : i ⟶ j)
{X' : C}
(f' : category_theory.limits.limit (F ⋙ (category_theory.evaluation K C).obj j) ⟶ X') :
@[simp]
theorem
category_theory.limits.limit_map_limit_obj_iso_limit_comp_evaluation_hom
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
{i j : K}
(F : J ⥤ K ⥤ C)
(f : i ⟶ j) :
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_limit_map
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
{i j : K}
(F : J ⥤ K ⥤ C)
(f : i ⟶ j) :
@[simp]
theorem
category_theory.limits.limit_obj_iso_limit_comp_evaluation_inv_limit_map_assoc
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
{i j : K}
(F : J ⥤ K ⥤ C)
(f : i ⟶ j)
{X' : C}
(f' : (category_theory.limits.limit F).obj j ⟶ X') :
@[ext]
theorem
category_theory.limits.limit_obj_ext
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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
@[protected, instance]
noncomputable
def
category_theory.limits.evaluation_preserves_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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)}
noncomputable
def
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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_inv_colimit_map
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
{i j : K}
(f : i ⟶ j) :
@[simp]
theorem
category_theory.limits.colimit_obj_iso_colimit_comp_evaluation_inv_colimit_map_assoc
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
{i j : K}
(f : i ⟶ j)
{X' : C}
(f' : (category_theory.limits.colimit F).obj j ⟶ X') :
(category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F i).inv ≫ (category_theory.limits.colimit F).map f ≫ f' = category_theory.limits.colim_map (category_theory.whisker_left F ((category_theory.evaluation K C).map f)) ≫ (category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F j).inv ≫ f'
@[simp]
theorem
category_theory.limits.colimit_map_colimit_obj_iso_colimit_comp_evaluation_hom
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
{i j : K}
(f : i ⟶ j) :
@[simp]
theorem
category_theory.limits.colimit_map_colimit_obj_iso_colimit_comp_evaluation_hom_assoc
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
{i j : K}
(f : i ⟶ j)
{X' : C}
(f' : category_theory.limits.colimit (F ⋙ (category_theory.evaluation K C).obj j) ⟶ X') :
(category_theory.limits.colimit F).map f ≫ (category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F j).hom ≫ f' = (category_theory.limits.colimit_obj_iso_colimit_comp_evaluation F i).hom ≫ category_theory.limits.colim_map (category_theory.whisker_left F ((category_theory.evaluation K C).map f)) ≫ f'
@[ext]
theorem
category_theory.limits.colimit_obj_ext
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[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
@[protected, instance]
noncomputable
def
category_theory.limits.evaluation_preserves_limits
{C : Type u}
[category_theory.category C]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits C]
(k : K) :
Equations
def
category_theory.limits.preserves_limit_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(G : J ⥤ D)
(H : Π (k : K), category_theory.limits.preserves_limit G (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves the limit of some G : J ⥤ D if it does for each k : K.
Equations
- category_theory.limits.preserves_limit_of_evaluation F G H = {preserves := λ (c : category_theory.limits.cone G) (hc : category_theory.limits.is_limit c), category_theory.limits.evaluation_jointly_reflects_limits (F.map_cone c) (λ (X : K), id (category_theory.limits.preserves_limit.preserves hc))}
def
category_theory.limits.preserves_limits_of_shape_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(J : Type u_1)
[category_theory.category J]
(H : Π (k : K), category_theory.limits.preserves_limits_of_shape J (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves limits of shape J if it does for each k : K.
Equations
def
category_theory.limits.preserves_limits_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(H : Π (k : K), category_theory.limits.preserves_limits_of_size (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves all limits if it does for each k : K.
Equations
@[protected, instance]
def
category_theory.limits.preserves_limits_const
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D] :
The constant functor C ⥤ (D ⥤ C) preserves limits.
@[protected, instance]
noncomputable
def
category_theory.limits.evaluation_preserves_colimits
{C : Type u}
[category_theory.category C]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits C]
(k : K) :
def
category_theory.limits.preserves_colimit_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(G : J ⥤ D)
(H : Π (k : K), category_theory.limits.preserves_colimit G (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves the colimit of some G : J ⥤ D if it does for each k : K.
Equations
- category_theory.limits.preserves_colimit_of_evaluation F G H = {preserves := λ (c : category_theory.limits.cocone G) (hc : category_theory.limits.is_colimit c), category_theory.limits.evaluation_jointly_reflects_colimits (F.map_cocone c) (λ (X : K), id (category_theory.limits.preserves_colimit.preserves hc))}
def
category_theory.limits.preserves_colimits_of_shape_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(J : Type u_1)
[category_theory.category J]
(H : Π (k : K), category_theory.limits.preserves_colimits_of_shape J (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves all colimits of shape J if it does for each k : K.
Equations
def
category_theory.limits.preserves_colimits_of_evaluation
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{K : Type u₂}
[category_theory.category K]
(F : D ⥤ K ⥤ C)
(H : Π (k : K), category_theory.limits.preserves_colimits_of_size (F ⋙ (category_theory.evaluation K C).obj k)) :
F : D ⥤ K ⥤ C preserves all colimits if it does for each k : K.
Equations
- category_theory.limits.preserves_colimits_of_evaluation F H = {preserves_colimits_of_shape := λ (L : Type w) (hL : category_theory.category L), category_theory.limits.preserves_colimits_of_shape_of_evaluation F L (λ (k : K), category_theory.limits.preserves_colimits_of_size.preserves_colimits_of_shape)}
@[protected, instance]
def
category_theory.limits.preserves_colimits_const
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D] :
The constant functor C ⥤ (D ⥤ C) preserves colimits.
@[simp]
theorem
category_theory.limits.limit_iso_flip_comp_lim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.limit_iso_flip_comp_lim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C) :
The limit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by
the individual limits on objects.
@[simp]
theorem
category_theory.limits.limit_iso_flip_comp_lim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ K ⥤ C)
(X : K) :
@[simp]
theorem
category_theory.limits.limit_flip_iso_comp_lim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : K ⥤ J ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.limit_flip_iso_comp_lim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : K ⥤ J ⥤ C) :
A variant of limit_iso_flip_comp_lim where the arguemnts of F are flipped.
@[simp]
theorem
category_theory.limits.limit_flip_iso_comp_lim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(F : K ⥤ J ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.limit_iso_swap_comp_lim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(G : J ⥤ K ⥤ C) :
For a functor G : J ⥤ K ⥤ C, its limit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ lim.
Note that this does not require K to be small.
@[simp]
theorem
category_theory.limits.limit_iso_swap_comp_lim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(G : J ⥤ K ⥤ C)
(X : K) :
@[simp]
theorem
category_theory.limits.limit_iso_swap_comp_lim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_limits_of_shape J C]
(G : J ⥤ K ⥤ C)
(X : K) :
@[simp]
theorem
category_theory.limits.colimit_iso_flip_comp_colim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(X : K) :
@[simp]
theorem
category_theory.limits.colimit_iso_flip_comp_colim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.colimit_iso_flip_comp_colim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ K ⥤ C) :
The colimit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by
the individual colimits on objects.
@[simp]
theorem
category_theory.limits.colimit_flip_iso_comp_colim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : K ⥤ J ⥤ C)
(X : K) :
@[simp]
theorem
category_theory.limits.colimit_flip_iso_comp_colim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : K ⥤ J ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.colimit_flip_iso_comp_colim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(F : K ⥤ J ⥤ C) :
A variant of colimit_iso_flip_comp_colim where the arguemnts of F are flipped.
@[simp]
theorem
category_theory.limits.colimit_iso_swap_comp_colim_hom_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(G : J ⥤ K ⥤ C)
(X : K) :
noncomputable
def
category_theory.limits.colimit_iso_swap_comp_colim
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(G : J ⥤ K ⥤ C) :
For a functor G : J ⥤ K ⥤ C, its colimit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ colim.
Note that this does not require K to be small.
@[simp]
theorem
category_theory.limits.colimit_iso_swap_comp_colim_inv_app
{C : Type u}
[category_theory.category C]
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
[category_theory.limits.has_colimits_of_shape J C]
(G : J ⥤ K ⥤ C)
(X : K) :