toBialgIso — Mathlib

English

From an algebra isomorphism e between X and Y, construct an isomorphism in the category BialgCat R via the induced BialgCat.ofHom morphisms.

Русский

Из изоморфизма алгебр e между X и Y строим изоморфизм в категории BialgCat R с помощью соответствующих морфизмов BialgCat.ofHom.

LaTeX

$$$\text{toBialgIso}(e) : X \cong Y$ in BialgCat\,R, with\ hom := BialgCat.ofHom(e)$$$

Lean4

/-- Build an isomorphism in the category `BialgCat R` from a
`BialgEquiv`. -/
@[simps]
def toBialgIso (e : X ≃ₐc[R] Y) : BialgCat.of R X ≅ BialgCat.of R Y
    where
  hom := BialgCat.ofHom e
  inv := BialgCat.ofHom e.symm
  hom_inv_id := Hom.ext <| DFunLike.ext _ _ e.left_inv
  inv_hom_id := Hom.ext <| DFunLike.ext _ _ e.right_inv

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