Documentation

Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

Categories with finite (co)products #

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

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.

Instances
    @[instance 10]

    If C has finite limits then it has finite products.

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

    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.

    Instances
      @[instance 10]

      If C has finite colimits then it has finite coproducts.

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