Categories with finite (co)products

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

class CategoryTheory.Limits.HasFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

A category has finite products if there exists a 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.

• out : ∀ (n : ℕ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete (Fin n)) C

  C has finite products

instance CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteProducts C

If C has finite limits then it has finite products.

Equations

• (_ : CategoryTheory.Limits.HasFiniteProducts C) = (_ : CategoryTheory.Limits.HasFiniteProducts C)

instance CategoryTheory.Limits.hasLimitsOfShape_discrete (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (ι : Type w) [Finite ι] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ι) C

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ι) C) = (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ι) C)

theorem CategoryTheory.Limits.hasFiniteProducts_of_hasProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasFiniteProducts C

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

class CategoryTheory.Limits.HasFiniteCoproducts (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

A category has finite coproducts if there exists a 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.

• out : ∀ (n : ℕ), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C

  C has all finite coproducts

instance CategoryTheory.Limits.hasColimitsOfShape_discrete (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] (ι : Type w) [Finite ι] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C) = (_ : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C)

instance CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteCoproducts C

If C has finite colimits then it has finite coproducts.

Equations

• (_ : CategoryTheory.Limits.HasFiniteCoproducts C) = (_ : CategoryTheory.Limits.HasFiniteCoproducts C)

theorem CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.Limits.HasFiniteCoproducts C

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