mathlib documentation

category_theory.limits.shapes.finite_products

Categories with finite (co)products #

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

source
@[class]
structure category_theory.limits.has_finite_products (C : Type u) [category_theory.category C] :
Prop

A category has finite products if there is a chosen limit for every diagram with shape discrete J, where we have [finite J].

We require this condition only for J = fin n in the definition, then deduce a version for any J : Type* as a corollary of this definition.

Instances of this typeclass
source
@[protected, instance]
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] :
category_theory.limits.has_finite_products C

If C has finite limits then it has finite products.

source
@[protected, instance]
def category_theory.limits.has_limits_of_shape_discrete (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_products C] (ι : Type w) [finite ι] :
category_theory.limits.has_limits_of_shape (category_theory.discrete ι) C
source
theorem category_theory.limits.has_finite_products_of_has_products (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] :
category_theory.limits.has_finite_products C

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

source
@[class]
structure category_theory.limits.has_finite_coproducts (C : Type u) [category_theory.category C] :
Prop

A category has finite coproducts if there is a chosen colimit for every diagram with shape discrete J, where we have [fintype J].

We require this condition only for J = fin n in the definition, then deduce a version for any J : Type* as a corollary of this definition.

Instances of this typeclass
source
@[protected, instance]
def category_theory.limits.has_colimits_of_shape_discrete (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_coproducts C] (ι : Type w) [finite ι] :
category_theory.limits.has_colimits_of_shape (category_theory.discrete ι) C
source
@[protected, instance]
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] :
category_theory.limits.has_finite_coproducts C

If C has finite colimits then it has finite coproducts.

source
theorem category_theory.limits.has_finite_coproducts_of_has_coproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_coproducts C] :
category_theory.limits.has_finite_coproducts C

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