tensorEquivEnd — Mathlib

English

There is a canonical isomorphism of R-algebras between the tensor product R ⊗_R R^{op} and the endomorphism algebra End_R(R).

Русский

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

LaTeX

$$$R ⊗_R R^{op} \cong_R \\mathrm{End}_R(R).$$$

Lean4

/-- The "canonical" isomorphism between `R ⊗ Rᵒᵖ` and `End R R` which is equal
  to `AlgHom.mulLeftRight R R`. -/
abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=
  Algebra.TensorProduct.lid R Rᵐᵒᵖ |>.trans <| .moduleEndSelf R

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