str_isIso — Mathlib

English

Given a terminal coalgebra A for an endofunctor F, the structure map A.str: A ⟶ F A is an isomorphism; equivalently, A is isomorphic to F A via this structure map.

Русский

Пусть A — терминальная коалгебра для конечного эндофункторa F; структура A.str: A ⟶ F A является изоморфизмом; таким образом A изоморфно FA через данную структуру.

LaTeX

$$$\\text{IsIso }(A.\\mathrm{str}).$$$

Lean4

/-- The structure map of the terminal coalgebra is an isomorphism,
hence endofunctors preserve their terminal coalgebras
-/
theorem str_isIso (h : Limits.IsTerminal A) : IsIso A.str :=
  { out := ⟨strInv h, right_inv _, left_inv _⟩ }

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