English
If a bialgebra homomorphism f: A →ₐc[R] B is bijective, then there exists a BialgEquiv R A B with f as its forward map and the inverse given by its inverse homomorphism.
Русский
Если биалгебровый гомоморфизм f: A →ₐc[R] B биективен, тогда существует BialgEquiv R A B с f как прямой маппингом и обратным маппингом, задаваемым обратным гомоморфизмом.
LaTeX
$$$\\exists e : A \\simeq_{bialg} B \\;\\text{ with } e. toFun = f \\text{ and } e.invFun = g$$$
Lean4
/-- If an coalgebra morphism has an inverse, it is an coalgebra isomorphism. -/
def ofBialgHom (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A) :
A ≃ₐc[R] B where
__ := f
toFun := f
invFun := g
left_inv := BialgHom.ext_iff.1 h₂
right_inv := BialgHom.ext_iff.1 h₁
