Documentation

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

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 #

@[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₄) :
QuadraticMap.comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul 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₃) :
(Q₂.tmul Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (Q₁.tmul Q₃) x
noncomputable def QuadraticMap.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₄) :
Q₁.tmul Q₃ →qᵢ Q₂.tmul Q₄

TensorProduct.map for Quadraticform.Isometrys

Equations
  • f.tmul g = { toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap, map_app' := }
Instances For
    @[simp]
    theorem QuadraticMap.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₃) :
    (f.tmul 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₂) :
    QuadraticMap.comp (Q₂.tmul Q₁) (TensorProduct.comm R M₁ M₂) = Q₁.tmul 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₂) :
    (Q₂.tmul Q₁) ((TensorProduct.comm R M₁ M₂) x) = (Q₁.tmul 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₂) :
    QuadraticMap.IsometryEquiv (Q₁.tmul Q₂) (Q₂.tmul Q₁)

    TensorProduct.comm preserves tensor products of quadratic forms.

    Equations
    Instances For
      @[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₂) :
      (Q₁.tensorComm 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₂) :
      (Q₁.tensorComm 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₂) :
      (Q₁.tensorComm Q₂).symm = Q₂.tensorComm 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₃) :
      QuadraticMap.comp (Q₁.tmul (Q₂.tmul Q₃)) (TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul 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₃) :
      (Q₁.tmul (Q₂.tmul Q₃)) ((TensorProduct.assoc R M₁ M₂ M₃) x) = ((Q₁.tmul Q₂).tmul 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₃) :
      QuadraticMap.IsometryEquiv ((Q₁.tmul Q₂).tmul Q₃) (Q₁.tmul (Q₂.tmul Q₃))

      TensorProduct.assoc preserves tensor products of quadratic forms.

      Equations
      • Q₁.tensorAssoc Q₂ Q₃ = { toLinearEquiv := TensorProduct.assoc R M₁ M₂ M₃, map_app' := }
      Instances For
        @[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₃) :
        (Q₁.tensorAssoc 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₃) :
        (Q₁.tensorAssoc 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₃)) :
        (Q₁.tensorAssoc Q₂ Q₃).symm x = (TensorProduct.assoc R M₁ M₂ M₃).symm 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₁) :
        QuadraticMap.comp Q₁ (TensorProduct.rid R M₁) = Q₁.tmul QuadraticMap.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) = (Q₁.tmul QuadraticMap.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₁) :
        QuadraticMap.IsometryEquiv (Q₁.tmul QuadraticMap.sq) Q₁

        TensorProduct.rid preserves tensor products of quadratic forms.

        Equations
        Instances For
          @[simp]
          theorem QuadraticForm.tensorRId_toLinearEquiv {R : Type uR} {M₁ : Type uM₁} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Invertible 2] (Q₁ : QuadraticForm R M₁) :
          Q₁.tensorRId.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) :
          Q₁.tensorRId 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₁) :
          Q₁.tensorRId.symm x = (TensorProduct.rid R M₁).symm 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₂) :
          QuadraticMap.comp Q₂ (TensorProduct.lid R M₂) = QuadraticForm.tmul QuadraticMap.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 QuadraticMap.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₂) :

          TensorProduct.lid preserves tensor products of quadratic forms.

          Equations
          Instances For
            @[simp]
            theorem QuadraticForm.tensorLId_toLinearEquiv {R : Type uR} {M₂ : Type uM₂} [CommRing R] [AddCommGroup M₂] [Module R M₂] [Invertible 2] (Q₂ : QuadraticForm R M₂) :
            Q₂.tensorLId.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₂) :
            Q₂.tensorLId 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₂) :
            Q₂.tensorLId.symm x = (TensorProduct.lid R M₂).symm x