associator_inv_apply — Mathlib

English

Let M, N, K be modules over a commutative ring R. The inverse of the associator α_{M,N,K}: M ⊗ N ⊗ K → (M ⊗ N) ⊗ K acts on a pure tensor m ⊗ (n ⊗ k) by sending it to m ⊗ n ⊗ k; i.e., (α_{M,N,K})^{-1}(m ⊗ (n ⊗ k)) = m ⊗ n ⊗ k.

Русский

Пусть M, N, K — модули над кольцом R. Обратимый ассоциатор α_{M,N,K}: M ⊗ N ⊗ K → (M ⊗ N) ⊗ K действует на простое тензорное произведение m ⊗ (n ⊗ k) так, что (α_{M,N,K})^{-1}(m ⊗ (n ⊗ k)) = m ⊗ n ⊗ k.

LaTeX

$$$((\\alpha_{M,N,K})^{-1} : M \\otimes N \\otimes K \\to (M \\otimes N) \\otimes K)(m \\otimes (n \\otimes k)) = m \\otimes n \\otimes k$$$

Lean4

@[simp]
theorem associator_inv_apply {M N K : ModuleCat.{u} R} (m : M) (n : N) (k : K) :
    ((α_ M N K).inv : M ⊗ N ⊗ K ⟶ (M ⊗ N) ⊗ K) (m ⊗ₜ (n ⊗ₜ k)) = m ⊗ₜ n ⊗ₜ k :=
  rfl

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