coalgebra_iso_of_iso — Mathlib

English

If a coalgebra morphism f: A → B has an isomorphism carrier f.f in C, then f is an isomorphism in Coalgebra G.

Русский

Если морфизм коалгебр f: A → B имеет изоморфную carrier-часть f.f в C, то f является изоморфизмом в G-коалгебрах.

LaTeX

$$$\\\\forall A,B \\in G. Coalgebra, \\\\forall f: A \\\\to B, [IsIso f.f] \\\\Rightarrow IsIso f.$$$

Lean4

/-- Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalgebra isomorphism.
-/
theorem coalgebra_iso_of_iso {A B : Coalgebra G} (f : A ⟶ B) [IsIso f.f] : IsIso f :=
  ⟨⟨{   f := inv f.f
        h := by
          rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
          simp },
      by cat_disch⟩⟩

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