@[class]
structure
category_theory.limits.has_finite_products
(C : Type u)
[category_theory.category C] :
Prop
- out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.discrete J) C
A category has finite products if there is a chosen limit for every diagram
with shape discrete J
, where we have [decidable_eq J]
and [fintype J]
.
@[instance]
def
category_theory.limits.has_limits_of_shape_discrete
(C : Type u)
[category_theory.category C]
(J : Type v)
[fintype J]
[category_theory.limits.has_finite_products C] :
theorem
category_theory.limits.has_finite_products_of_has_finite_limits
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_finite_limits C] :
If C
has finite limits then it has finite products.
theorem
category_theory.limits.has_finite_products_of_has_products
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_products C] :
If a category has all products then in particular it has finite products.
@[class]
structure
category_theory.limits.has_finite_coproducts
(C : Type u)
[category_theory.category C] :
Prop
- out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C
A category has finite coproducts if there is a chosen colimit for every diagram
with shape discrete J
, where we have [decidable_eq J]
and [fintype J]
.
@[instance]
def
category_theory.limits.has_colimits_of_shape_discrete
(C : Type u)
[category_theory.category C]
(J : Type v)
[fintype J]
[category_theory.limits.has_finite_coproducts C] :
theorem
category_theory.limits.has_finite_coproducts_of_has_finite_colimits
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_finite_colimits C] :
If C
has finite colimits then it has finite coproducts.
theorem
category_theory.limits.has_finite_coproducts_of_has_coproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_coproducts C] :
If a category has all coproducts then in particular it has finite coproducts.