isoMk — Mathlib

English

From a BialgEquiv between X and Y one builds a commutative bialgebra isomorphism between of R X and of R Y.

Русский

Из биалгебрового эквивалента между X и Y строится изоморфизм биалгебр между of R X и of R Y.

LaTeX

$$$\mathrm{isoMk}\;\{X,Y\} : \mathrm{of}\,R X \cong \mathrm{of}\,R Y$$$

Lean4

/-- Build an isomorphism in the category `CommBialgCat R` from a `BialgEquiv` between
`Bialgebra`s. -/
@[simps]
def isoMk {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Bialgebra R X} {_ : Bialgebra R Y} (e : X ≃ₐc[R] Y) :
    of R X ≅ of R Y where
  hom := ofHom (e : X →ₐc[R] Y)
  inv := ofHom (e.symm : Y →ₐc[R] X)

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