English
For a quadratic form Q2, composing with TensorProduct.lid yields Q2 ⊗ sq, i.e., Q2 ∘ lid = Q2 ⊗ sq.
Русский
Для Q2 композиция с TensorProduct.lid дает Q2 ⊗ sq.
LaTeX
$$$Q_2 \circ (\mathrm{TensorProduct}.lid\, R\, M_2) = Q_2 \otimes \mathrm{sq}$$$
Lean4
/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products.
Note this is heterobasic; the quadratic map on the left can take values in a module over a larger
ring than the one on the right. -/
def tensorDistrib : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂)
let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂)
let toB :=
AlgebraTensorModule.map (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁)
(QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂)
toQ ∘ₗ tmulB ∘ₗ toB
