mathlibdocumentation

category_theory.limits.shapes.finite_products

Categories with finite (co)products #

Typeclasses representing categories with (co)products over finite indexing types.

@[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
@[protected, instance]
@[protected, instance]

If C has finite limits then it has finite products.

@[protected, instance]
def category_theory.limits.has_fintype_products (C : Type u) (ι : Type w) [fintype ι] :

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
@[protected, instance]
@[protected, instance]

If C has finite colimits then it has finite coproducts.

@[protected, instance]
def category_theory.limits.has_fintype_coproducts (C : Type u) (ι : Type w) [fintype ι] :

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