rightComm — Mathlib

English

The associator is compatible with permutation of factors: (m ⊗ (n ⊗ p)) maps to (m ⊗ n) ⊗ p under the canonical isomorphisms.

Русский

Ассоциатор совместим с перестановкой факторов: (m ⊗ (n ⊗ p)) переходит в ((m ⊗ n) ⊗ p) через канонические изоморфизмы.

LaTeX

$$$\\text{assoc}_R(m, n, p) = m\\otimes_R (n\\otimes_R p) \\;\\text{to} \\; (m\\otimes_R n)\\otimes_R p$$$

Lean4

/-- A tensor product analogue of `mul_right_comm`. -/
def rightComm : M ⊗[R] N ⊗[R] P ≃ₗ[R] M ⊗[R] P ⊗[R] N :=
  LinearEquiv.ofLinear (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ (mk _ _ _).compr₂ (mk _ _ _))))
    (lift (lift (LinearMap.lflip.toLinearMap ∘ₗ (mk _ _ _).compr₂ (mk _ _ _)))) (by ext; rfl) (by ext; rfl)

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