English
From a BialgEquiv e: X ≃ₐc[R] Y one constructs a HopfAlgCat R isomorphism between the corresponding objects X and Y, whose forward and inverse maps are given by e.liftings as Hopf algebra homomorphisms, with the appropriate left and right inverse properties.
Русский
Из эквивалента биалгебр e: X ≃ₐc[R] Y строится изоморфизм в HopfAlgCat R между X и Y, где прямой и обратный морфизмы задаются как гомоморфизмыHopf-алгебр, с выполняющимися свойствами обратимости слева и справа.
LaTeX
$$$$ toHopfAlgIso: e \\mapsto (X \\xrightarrow{e} Y) \\quad\\text{где } e.toBialgHom \\text{ задаёт гомоморфизм биалгебры.} $$$$
Lean4
/-- Build an isomorphism in the category `HopfAlgCat R` from a
`BialgEquiv`. -/
@[simps]
def toHopfAlgIso (e : X ≃ₐc[R] Y) : HopfAlgCat.of R X ≅ HopfAlgCat.of R Y
where
hom := HopfAlgCat.ofHom e
inv := HopfAlgCat.ofHom e.symm
hom_inv_id := Hom.ext <| DFunLike.ext _ _ e.left_inv
inv_hom_id := Hom.ext <| DFunLike.ext _ _ e.right_inv
