mathlibdocumentation

category_theory.limits.shapes.finite_products

@[class]
def category_theory.limits.has_finite_products (C : Type u)  :
Prop

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
• = ∀ (J : Type v) [_inst_2 : [_inst_3 : fintype J],
Instances
@[instance]

If C has finite limits then it has finite products.

If a category has all products then in particular it has finite products.

@[class]

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
• = ∀ (J : Type v) [_inst_2 : [_inst_3 : fintype J],
Instances
@[instance]

If C has finite colimits then it has finite coproducts.

If a category has all coproducts then in particular it has finite coproducts.