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 aQuadraticForm.Isometry
QuadraticForm.tensorComm
:TensorProduct.comm
as aQuadraticForm.IsometryEquiv
QuadraticForm.tensorAssoc
:TensorProduct.assoc
as aQuadraticForm.IsometryEquiv
QuadraticForm.tensorRId
:TensorProduct.rid
as aQuadraticForm.IsometryEquiv
QuadraticForm.tensorLId
:TensorProduct.lid
as aQuadraticForm.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
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.Isometry
s
Instances For
@[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
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.
Instances For
@[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₂)
:
@[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
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.
Instances For
@[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
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.
Instances For
@[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
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.
Instances For
@[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