Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

CategoryTheory.Limits.HasFiniteProducts structure

Full source

/-- 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.
-/
class HasFiniteProducts : Prop where
  /-- `C` has finite products -/
  out (n : ℕ) : HasLimitsOfShape (Discrete (Fin n)) C

Category with finite products

Informal description

A category $ C $ has finite products if for every finite indexing type $ J $, there exists a limit for every diagram with shape $ \text{Discrete } J $. In the definition, this condition is only required for $ J = \text{Fin } n $, and the general case for any finite $ J $ is derived as a corollary.

CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits instance

[HasFiniteLimits C] : HasFiniteProducts C

Full source

/-- If `C` has finite limits then it has finite products. -/
instance (priority := 10) hasFiniteProducts_of_hasFiniteLimits [HasFiniteLimits C] :
    HasFiniteProducts C :=
  ⟨fun _ => inferInstance⟩

Finite Limits Imply Finite Products in a Category

Informal description

Every category $\mathcal{C}$ with finite limits has finite products.

CategoryTheory.Limits.hasLimitsOfShape_discrete instance

[HasFiniteProducts C] (ι : Type w) [Finite ι] : HasLimitsOfShape (Discrete ι) C

Full source

instance hasLimitsOfShape_discrete [HasFiniteProducts C] (ι : Type w) [Finite ι] :
    HasLimitsOfShape (Discrete ι) C := by
  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
  haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
  exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Finite Products Imply Limits over Finite Discrete Categories

Informal description

For any category $\mathcal{C}$ with finite products and any finite type $\iota$, $\mathcal{C}$ has limits of shape $\mathrm{Discrete}\,\iota$. Here, $\mathrm{Discrete}\,\iota$ denotes the discrete category on $\iota$, where the only morphisms are identity morphisms.

CategoryTheory.Limits.hasFiniteProducts_of_hasProducts theorem

[HasProducts.{w} C] : HasFiniteProducts C

Full source

/-- If a category has all products then in particular it has finite products.
-/
theorem hasFiniteProducts_of_hasProducts [HasProducts.{w} C] : HasFiniteProducts C :=
  ⟨fun _ => hasLimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift.{w})⟩

Existence of Finite Products from All Products in a Category

Informal description

If a category $\mathcal{C}$ has all products (i.e., limits over discrete categories of any size), then it in particular has finite products (i.e., limits over finite discrete categories).

CategoryTheory.Limits.HasFiniteCoproducts structure

Full source

/-- 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.
-/
class HasFiniteCoproducts : Prop where
  /-- `C` has all finite coproducts -/
  out (n : ℕ) : HasColimitsOfShape (Discrete (Fin n)) C

Category with finite coproducts

Informal description

A category $ C $ has finite coproducts if for every finite indexing type $ J $, the category has colimits for all diagrams with shape $ \text{Discrete } J $. In the definition, we only require this condition for $ J = \text{Fin } n $, and then deduce the general case for any finite $ J $ as a consequence.

CategoryTheory.Limits.hasColimitsOfShape_discrete instance

[HasFiniteCoproducts C] (ι : Type w) [Finite ι] : HasColimitsOfShape (Discrete ι) C

Full source

instance hasColimitsOfShape_discrete [HasFiniteCoproducts C] (ι : Type w) [Finite ι] :
    HasColimitsOfShape (Discrete ι) C := by
  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
  haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
  exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Existence of Colimits for Discrete Finite Diagrams in Categories with Finite Coproducts

Informal description

For any category $C$ with finite coproducts and any finite type $\iota$, $C$ has colimits of shape $\mathrm{Discrete}\,\iota$. Here, $\mathrm{Discrete}\,\iota$ denotes the discrete category on $\iota$, where the only morphisms are identity morphisms.

CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits instance

[HasFiniteColimits C] : HasFiniteCoproducts C

Full source

/-- If `C` has finite colimits then it has finite coproducts. -/
instance (priority := 10) hasFiniteCoproducts_of_hasFiniteColimits [HasFiniteColimits C] :
    HasFiniteCoproducts C :=
  ⟨fun J => by infer_instance⟩

Finite Colimits Imply Finite Coproducts

Informal description

Every category $C$ with finite colimits has finite coproducts.

CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts theorem

[HasCoproducts.{w} C] : HasFiniteCoproducts C

Full source

/-- If a category has all coproducts then in particular it has finite coproducts.
-/
theorem hasFiniteCoproducts_of_hasCoproducts [HasCoproducts.{w} C] : HasFiniteCoproducts C :=
  ⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift.{w})⟩

Existence of Finite Coproducts from All Coproducts

Informal description

If a category $\mathcal{C}$ has all coproducts, then it has finite coproducts.