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₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] : TensorProduct R (QuadraticForm A M₁) (QuadraticForm R M₂) →ₗ[A] QuadraticForm A (TensorProduct R M₁ 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.

@[simp]

theorem QuadraticForm.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : ((QuadraticForm.tensorDistrib R A) (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₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm A (TensorProduct R M₁ M₂)

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

Equations

• Q₁.tmul Q₂ = (QuadraticForm.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)

theorem QuadraticForm.associated_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.associated (Q₁.tmul Q₂) = (QuadraticForm.associated Q₁).tmul (QuadraticForm.associated Q₂)

theorem QuadraticForm.polarBilin_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [Invertible 2] [Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : (Q₁.tmul Q₂).polarBilin = ⅟2 • Q₁.polarBilin.tmul Q₂.polarBilin

noncomputable def QuadraticForm.baseChange {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] (Q : QuadraticForm R M₂) : QuadraticForm A (TensorProduct R A M₂)

The base change of a quadratic form.

Equations

• QuadraticForm.baseChange A Q = QuadraticForm.sq.tmul Q

@[simp]

theorem QuadraticForm.baseChange_tmul {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : (QuadraticForm.baseChange A Q) (a ⊗ₜ[R] m₂) = Q m₂ • (a * a)

theorem QuadraticForm.associated_baseChange {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] [Invertible 2] (Q : QuadraticForm R M₂) : QuadraticForm.associated (QuadraticForm.baseChange A Q) = LinearMap.BilinForm.baseChange A (QuadraticForm.associated Q)

theorem QuadraticForm.polarBilin_baseChange {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] [Invertible 2] [Invertible 2] (Q : QuadraticForm R M₂) : (QuadraticForm.baseChange A Q).polarBilin = LinearMap.BilinForm.baseChange A Q.polarBilin