leftComm — Mathlib

English

The heterobasic left-commuting isomorphism equals the standard leftComm: leftComm R R M P Q = TensorProduct.leftComm R M P Q.

Русский

Гетеробазовая левосторонняя коммутативность совпадает с обычной leftComm: leftComm R R M P Q = TensorProduct.leftComm R M P Q.

LaTeX

$$$\mathrm{leftComm} \;R\;R\;M\;P\;Q = \mathrm{TensorProduct}.leftComm\;R\;M\;P\;Q$$$

Lean4

/-- Heterobasic version of `TensorProduct.leftComm` -/
def leftComm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) :=
  let e₁ := (assoc R A A M P Q).symm
  let e₂ := congr (TensorProduct.comm A M P) (1 : Q ≃ₗ[R] Q)
  let e₃ := assoc R A A P M Q
  e₁ ≪≫ₗ e₂ ≪≫ₗ e₃

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