Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.BasicTensor products of two complex Lorentz vectors
@[expose] public section
Equivalence of complexContr ⊗ complexContr to 4 x 4 complex matrices.
def contrContrToMatrix : (ContrℂModule ⊗[ℂ] ContrℂModule) ≃ₗ[ℂ]
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
(Basis.tensorProduct complexContrBasis complexContrBasis).repr ≪≫ₗ
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
Expanding contrContrToMatrix in terms of the standard basis.
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ ∑ x,
∑ y,
((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(x, y) •
(complexContrBasis.tensorProduct complexContrBasis) (x, y) =
∑ i, ∑ j, M i j • complexContrBasis i ⊗ₜ[ℂ] complexContrBasis j
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin 3x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(i, j) •
(complexContrBasis.tensorProduct complexContrBasis) (i, j) =
M i j • complexContrBasis i ⊗ₜ[ℂ] complexContrBasis j
All goals completed! 🐙
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M) ∈
Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙
Equivalence of complexCo ⊗ complexCo to 4 x 4 complex matrices.
def coCoToMatrix : (CoℂModule ⊗[ℂ] CoℂModule) ≃ₗ[ℂ]
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
(Basis.tensorProduct complexCoBasis complexCoBasis).repr ≪≫ₗ
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
Expanding coCoToMatrix in terms of the standard basis.
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ ∑ x,
∑ y,
((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(x, y) •
(complexCoBasis.tensorProduct complexCoBasis) (x, y) =
∑ i, ∑ j, M i j • complexCoBasis i ⊗ₜ[ℂ] complexCoBasis j
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin 3x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(i, j) •
(complexCoBasis.tensorProduct complexCoBasis) (i, j) =
M i j • complexCoBasis i ⊗ₜ[ℂ] complexCoBasis j
All goals completed! 🐙
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M) ∈
Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙
Equivalence of complexContr ⊗ complexCo to 4 x 4 complex matrices.
def contrCoToMatrix : (ContrℂModule ⊗[ℂ] CoℂModule) ≃ₗ[ℂ]
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
(Basis.tensorProduct complexContrBasis complexCoBasis).repr ≪≫ₗ
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
Expansion of contrCoToMatrix in terms of the standard basis.
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ ∑ x,
∑ y,
((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(x, y) •
(complexContrBasis.tensorProduct complexCoBasis) (x, y) =
∑ i, ∑ j, M i j • complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin 3x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(i, j) •
(complexContrBasis.tensorProduct complexCoBasis) (i, j) =
M i j • complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j
All goals completed! 🐙
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M) ∈
Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙
Equivalence of complexCo ⊗ complexContr to 4 x 4 complex matrices.
def coContrToMatrix : (CoℂModule ⊗[ℂ] ContrℂModule) ≃ₗ[ℂ]
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
(Basis.tensorProduct complexCoBasis complexContrBasis).repr ≪≫ₗ
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
Expansion of coContrToMatrix in terms of the standard basis.
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ ∑ x,
∑ y,
((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(x, y) •
(complexCoBasis.tensorProduct complexContrBasis) (x, y) =
∑ i, ∑ j, M i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin 3x✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M))
(i, j) •
(complexCoBasis.tensorProduct complexContrBasis) (i, j) =
M i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j
All goals completed! 🐙
M:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ⊢ (Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3))).symm
((LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)).symm M) ∈
Finsupp.supported ℂ ℂ ↑Finset.univ All goals completed! 🐙Group actions
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x⊢ ∑ y,
∑ x,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j y *
contrContrToMatrix v x y =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x⊢ (fun y =>
∑ x,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j y *
contrContrToMatrix v x y) =
fun x =>
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3⊢ ∑ x_1,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
contrContrToMatrix v x_1 x =
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3⊢ (fun x_1 =>
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
contrContrToMatrix v x_1 x) =
fun x1 =>
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
contrContrToMatrix v x1 x =
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:ContrℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x *
contrContrToMatrix v x1 x =
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
All goals completed! 🐙v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j⊢ ∑ y,
∑ x,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j y *
coCoToMatrix v x y =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j⊢ (fun y =>
∑ x,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j y *
coCoToMatrix v x y) =
fun x =>
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3⊢ ∑ x_1,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
coCoToMatrix v x_1 x =
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3⊢ (fun x_1 =>
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
coCoToMatrix v x_1 x) =
fun x1 =>
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
coCoToMatrix v x1 x =
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:CoℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j *
coCoToMatrix v x1 x =
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
All goals completed! 🐙v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j⊢ ∑ y,
∑ x,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j y *
contrCoToMatrix v x y =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j⊢ (fun y =>
∑ x,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j y *
contrCoToMatrix v x y) =
fun x =>
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3⊢ ∑ x_1,
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
contrCoToMatrix v x_1 x =
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3⊢ (fun x_1 =>
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
contrCoToMatrix v x_1 x) =
fun x1 =>
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i x1 *
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) j x *
contrCoToMatrix v x1 x =
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
v:ContrℂModule ⊗[ℂ] CoℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x) *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j =
∑ x,
∑ x1,
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x jx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j *
contrCoToMatrix v x1 x =
LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 * contrCoToMatrix v x1 x *
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
All goals completed! 🐙v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x⊢ ∑ y,
∑ x,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j y *
coContrToMatrix v x y =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x⊢ (fun y =>
∑ x,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j y *
coContrToMatrix v x y) =
fun x =>
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3⊢ ∑ x_1,
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
coContrToMatrix v x_1 x =
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3⊢ (fun x_1 =>
(LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x_1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
coContrToMatrix v x_1 x) =
fun x1 =>
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i x1 *
(LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) j x *
coContrToMatrix v x1 x =
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
v:CoℂModule ⊗[ℂ] ContrℂModuleM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h1:∑ x,
(∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x) *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x =
∑ x,
∑ x1,
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j xx:Fin 1 ⊕ Fin 3x1:Fin 1 ⊕ Fin 3⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x *
coContrToMatrix v x1 x =
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i * coContrToMatrix v x1 x *
LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
All goals completed! 🐙The symm version of the group actions.
All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙