assoc — Mathlib

English

There exists a natural associativity isomorphism for tensor products of R-modules: M ⊗R N ⊗R P ≅ M ⊗R (N ⊗R P).

Русский

Существует естественный ассоциативный изоморфизм тензорного произведения модулей: M ⊗R N ⊗R P ≅ M ⊗R (N ⊗R P).

LaTeX

$$$M \\otimes_R N \\otimes_R P \\cong_R M \\otimes_R (N \\otimes_R P)$$$

Lean4

/-- The associator for tensor product of R-modules, as a linear equivalence. -/
protected def assoc : M ⊗[R] N ⊗[R] P ≃ₗ[R] M ⊗[R] (N ⊗[R] P) :=
  LinearEquiv.ofLinear (lift <| lift <| lcurry _ _ _ _ ∘ₗ mk _ _ _) (lift <| uncurry _ _ _ _ ∘ₗ curry (mk R _ _))
    (by ext; rfl) (by ext; rfl)

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