mathlib documentation


Connected limits #

A connected limit is a limit whose shape is a connected category.

We give examples of connected categories, and prove that the functor given by (X × -) preserves any connected limit. That is, any limit of shape J where J is a connected category is preserved by the functor (X × -).

(Impl). The obvious natural transformation from (X × K -) to K.


The functor (X × -) preserves any connected limit. Note that this functor does not preserve the two most obvious disconnected limits - that is, (X × -) does not preserve products or terminal object, eg (X ⨯ A) ⨯ (X ⨯ B) is not isomorphic to X ⨯ (A ⨯ B) and X ⨯ 1 is not isomorphic to 1.