Tensor products of equivalent quadratic forms

This file shows that tensor products preserve isometric equivalences and equivalence of quadratic forms, including Mathlib's heterobasic tensor products whose left factor is a form over an R-algebra A. It complements Mathlib's tensor product of quadratic-form isometries.

Main definitions

• QuadraticMap.IsometryEquiv.tmul: the tensor product of two isometric equivalences.
• QuadraticMap.Equivalent.tmul: tensor products preserve equivalence of quadratic forms.
• QuadraticForm.smul_tmul: scaling the left form scales the tensor product.
• QuadraticMap.rankOneTensorIsometry: tensoring with a • sq scales the other form by a.
• QuadraticForm.IsometryEquiv.tmulProd: tensor product distributes over orthogonal product.

@[simp]

theorem QuadraticForm.smul_tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing A] [Algebra R A] [AddCommGroup M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] [AddCommGroup M₂] [Module R M₂] (a : A) (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : (a • Q₁).tmul Q₂ = a • Q₁.tmul Q₂

Scaling the left form scales the tensor product of two quadratic forms.

def QuadraticMap.rankOneTensorIsometry {R : Type u_1} [CommRing R] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (a : R) : IsometryEquiv (QuadraticForm.tmul (a • sq) Q) (a • Q)

Tensoring a form with the quadratic line a • sq is isometric to scaling by a. The isometry is the left unit equivalence of the tensor product.

@[simp]

theorem QuadraticMap.rankOneTensorIsometry_tmul {R : Type u_1} [CommRing R] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (a r : R) (v : V) : (rankOneTensorIsometry Q a) (r ⊗ₜ[R] v) = r • v

The rank-one tensor isometry sends a pure tensor to scalar multiplication.

@[simp]

theorem QuadraticMap.rankOneTensorIsometry_symm_apply {R : Type u_1} [CommRing R] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (a : R) (v : V) : (rankOneTensorIsometry Q a).symm v = 1 ⊗ₜ[R] v

The inverse rank-one tensor isometry sends a vector to its unit pure tensor.

def QuadraticMap.IsometryEquiv.tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommRing A] [Algebra R A] [AddCommGroup M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] [AddCommGroup M₂] [Module R M₂] [Module A M₂] [IsScalarTower R A M₂] [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] {Q₁ : QuadraticForm A M₁} {Q₂ : QuadraticForm A M₂} {S₁ : QuadraticForm R N₁} {S₂ : QuadraticForm R N₂} (e : IsometryEquiv Q₁ Q₂) (f : IsometryEquiv S₁ S₂) : IsometryEquiv (Q₁.tmul S₁) (Q₂.tmul S₂)

Tensor product of isometric equivalences of quadratic forms. As for QuadraticForm.tmul, the left factors may be forms over an R-algebra A.

@[simp]

theorem QuadraticMap.IsometryEquiv.tmul_tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommRing A] [Algebra R A] [AddCommGroup M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] [AddCommGroup M₂] [Module R M₂] [Module A M₂] [IsScalarTower R A M₂] [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] {Q₁ : QuadraticForm A M₁} {Q₂ : QuadraticForm A M₂} {S₁ : QuadraticForm R N₁} {S₂ : QuadraticForm R N₂} (e : IsometryEquiv Q₁ Q₂) (f : IsometryEquiv S₁ S₂) (x : M₁) (y : N₁) : (e.tmul f) (x ⊗ₜ[R] y) = e x ⊗ₜ[R] f y

The tensor product of two isometric equivalences acts componentwise on pure tensors.

theorem QuadraticMap.Equivalent.tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommRing A] [Algebra R A] [AddCommGroup M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] [AddCommGroup M₂] [Module R M₂] [Module A M₂] [IsScalarTower R A M₂] [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] {Q₁ : QuadraticForm A M₁} {Q₂ : QuadraticForm A M₂} {S₁ : QuadraticForm R N₁} {S₂ : QuadraticForm R N₂} (hQ : Equivalent Q₁ Q₂) (hS : Equivalent S₁ S₂) : Equivalent (Q₁.tmul S₁) (Q₂.tmul S₂)

Tensor product preserves equivalence of quadratic forms.

def QuadraticForm.IsometryEquiv.tmulProd {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (Q : QuadraticForm A M) (S : QuadraticForm R N) (T : QuadraticForm R P) : QuadraticMap.IsometryEquiv (Q.tmul (QuadraticMap.prod S T)) (QuadraticMap.prod (Q.tmul S) (Q.tmul T))

Tensor product distributes over the orthogonal product of quadratic forms.

@[simp]

theorem QuadraticForm.IsometryEquiv.tmulProd_tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (Q : QuadraticForm A M) (S : QuadraticForm R N) (T : QuadraticForm R P) (m : M) (np : N × P) : (tmulProd Q S T) (m ⊗ₜ[R] np) = (m ⊗ₜ[R] np.1, m ⊗ₜ[R] np.2)

The distributivity isometry acts on a pure tensor by projecting its product-valued factor.

@[simp]

theorem QuadraticForm.IsometryEquiv.tmulProd_symm_tmul {R : Type u_1} [CommRing R] [Invertible 2] {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (Q : QuadraticForm A M) (S : QuadraticForm R N) (T : QuadraticForm R P) (m : M) (n : N) (p : P) : (tmulProd Q S T).symm (m ⊗ₜ[R] n, m ⊗ₜ[R] p) = m ⊗ₜ[R] (n, p)

The inverse distributivity isometry combines a pair of pure tensors with the same first factor into a pure tensor with product-valued second factor.