toBialgHom — Mathlib

English

The bialgebra morphism underlying a bialgebra equivalence.

Русский

Биалгебровый морфизм, лежащий в основе биалгебровой эквивалентности.

LaTeX

$$$f_{BialgHom} : A \\to_{Bialg} B$$$

Lean4

/-- The bialgebra morphism underlying a bialgebra equivalence. -/
def toBialgHom (f : A ≃ₐc[R] B) : A →ₐc[R] B :=
  { f.toCoalgEquiv with
    map_one' := map_one f.toMulEquiv
    map_mul' := map_mul f.toMulEquiv }

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