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 QuadraticMap.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] [Invertible 2] : TensorProduct R (QuadraticMap A M₁ N₁) (QuadraticMap R M₂ N₂) →ₗ[A] QuadraticMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuadraticMap.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] [Invertible 2] (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂) : ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₁ m₁ ⊗ₜ[R] Q₂ m₂

@[reducible, inline]

noncomputable abbrev QuadraticMap.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [CommRing R] [CommRing A] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [IsScalarTower R A N₁] [Module R M₂] [Module R N₂] [Invertible 2] (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) : QuadraticMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)

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

Equations

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

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

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

• QuadraticForm.tensorDistrib R A = ↑(TensorProduct.AlgebraTensorModule.rid R A A).congrQuadraticMap ∘ₗ QuadraticMap.tensorDistrib R A

@[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₂) : ((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₂) = LinearMap.BilinForm.tmul (QuadraticMap.associated Q₁) (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 • LinearMap.BilinForm.tmul (QuadraticMap.polarBilin Q₁) (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.BilinForm.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.BilinForm.baseChange A (QuadraticMap.polarBilin Q)

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

If two quadratic maps 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 map, it is unique.

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

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