moduleEndSelfOp — Mathlib

English

There is a canonical ring isomorphism from R to End_R(R)^{op} given by left multiplication: r ↦ (x ↦ r x).

Русский

Существует канонический кольцевой изоморфизм R ≅ End_R(R)^{op}, заданный левым умножением: r ↦ (x ↦ r x).

LaTeX

$$$R \\cong \\mathrm{End}_R(R)^{\\mathrm{op}},\\; r \\mapsto (x \\mapsto r x).$$$

Lean4

/-- The canonical (semi)ring isomorphism from `R` to `Module.End Rᵐᵒᵖ R` induced by the left
multiplication. -/
@[simps]
def moduleEndSelfOp : R ≃+* Module.End Rᵐᵒᵖ R :=
  { Module.toModuleEnd _ _ with
    toFun := DistribMulAction.toLinearMap _ _
    invFun := fun f ↦ f 1
    left_inv := mul_one
    right_inv := fun _ ↦ LinearMap.ext_ring_op <| mul_one _ }

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