Linear equivalences of tensor products as isometries

These results are separate from the definition of QuadraticForm.tmul as that file is very slow.

Main definitions

• QuadraticForm.Isometry.tmul: TensorProduct.map as a QuadraticForm.Isometry
• QuadraticForm.tensorComm: TensorProduct.comm as a QuadraticForm.IsometryEquiv
• QuadraticForm.tensorAssoc: TensorProduct.assoc as a QuadraticForm.IsometryEquiv
• QuadraticForm.tensorRId: TensorProduct.rid as a QuadraticForm.IsometryEquiv
• QuadraticForm.tensorLId: TensorProduct.lid as a QuadraticForm.IsometryEquiv

@[simp]

theorem QuadraticForm.tmul_comp_tensorMap {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) : QuadraticForm.comp (QuadraticForm.tmul Q₂ Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = QuadraticForm.tmul Q₁ Q₃

@[simp]

theorem QuadraticForm.tmul_tensorMap_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃) : (QuadraticForm.tmul Q₂ Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (QuadraticForm.tmul Q₁ Q₃) x

noncomputable def QuadraticForm.Isometry.tmul {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) : QuadraticForm.tmul Q₁ Q₃ →qᵢ QuadraticForm.tmul Q₂ Q₄

TensorProduct.map for Quadraticform.Isometrys

Equations

• QuadraticForm.Isometry.tmul f g = { toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.tmul_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃) : (QuadraticForm.Isometry.tmul f g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x

@[simp]

theorem QuadraticForm.tmul_comp_tensorComm {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.comp (QuadraticForm.tmul Q₂ Q₁) ↑(TensorProduct.comm R M₁ M₂) = QuadraticForm.tmul Q₁ Q₂

@[simp]

theorem QuadraticForm.tmul_tensorComm_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : TensorProduct R M₁ M₂) : (QuadraticForm.tmul Q₂ Q₁) ((TensorProduct.comm R M₁ M₂) x) = (QuadraticForm.tmul Q₁ Q₂) x

noncomputable def QuadraticForm.tensorComm {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.IsometryEquiv (QuadraticForm.tmul Q₁ Q₂) (QuadraticForm.tmul Q₂ Q₁)

TensorProduct.comm preserves tensor products of quadratic forms.

Equations

• QuadraticForm.tensorComm Q₁ Q₂ = { toLinearEquiv := TensorProduct.comm R M₁ M₂, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.tensorComm_toLinearEquiv {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : (QuadraticForm.tensorComm Q₁ Q₂).toLinearEquiv = TensorProduct.comm R M₁ M₂

@[simp]

theorem QuadraticForm.tensorComm_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : TensorProduct R M₁ M₂) : (QuadraticForm.tensorComm Q₁ Q₂) x = (TensorProduct.comm R M₁ M₂) x

@[simp]

theorem QuadraticForm.tensorComm_symm {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm.IsometryEquiv.symm (QuadraticForm.tensorComm Q₁ Q₂) = QuadraticForm.tensorComm Q₂ Q₁

@[simp]

theorem QuadraticForm.tmul_comp_tensorAssoc {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) : QuadraticForm.comp (QuadraticForm.tmul Q₁ (QuadraticForm.tmul Q₂ Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = QuadraticForm.tmul (QuadraticForm.tmul Q₁ Q₂) Q₃

@[simp]

theorem QuadraticForm.tmul_tensorAssoc_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) (x : TensorProduct R (TensorProduct R M₁ M₂) M₃) : (QuadraticForm.tmul Q₁ (QuadraticForm.tmul Q₂ Q₃)) ((TensorProduct.assoc R M₁ M₂ M₃) x) = (QuadraticForm.tmul (QuadraticForm.tmul Q₁ Q₂) Q₃) x

noncomputable def QuadraticForm.tensorAssoc {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) : QuadraticForm.IsometryEquiv (QuadraticForm.tmul (QuadraticForm.tmul Q₁ Q₂) Q₃) (QuadraticForm.tmul Q₁ (QuadraticForm.tmul Q₂ Q₃))

TensorProduct.assoc preserves tensor products of quadratic forms.

Equations

• QuadraticForm.tensorAssoc Q₁ Q₂ Q₃ = { toLinearEquiv := TensorProduct.assoc R M₁ M₂ M₃, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.tensorAssoc_toLinearEquiv {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) : (QuadraticForm.tensorAssoc Q₁ Q₂ Q₃).toLinearEquiv = TensorProduct.assoc R M₁ M₂ M₃

@[simp]

theorem QuadraticForm.tensorAssoc_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) (x : TensorProduct R (TensorProduct R M₁ M₂) M₃) : (QuadraticForm.tensorAssoc Q₁ Q₂ Q₃) x = (TensorProduct.assoc R M₁ M₂ M₃) x

@[simp]

theorem QuadraticForm.tensorAssoc_symm_apply {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃) (x : TensorProduct R M₁ (TensorProduct R M₂ M₃)) : (QuadraticForm.IsometryEquiv.symm (QuadraticForm.tensorAssoc Q₁ Q₂ Q₃)) x = (LinearEquiv.symm (TensorProduct.assoc R M₁ M₂ M₃)) x

theorem QuadraticForm.comp_tensorRId_eq {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) : QuadraticForm.comp Q₁ ↑(TensorProduct.rid R M₁) = QuadraticForm.tmul Q₁ QuadraticForm.sq

@[simp]

theorem QuadraticForm.tmul_tensorRId_apply {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) (x : TensorProduct R M₁ R) : Q₁ ((TensorProduct.rid R M₁) x) = (QuadraticForm.tmul Q₁ QuadraticForm.sq) x

noncomputable def QuadraticForm.tensorRId {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) : QuadraticForm.IsometryEquiv (QuadraticForm.tmul Q₁ QuadraticForm.sq) Q₁

TensorProduct.rid preserves tensor products of quadratic forms.

Equations

• QuadraticForm.tensorRId Q₁ = { toLinearEquiv := TensorProduct.rid R M₁, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.tensorRId_toLinearEquiv {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) : (QuadraticForm.tensorRId Q₁).toLinearEquiv = TensorProduct.rid R M₁

@[simp]

theorem QuadraticForm.tensorRId_apply {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) (x : TensorProduct R M₁ R) : (QuadraticForm.tensorRId Q₁) x = (TensorProduct.rid R M₁) x

@[simp]

theorem QuadraticForm.tensorRId_symm_apply {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) (x : M₁) : (QuadraticForm.IsometryEquiv.symm (QuadraticForm.tensorRId Q₁)) x = (LinearEquiv.symm (TensorProduct.rid R M₁)) x

theorem QuadraticForm.comp_tensorLId_eq {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) : QuadraticForm.comp Q₂ ↑(TensorProduct.lid R M₂) = QuadraticForm.tmul QuadraticForm.sq Q₂

@[simp]

theorem QuadraticForm.tmul_tensorLId_apply {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) (x : TensorProduct R R M₂) : Q₂ ((TensorProduct.lid R M₂) x) = (QuadraticForm.tmul QuadraticForm.sq Q₂) x

noncomputable def QuadraticForm.tensorLId {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) : QuadraticForm.IsometryEquiv (QuadraticForm.tmul QuadraticForm.sq Q₂) Q₂

TensorProduct.lid preserves tensor products of quadratic forms.

Equations

• QuadraticForm.tensorLId Q₂ = { toLinearEquiv := TensorProduct.lid R M₂, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.tensorLId_toLinearEquiv {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) : (QuadraticForm.tensorLId Q₂).toLinearEquiv = TensorProduct.lid R M₂

@[simp]

theorem QuadraticForm.tensorLId_apply {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) (x : TensorProduct R R M₂) : (QuadraticForm.tensorLId Q₂) x = (TensorProduct.lid R M₂) x

@[simp]

theorem QuadraticForm.tensorLId_symm_apply {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) (x : M₂) : (QuadraticForm.IsometryEquiv.symm (QuadraticForm.tensorLId Q₂)) x = (LinearEquiv.symm (TensorProduct.lid R M₂)) x