iso_of_iso — Mathlib

English

The forgetful functor forget F from Endofunctor.Algebra reflects isomorphisms.

Русский

Забывающий функтор forget F из Endofunctor.Algebra отражает изоморфизмы.

LaTeX

$$$\\operatorname{forget} F \\;:\\; \\mathbf{Endofunctor.Algebra} F \\to \\mathbf{C}$ ReflectsIsomorphisms$$

Lean4

/-- An algebra morphism with an underlying isomorphism hom in `C` is an algebra isomorphism. -/
theorem iso_of_iso (f : A₀ ⟶ A₁) [IsIso f.1] : IsIso f :=
  ⟨⟨{   f := inv f.1
        h := by simp }, by cat_disch, by cat_disch⟩⟩

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