hasTerminal_of_hasTerminal_of_preservesLimit

English

If C has a terminal object and G preserves terminal objects, then D has a terminal object.

Русский

Если в C имеется терминал и G сохраняет терминальность, то в D также имеется терминал.

LaTeX

$$$[\\HasTerminal C] \\land [\\text{PreservesTerminal}(G)] \\Rightarrow \\text{HasTerminal}(D).$$$

Lean4

/-- 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`.
-/
theorem hasTerminal_of_hasTerminal_of_preservesLimit [PreservesLimit (Functor.empty.{0} C) G] : HasTerminal D :=
  ⟨fun F => by
    haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
    apply hasLimit_of_iso F.uniqueFromEmpty.symm⟩

Похожие утверждения