moduleEndSelf — Mathlib

English

There is a canonical R-algebra isomorphism from A^op to End_R(A) induced by right multiplication.

Русский

Существует каноническое R-алгебрное изоморфирование из A^{op} в End_R(A), индуцированное правым умножением.

LaTeX

$$$ A^{op} \\cong_R \\mathrm{End}_R(A) \\quad\\text{(given by } a^{op} \\mapsto (x \\mapsto x a) \\text{)} $$$

Lean4

/-- The canonical algebra isomorphism from `Aᵐᵒᵖ` to `Module.End A A` induced by the right
multiplication. -/
@[simps!]
def moduleEndSelf : Aᵐᵒᵖ ≃ₐ[R] Module.End A A
    where
  __ := RingEquiv.moduleEndSelf A
  commutes' _ := by ext; simp [Algebra.algebraMap_eq_smul_one]

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