counitBialgHom_toCoalgHom

Mathlib.RingTheory.Bialgebra.Hom

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

English

Any two bialgebra homomorphisms A →ₐc[R] R are equal; there is at most one such map.

Русский

Любые две биалгебра-гомоморфные A →ₐc[R] R совпадают; существует не более одного такого отображения.

LaTeX

$$ext_to_ring (f g : A →ₐc[R] R) : f = g$$

Lean4

@[simp]
theorem counitBialgHom_toCoalgHom : counitBialgHom R A = Coalgebra.counitCoalgHom R A :=
  rfl

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

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

Разделы

Аффилиация

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