toModuleEnd_bijective — Mathlib

English

For an invertible module M over R, the canonical map from R to End_R(M) given by scalar multiplication is a bijection.

Русский

Для обратимого модуля M над R каноническое отображение R в End_R(M), заданное умножением на скаляры, является биекцией.

LaTeX

$$$\operatorname{toModuleEnd}_R(M): R \to \operatorname{End}_R(M) \text{ is bijective}$$$

Lean4

theorem toModuleEnd_bijective : Function.Bijective (toModuleEnd R (S := R) M) :=
  by
  have :
    toModuleEnd R (S := R) M =
      (lid R M).conj ∘
        rTensorEquiv R R (comm .. ≪≫ₗ linearEquiv R M) ∘ RingEquiv.moduleEndSelf R ∘ MulOpposite.opEquiv :=
    by ext; simp [LinearEquiv.conj, liftAux]
  simpa [this] using MulOpposite.opEquiv.bijective

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