moduleEndSelfOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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