English
Let R be a commutative ring in which 2 is invertible. For quadratic forms Q1 on M1, Q2 on M2, and Q3 on M3, there exists a canonical isometry between the triple tensor products ((Q1 ⊗ Q2) ⊗ Q3) and (Q1 ⊗ (Q2 ⊗ Q3)).
Русский
Пусть R — коммутативное кольцо, в котором обратимо 2. Пусть Q1 на M1, Q2 на M2, Q3 на M3 — квадратичные формы. Существование канонической изометрии между тройными тензорными произведениями ((Q1 ⊗ Q2) ⊗ Q3) и (Q1 ⊗ (Q2 ⊗ Q3)).
LaTeX
$$$((Q_1 \otimes Q_2) \otimes Q_3) \cong_{\mathrm{iso}} (Q_1 \otimes (Q_2 \otimes Q_3)).$$$
Lean4
/-- `TensorProduct.assoc` preserves tensor products of quadratic forms. -/
@[simps toLinearEquiv]
def tensorAssoc (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) :
((Q₁.tmul Q₂).tmul Q₃).IsometryEquiv (Q₁.tmul (Q₂.tmul Q₃))
where
toLinearEquiv := TensorProduct.assoc R M₁ M₂ M₃
map_app' := tmul_tensorAssoc_apply Q₁ Q₂ Q₃
