Limits in the category of indexed families of objects.

Given a functor F : J ⥤ Π i, C i into a category of indexed families,

1. we can assemble a collection of cones over F ⋙ Pi.eval C i into a cone over F
2. if all those cones are limit cones, the assembled cone is a limit cone, and
3. if we have limits for each of F ⋙ Pi.eval C i, we can produce a HasLimit F instance

def CategoryTheory.pi.coneCompEval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} (c : CategoryTheory.Limits.Cone F) (i : I) : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))

A cone over F : J ⥤ Π i, C i has as its components cones over each of the F ⋙ Pi.eval C i.

Equations

• CategoryTheory.pi.coneCompEval c i = { pt := c.pt i, π := { app := fun (j : J) => c.π.app j i, naturality := ⋯ } }

def CategoryTheory.pi.coconeCompEval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} (c : CategoryTheory.Limits.Cocone F) (i : I) : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))

A cocone over F : J ⥤ Π i, C i has as its components cocones over each of the F ⋙ Pi.eval C i.

Equations

• CategoryTheory.pi.coconeCompEval c i = { pt := c.pt i, ι := { app := fun (j : J) => c.ι.app j i, naturality := ⋯ } }

def CategoryTheory.pi.coneOfConeCompEval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} (c : (i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))) : CategoryTheory.Limits.Cone F

Given a family of cones over the F ⋙ Pi.eval C i, we can assemble these together as a Cone F.

Equations

• CategoryTheory.pi.coneOfConeCompEval c = { pt := fun (i : I) => (c i).pt, π := { app := fun (j : J) (i : I) => (c i).π.app j, naturality := ⋯ } }

def CategoryTheory.pi.coconeOfCoconeCompEval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} (c : (i : I) → CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))) : CategoryTheory.Limits.Cocone F

Given a family of cocones over the F ⋙ Pi.eval C i, we can assemble these together as a Cocone F.

Equations

• CategoryTheory.pi.coconeOfCoconeCompEval c = { pt := fun (i : I) => (c i).pt, ι := { app := fun (j : J) (i : I) => (c i).ι.app j, naturality := ⋯ } }

def CategoryTheory.pi.coneOfConeEvalIsLimit {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} {c : (i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))} (P : (i : I) → CategoryTheory.Limits.IsLimit (c i)) : CategoryTheory.Limits.IsLimit (CategoryTheory.pi.coneOfConeCompEval 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

• CategoryTheory.pi.coneOfConeEvalIsLimit P = { lift := fun (s : CategoryTheory.Limits.Cone F) (i : I) => (P i).lift (CategoryTheory.pi.coneCompEval s i), fac := ⋯, uniq := ⋯ }

def CategoryTheory.pi.coconeOfCoconeEvalIsColimit {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} {c : (i : I) → CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))} (P : (i : I) → CategoryTheory.Limits.IsColimit (c i)) : CategoryTheory.Limits.IsColimit (CategoryTheory.pi.coconeOfCoconeCompEval c)

Given a family of colimit cocones over the F ⋙ Pi.eval C i, assembling them together as a Cocone F produces a colimit cocone.

Equations

• CategoryTheory.pi.coconeOfCoconeEvalIsColimit P = { desc := fun (s : CategoryTheory.Limits.Cocone F) (i : I) => (P i).desc (CategoryTheory.pi.coconeCompEval s i), fac := ⋯, uniq := ⋯ }

theorem CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} [∀ (i : I), CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Pi.eval C i))] : CategoryTheory.Limits.HasLimit F

If we have a functor F : J ⥤ Π i, C i into a category of indexed families, and we have limits for each of the F ⋙ Pi.eval C i, then F has a limit.

theorem CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval {I : Type v₁} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)} [∀ (i : I), CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Pi.eval C i))] : CategoryTheory.Limits.HasColimit F

If we have a functor F : J ⥤ Π i, C i into a category of indexed families, and colimits exist for each of the F ⋙ Pi.eval C i, there is a colimit for F.

As an example, we can use this to construct particular shapes of limits in a category of indexed families.

With the addition of import CategoryTheory.Limits.Shapes.Types we can use:

attribute [local instance] hasLimit_of_hasLimit_comp_eval
example : hasBinaryProducts (I → Type v₁) := ⟨by infer_instance⟩