English
If coalgebra homomorphisms f: A → B and g: B → A satisfy f ∘ g = id_B and g ∘ f = id_A, then there is a coalgebra equivalence A ≃ B induced by f.
Русский
Если коалгоморфизмы f: A → B и g: B → A удовлетворяют f ∘ g = id_B и g ∘ f = id_A, то существует коалгебраическое эквивалентное отображение A ≃ B, индуцируемое f.
LaTeX
$$$\\exists e : A \\simeq_{coalg} B$ при условии\\; f \\circ g = id_B \\; и \\; g \\circ f = id_A$$$
Lean4
/-- If an coalgebra morphism has an inverse, it is an coalgebra isomorphism. -/
def ofCoalgHom (f : A →ₗc[R] B) (g : B →ₗc[R] A) (h₁ : f.comp g = CoalgHom.id R B) (h₂ : g.comp f = CoalgHom.id R A) :
A ≃ₗc[R] B where
__ := f
toFun := f
invFun := g
left_inv := CoalgHom.ext_iff.1 h₂
right_inv := CoalgHom.ext_iff.1 h₁
