algebraMap

Mathlib.CategoryTheory.Monoidal.Internal.Module

URI: https://scilib.ai/kg/mathlib#ModuleCat.MonModuleEquivalenceAlgebra.algebraMap

English

In ModuleCat with Monoidal structure, the algebraMap from R to A coincides with the unit action η[A] on R.

Русский

В ModuleCat с мономорфной структурой алгебра Map R → A совпадает с действием единицы η[A] на R.

LaTeX

$$$ algebraMap R A r = η[A] r $$$

Lean4

@[simp]
theorem algebraMap (A : ModuleCat.{u} R) [MonObj A] (r : R) : algebraMap R A r = η[A] r :=
  rfl

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

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

Разделы

Аффилиация

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