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₂) : QuadraticMap.associated (Q₁.tmul Q₂) = (QuadraticMap.associated Q₁).tmul (QuadraticMap.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₂) : QuadraticMap.polarBilin (Q₁.tmul Q₂) = ⅟2 • (QuadraticMap.polarBilin Q₁).tmul (QuadraticMap.polarBilin Q₂)

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.tmul QuadraticMap.sq 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₂) : QuadraticMap.associated (QuadraticForm.baseChange A Q) = LinearMap.BilinMap.baseChange A (QuadraticMap.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₂) : QuadraticMap.polarBilin (QuadraticForm.baseChange A Q) = LinearMap.BilinMap.baseChange A (QuadraticMap.polarBilin Q)

theorem QuadraticForm.baseChange_ext_iff {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] {Q₁ : QuadraticForm A (TensorProduct R A M₂)} {Q₂ : QuadraticForm A (TensorProduct R A M₂)} : Q₁ = Q₂ ↔ ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)

theorem QuadraticForm.baseChange_ext {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [CommRing R] [CommRing A] [AddCommGroup M₂] [Algebra R A] [Module R M₂] ⦃Q₁ : QuadraticForm A (TensorProduct R A M₂)⦄ ⦃Q₂ : QuadraticForm A (TensorProduct R A M₂)⦄ (h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)) : Q₁ = Q₂

If two quadratic forms from A ⊗[R] M₂ agree on elements of the form 1 ⊗ m, they are equal.

In other words, if a base change exists for a quadratic form, it is unique.

Note that unlike QuadraticForm.baseChange, this does not need Invertible (2 : R).