English
From an isomorphism i in HopfAlgCat R one constructs a BialgEquiv between X and Y whose underlying bialgebra maps are the components of i.hom and i.inv, and whose inverse data come from the rest of the isomorphism.
Русский
Из изоморфизма i в HopfAlgCat R строится BialgEquiv между X и Y, где основанные на биалгебрах карты совпадают с компонентами i.hom и i.inv, а данные обратного направления получаются из остальной части изоморфизма.
LaTeX
$$$$ toHopfAlgEquiv(i) : X \\simeq_{bialg} Y, \\quad (toHopfAlgEquiv(i)).hom = i.hom.toBialgHom, \\ (toHopfAlgEquiv(i)).inv = i.inv.toBialgHom. $$$$
Lean4
/-- Build a `BialgEquiv` from an isomorphism in the category
`HopfAlgCat R`. -/
def toHopfAlgEquiv (i : X ≅ Y) : X ≃ₐc[R] Y :=
{ i.hom.toBialgHom with
invFun := i.inv.toBialgHom
left_inv := fun x => BialgHom.congr_fun (congr_arg HopfAlgCat.Hom.toBialgHom i.3) x
right_inv := fun x => BialgHom.congr_fun (congr_arg HopfAlgCat.Hom.toBialgHom i.4) x }
