toBialgEquiv — Mathlib

English

For an isomorphism i, the induced BialgEquiv equals the underlying first projection of i.hom.

Русский

Для изоморфизма i получаемый BialgEquiv равен первому проекции из i.hom.

LaTeX

$$$ (i.toBialgEquiv : X \to Y) = i.hom.1 $$$

Lean4

/-- Build a `BialgEquiv` from an isomorphism in the category
`BialgCat R`. -/
def toBialgEquiv (i : X ≅ Y) : X ≃ₐc[R] Y :=
  { i.hom.toBialgHom with
    invFun := i.inv.toBialgHom
    left_inv := fun x => BialgHom.congr_fun (congr_arg BialgCat.Hom.toBialgHom i.3) x
    right_inv := fun x => BialgHom.congr_fun (congr_arg BialgCat.Hom.toBialgHom i.4) x }

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