mathlib3 documentation

category_theory.limits.essentially_small

Limits over essentially small indexing categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If C has limits of size w and J is w-essentially small, then C has limits of shape J.

source
theorem category_theory.limits.has_limits_of_shape_of_essentially_small (J : Type u₂) [category_theory.category J] (C : Type u₁) [category_theory.category C] [category_theory.essentially_small J] [category_theory.limits.has_limits_of_size C] :
category_theory.limits.has_limits_of_shape J C
source
theorem category_theory.limits.has_colimits_of_shape_of_essentially_small (J : Type u₂) [category_theory.category J] (C : Type u₁) [category_theory.category C] [category_theory.essentially_small J] [category_theory.limits.has_colimits_of_size C] :
category_theory.limits.has_colimits_of_shape J C
source
theorem category_theory.limits.has_products_of_shape_of_small (C : Type u₁) [category_theory.category C] (β : Type w₂) [small β] [category_theory.limits.has_products C] :
category_theory.limits.has_products_of_shape β C
source
theorem category_theory.limits.has_coproducts_of_shape_of_small (C : Type u₁) [category_theory.category C] (β : Type w₂) [small β] [category_theory.limits.has_coproducts C] :
category_theory.limits.has_coproducts_of_shape β C