mathlib documentation

category_theory.limits.shapes.constructions.limits_of_products_and_equalizers

Constructing limits from products and equalizers.

If a category has all products, and all equalizers, then it has all limits. Similarly, if it has all finite products, and all equalizers, then it has all finite limits.

TODO: provide the dual result.

@[simp]

Corresponding to any functor F : J ⥤ C, we construct a new functor from the walking parallel pair of morphisms to C, given by the diagram

         s
_j F j ===> Π_{f : j  j'} F j'
         t

where the two morphisms s and t are defined componentwise:

  • The s_f component is the projection ∏_j F j ⟶ F j followed by f.
  • The t_f component is the projection ∏_j F j ⟶ F j'.

In a moment we prove that cones over F are isomorphic to cones over this new diagram.

Equations

Any category with products and equalizers has all limits.

See https://stacks.math.columbia.edu/tag/002N.

Any category with finite products and equalizers has all finite limits.

See https://stacks.math.columbia.edu/tag/002O. (We do not prove equivalence with the third condition.)