preservesTerminal_of_isIso — Mathlib

English

There is a canonical isomorphism terminalComparison G whenever G preserves terminal objects.

Русский

Существует каноническая изоморфия terminalComparison G при сохранении терминалов G.

LaTeX

$$$\\operatorname{IsIso}(\\operatorname{terminalComparison} G).$$$

Lean4

/-- If there is any isomorphism `G.obj ⊤ ⟶ ⊤`, then `G` preserves terminal objects. -/
theorem preservesTerminal_of_isIso (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : IsIso f] : PreservesLimit (Functor.empty.{0} C) G :=
  by
  rw [Subsingleton.elim f (terminalComparison G)] at i
  exact PreservesTerminal.of_iso_comparison G

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