# mathlibdocumentation

category_theory.limits.shapes.finite_products

@[class]
structure category_theory.limits.has_finite_products (C : Type u)  :
Prop
• out : ∀ (J : Type ?) [_inst_2 : [_inst_3 : fintype J],

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].

Instances
@[instance]
@[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]
structure category_theory.limits.has_finite_coproducts (C : Type u)  :
Prop
• out : ∀ (J : Type ?) [_inst_2 : [_inst_3 : fintype J],

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].

Instances
@[instance]
@[instance]

If C has finite colimits then it has finite coproducts.

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