CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape
theorem CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w)
[inst_1 : CategoryTheory.Category.{w', w} I] [inst_2 : CategoryTheory.IsCofiltered I],
CategoryTheory.Limits.HasLimitsOfShape I C
This theorem states that for any filtered category `C` of type `u` and given an arbitrary type `I` of size `w`, if `C` has cofiltered limits of size `w`, then `C` also has limits of shape `I`. Here, the size and shape of limits refers to the category of diagrams over which the limit is taken.
More concisely: If `C` is a filtered category of type `u` with cofiltered limits of size `w`, then `C` has limits of shape any type `I` of size `w`.
|
CategoryTheory.Limits.HasFilteredColimitsOfSize.HasColimitsOfShape
theorem CategoryTheory.Limits.HasFilteredColimitsOfSize.HasColimitsOfShape :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] (I : Type w)
[inst_1 : CategoryTheory.Category.{w', w} I] [inst_2 : CategoryTheory.IsFiltered I],
CategoryTheory.Limits.HasColimitsOfShape I C
The theorem states that for any filtered type of a specific size `w`, there exist colimits in the category `C`. More formally, given a type `C` that is also a category and has filtered colimits of a certain size, and given another type `I` that is also a category and is filtered, `C` has colimits of the shape `I`. This means that for any diagram in `C` indexed by `I`, there exists a colimit cocone for that diagram.
More concisely: For any filtered category `C` of size `w` and any filtered index category `I`, `C` has filtered colimits indexed by `I`.
|