# The quadratic form on a tensor product #

## Main definitions #

• QuadraticForm.tensorDistrib (Q₁ ⊗ₜ Q₂): the quadratic form on M₁ ⊗ M₂ constructed by applying Q₁ on M₁ and Q₂ on M₂. This construction is not available in characteristic two.
noncomputable def QuadraticForm.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] :

The tensor product of two quadratic forms injects into quadratic forms on tensor products.

Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuadraticForm.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] (Q₁ : ) (Q₂ : ) (m₁ : M₁) (m₂ : M₂) :
( (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₂ m₂ Q₁ m₁
@[reducible, inline]
noncomputable abbrev QuadraticForm.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] (Q₁ : ) (Q₂ : ) :

The tensor product of two quadratic forms, a shorthand for dot notation.

Equations
Instances For
theorem QuadraticForm.associated_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] [] (Q₁ : ) (Q₂ : ) :
theorem QuadraticForm.polarBilin_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] [] (Q₁ : ) (Q₂ : ) :
QuadraticMap.polarBilin (Q₁.tmul Q₂) = 2 .tmul
noncomputable def QuadraticForm.baseChange {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] [] (Q : ) :

The base change of a quadratic form.

Equations
Instances For
@[simp]
theorem QuadraticForm.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] [] (Q : ) (a : A) (m₂ : M₂) :
(a ⊗ₜ[R] m₂) = Q m₂ (a * a)
theorem QuadraticForm.associated_baseChange {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [] [] [] [Algebra R A] [Module R M₂] [] [] (Q : ) :
If two quadratic forms from A ⊗[R] M₂ agree on elements of the form 1 ⊗ m, they are equal.
Note that unlike QuadraticForm.baseChange, this does not need Invertible (2 : R).