Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Preserving terminal object #

Constructions to relate the notions of preserving terminal objects and reflecting terminal objects to concrete objects.

In particular, we show that terminalComparison G is an isomorphism iff G preserves terminal objects.

The map of an empty cone is a limit iff the mapped object is terminal.

Instances For

    If G preserves the terminal object and C has a terminal object, then the image of the terminal object is terminal.

    Instances For

      If C has a terminal object and G preserves terminal objects, then D has a terminal object also. Note this property is somewhat unique to (co)limits of the empty diagram: for general J, if C has limits of shape J and G preserves them, then D does not necessarily have limits of shape J.

      The map of an empty cocone is a colimit iff the mapped object is initial.

      Instances For

        If G preserves the initial object and C has an initial object, then the image of the initial object is initial.

        Instances For

          If C has an initial object and G preserves initial objects, then D has an initial object also. Note this property is somewhat unique to colimits of the empty diagram: for general J, if C has colimits of shape J and G preserves them, then D does not necessarily have colimits of shape J.