tmul_comp_tensorMap — Mathlib

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]

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