comul_algebraMap

Mathlib.RingTheory.Bialgebra.Basic

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

English

The comultiplication of the image of r under algebraMap R A equals the image of r in A ⊗ A.

Русский

Кoумульования образа r через algebraMap равняется образу r в A ⊗ A.

LaTeX

$$$\text{comul}(\text{algebraMap}_R A\, r) = \text{algebraMap}_R (A\otimes_R A)\, r$$$

Lean4

@[simp]
theorem comul_algebraMap (r : R) : comul (R := R) (algebraMap R A r) = algebraMap R (A ⊗[R] A) r :=
  (comulAlgHom R A).commutes r

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

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

Разделы

Аффилиация

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