Categories with finite (co)products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Typeclasses representing categories with (co)products over finite indexing types.
- out : ∀ (n : ℕ), category_theory.limits.has_limits_of_shape (category_theory.discrete (fin n)) C
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.
If C
has finite limits then it has finite products.
If a category has all products then in particular it has finite products.
- out : ∀ (n : ℕ), category_theory.limits.has_colimits_of_shape (category_theory.discrete (fin n)) C
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.
If C
has finite colimits then it has finite coproducts.
If a category has all coproducts then in particular it has finite coproducts.