unitBialgHom

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#Bialgebra.unitBialgHom

English

The unit map from the base ring R to a bialgebra A is a bialgebra hom.

Русский

Единичное отображение из базового кольца R в биалгебру A является гомоморфизмом биалгебры.

LaTeX

$$unitBialgHom : R →ₐc[R] A$$

Lean4

/-- The unit of a bialgebra as a `BialgHom`. -/
noncomputable def unitBialgHom : R →ₐc[R] A :=
  .ofAlgHom (Algebra.ofId R A) (by ext) (by ext)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru