@[class]
def
category_theory.limits.has_finite_products
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u)
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].
Equations
- category_theory.limits.has_finite_products C = Π (J : Type v) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.discrete J) C
@[instance]
def
category_theory.limits.has_limits_of_shape_discrete
(C : Type u)
[category_theory.category C]
(J : Type v)
[decidable_eq J]
[fintype J]
[category_theory.limits.has_finite_products C] :
Equations
- category_theory.limits.has_limits_of_shape_discrete C J = _inst_4 J
def
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.
Equations
- category_theory.limits.has_finite_products_of_has_finite_limits C = λ (J : Type v) (𝒥₁ : decidable_eq J) (𝒥₂ : fintype J), infer_instance
def
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.
Equations
- category_theory.limits.has_finite_products_of_has_products C = id (λ (J : Type v) [_inst_2_1 : decidable_eq J] [_inst_3 : fintype J], _inst_2 J)
@[class]
def
category_theory.limits.has_finite_coproducts
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u)
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].
Equations
- category_theory.limits.has_finite_coproducts C = Π (J : Type v) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C
@[instance]
def
category_theory.limits.has_colimits_of_shape_discrete
(C : Type u)
[category_theory.category C]
(J : Type v)
[decidable_eq J]
[fintype J]
[category_theory.limits.has_finite_coproducts C] :
Equations
- category_theory.limits.has_colimits_of_shape_discrete C J = _inst_4 J
def
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.
Equations
- category_theory.limits.has_finite_coproducts_of_has_finite_colimits C = λ (J : Type v) (𝒥₁ : decidable_eq J) (𝒥₂ : fintype J), infer_instance
def
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.
Equations
- category_theory.limits.has_finite_coproducts_of_has_coproducts C = id (λ (J : Type v) [_inst_2_1 : decidable_eq J] [_inst_3 : fintype J], _inst_2 J)