English
If f and g are isometries between quadratic forms, then the composed map on the tensor product equals the tmul of the sources, i.e., (Q1 → Q2) ∘ (Q3 → Q4) induces Q1.tmul Q3 → Q2.tmul Q4 via TensorProduct.map.
Русский
Если f и g — изометрии между квадратичными формами, то композиция на тензорном произведении равна tmul между исходными формами: (Q1 → Q2) ∘ (Q3 → Q4) порождает Q1.tmul Q3 → Q2.tmul Q4 через TensorProduct.map.
LaTeX
$$$(Q_1 \\to q\\!\\!\\!i Q_2) \\; (Q_3 \\to q\\!\\!\\!i Q_4) \\Rightarrow (Q_2 \\tmul Q_4) \\circ \\mathrm{TensorProduct}.map f.toLinearMap g.toLinearMap = Q_1 \\tmul Q_3$$$
Lean4
@[simp]
theorem tmul_comp_tensorMap {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
{Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) :
(Q₂.tmul Q₄).comp (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃ :=
by
have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm
have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm
refine (QuadraticMap.associated_rightInverse R).injective ?_
ext m₁ m₃ m₁' m₃'
simp [-associated_apply, h₁, h₃, associated_tmul]