iso_of_iso — Mathlib

English

The forgetful functor forget F from Coalgebra to base category reflects isomorphisms.

Русский

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

LaTeX

$$$\\text{forget } F \\;:\\; \\mathbf{Coalgebra} F \\to \\mathbf{C}$ ReflectsIsomorphisms$$

Lean4

/-- A coalgebra morphism with an underlying isomorphism hom in `C` is a coalgebra isomorphism. -/
theorem iso_of_iso (f : V₀ ⟶ V₁) [IsIso f.1] : IsIso f :=
  ⟨⟨{   f := inv f.1
        h := by
          rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
          simp },
      by cat_disch, by cat_disch⟩⟩

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