mathlib3 documentation

category_theory.limits.preserves.shapes.terminal

Preserving terminal object #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

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.

If C has a initial object and G preserves initial objects, then D has a 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.