Documentation

Mathlib.CategoryTheory.Limits.Connected

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.

Equations
Instances For

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

    Equations
    Instances For

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For