Limits in the category of indexed families of objects.
Given a functor F : J ⥤ Π i, C i into a category of indexed families,
- we can assemble a collection of cones over
F ⋙ pi.eval C iinto a cone overF - if all those cones are limit cones, the assembled cone is a limit cone, and
- if we have chosen limits for each of
F ⋙ pi.eval C i, we can produce ahas_limit Finstance
def
category_theory.pi.cone_comp_eval
{I : Type v₁}
{C : I → Type u₁}
[Π (i : I), category_theory.category (C i)]
{J : Type v₁}
[category_theory.small_category J]
{F : J ⥤ Π (i : I), C i}
(c : category_theory.limits.cone F)
(i : I) :
A cone over F : J ⥤ Π i, C i has as its components cones over each of the F ⋙ pi.eval C i.
def
category_theory.pi.cone_of_cone_comp_eval
{I : Type v₁}
{C : I → Type u₁}
[Π (i : I), category_theory.category (C i)]
{J : Type v₁}
[category_theory.small_category J]
{F : J ⥤ Π (i : I), C i} :
(Π (i : I), category_theory.limits.cone (F ⋙ category_theory.pi.eval C i)) → category_theory.limits.cone F
Given a family of cones over the F ⋙ pi.eval C i, we can assemble these together as a cone F.
def
category_theory.pi.cone_of_cone_eval_is_limit
{I : Type v₁}
{C : I → Type u₁}
[Π (i : I), category_theory.category (C i)]
{J : Type v₁}
[category_theory.small_category J]
{F : J ⥤ Π (i : I), C i}
{c : Π (i : I), category_theory.limits.cone (F ⋙ category_theory.pi.eval C i)} :
(Π (i : I), category_theory.limits.is_limit (c i)) → category_theory.limits.is_limit (category_theory.pi.cone_of_cone_comp_eval c)
Given a family of limit cones over the F ⋙ pi.eval C i,
assembling them together as a cone F produces a limit cone.
Equations
- category_theory.pi.cone_of_cone_eval_is_limit P = {lift := λ (s : category_theory.limits.cone F) (i : I), (P i).lift (category_theory.pi.cone_comp_eval s i), fac' := _, uniq' := _}
def
category_theory.pi.has_limit_of_has_limit_comp_eval
{I : Type v₁}
{C : I → Type u₁}
[Π (i : I), category_theory.category (C i)]
{J : Type v₁}
[category_theory.small_category J]
{F : J ⥤ Π (i : I), C i}
[Π (i : I), category_theory.limits.has_limit (F ⋙ category_theory.pi.eval C i)] :
If we have a functor F : J ⥤ Π i, C i into a category of indexed families,
and we have chosen limits for each of the F ⋙ pi.eval C i,
there is a canonical choice of chosen limit for F.
Equations
- category_theory.pi.has_limit_of_has_limit_comp_eval = {cone := category_theory.pi.cone_of_cone_comp_eval (λ (i : I), category_theory.limits.limit.cone (F ⋙ category_theory.pi.eval (λ (i : I), C i) i)), is_limit := category_theory.pi.cone_of_cone_eval_is_limit (λ (i : I), category_theory.limits.limit.is_limit (F ⋙ category_theory.pi.eval (λ (i : I), C i) i))}
As an example, we can use this to construct particular shapes of limits in a category of indexed families.
With the addition of
import category_theory.limits.shapes.types
we can use:
local attribute [instance] has_limit_of_has_limit_comp_eval
example : has_binary_products (I → Type v₁) := ⟨by apply_instance⟩