Limits over essentially small indexing categories #
If C
has limits of size w
and J
is w
-essentially small, then C
has limits of shape J
.
See also the file FinallySmall.lean
for more general results.
theorem
CategoryTheory.Limits.hasLimitsOfShape_of_essentiallySmall
(J : Type u₂)
[Category J]
(C : Type u₁)
[Category C]
[EssentiallySmall J]
[HasLimitsOfSize C]
:
HasLimitsOfShape J C
theorem
CategoryTheory.Limits.hasColimitsOfShape_of_essentiallySmall
(J : Type u₂)
[Category J]
(C : Type u₁)
[Category C]
[EssentiallySmall J]
[HasColimitsOfSize C]
:
theorem
CategoryTheory.Limits.hasProductsOfShape_of_small
(C : Type u₁)
[Category C]
(β : Type w₂)
[Small β]
[HasProducts C]
:
theorem
CategoryTheory.Limits.hasCoproductsOfShape_of_small
(C : Type u₁)
[Category C]
(β : Type w₂)
[Small β]
[HasCoproducts C]
: