CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval
theorem CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval :
∀ {I : Type v₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁}
[inst_1 : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)}
[inst_2 : ∀ (i : I), CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Pi.eval C i))],
CategoryTheory.Limits.HasColimit F
This theorem establishes a condition under which a colimit exists for a functor `F` into a category of indexed families. Specifically, it states that if we have a functor `F : J ⥤ Π i, C i` from a small category `J` to a category of indexed families `C i`, indexed over `I`, and if colimits exist for each of the functors obtained by composing `F` with the evaluation functor at each index `i`, i.e., `F ⋙ Pi.eval C i`, then a colimit exists for `F`. In more intuitive terms, if we can find colimits for every 'slice' of the family (viewed by evaluating at each index), then we can find a colimit for the whole family.
More concisely: If a functor from a small category to the category of indexed families preserves all index-wise colimits, then it admits a colimit.
|
CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval
theorem CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval :
∀ {I : Type v₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁}
[inst_1 : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)}
[inst_2 : ∀ (i : I), CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Pi.eval C i))],
CategoryTheory.Limits.HasLimit F
This theorem states that if we have a functor `F` from category `J` to a category of `I`-indexed families of objects `C i`, and if each of the functors resulting from the composition of `F` with the evaluation functor at `i` (denoted `F ⋙ Pi.eval C i`) has a limit, then the functor `F` itself has a limit. In other words, if we have limits for each of the projections of `F` onto the individual categories `C i`, then `F` also has a limit in the category of `I`-indexed families.
More concisely: If each evaluation functor of a functor from a category to the category of `I`-indexed families of objects with limits has a limit, then the original functor has a limit in the category of such families.
|