Possession of filtered colimits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[class]
structure
category_theory.limits.has_cofiltered_limits_of_size
(C : Type u)
[category_theory.category C] :
Prop
- has_limits_of_shape : ∀ (I : Type ?) [_inst_2 : category_theory.category I] [_inst_3 : category_theory.is_cofiltered I], category_theory.limits.has_limits_of_shape I C
Class for having all cofiltered limits of a given size.
Instances of this typeclass
@[class]
structure
category_theory.limits.has_filtered_colimits_of_size
(C : Type u)
[category_theory.category C] :
Prop
- has_colimits_of_shape : ∀ (I : Type ?) [_inst_2 : category_theory.category I] [_inst_3 : category_theory.is_filtered I], category_theory.limits.has_colimits_of_shape I C
Class for having all filtered colimits of a given size.
Instances of this typeclass
@[protected, instance]
@[protected, instance]