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.Fermions.Weyl.Two
public import Physlib.Relativity.Fermions.Weyl.ContractionUnits of Weyl fermions
We define the units for Weyl fermions, often denoted δ in the literature.
@[expose] public section
The left-dual-left unit δᵃₐ as an element of (leftHanded ⊗ dualLeftHanded).V.
def leftDualLeftUnitVal : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) :=
leftDualLeftToMatrix.symm 1
Expansion of leftDualLeftUnitVal into the basis.
lemma leftDualLeftUnitVal_expand_tmul : leftDualLeftUnitVal =
LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 +
LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 := ⊢ leftDualLeftUnitVal =
LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1
⊢ leftDualLeftToMatrix.symm 1 =
LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1
erw [⊢ ∑ i, ∑ j, 1 i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j =
LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1⊢ ∑ i, ∑ j, 1 i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j =
LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1
All goals completed! 🐙
The left-dual-left unit δᵃₐ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ dualLeftHanded ,
manifesting the invariance under the SL(2,ℂ) action.
M:SL(2, ℂ)x:ℂ⊢ leftDualLeftToMatrix.symm 1 = leftDualLeftToMatrix.symm (↑M * 1 * (↑M)⁻¹)
M:SL(2, ℂ)x:ℂ⊢ 1 = ↑M * 1 * (↑M)⁻¹
All goals completed! 🐙lemma leftDualLeftUnit_apply_one : leftDualLeftUnit (1 : ℂ) = leftDualLeftUnitVal := ⊢ leftDualLeftUnit 1 = leftDualLeftUnitVal
⊢ 1 • leftDualLeftUnitVal = leftDualLeftUnitVal
All goals completed! 🐙
The dual-left-left unit δₐᵃ as an element of (dualLeftHanded ⊗ leftHanded).V.
def dualLeftLeftUnitVal : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) :=
dualLeftLeftToMatrix.symm 1
Expansion of dualLeftLeftUnitVal into the basis.
⊢ ∑ i, ∑ j, 1 i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j =
DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 + DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1
All goals completed! 🐙
The dual-left-left unit δₐᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualLeftHanded ⊗ leftHanded , manifesting the invariance under the SL(2,ℂ) action.
M:SL(2, ℂ)x:ℂ⊢ dualLeftLeftToMatrix.symm 1 = dualLeftLeftToMatrix.symm ((↑M)⁻¹ᵀ * 1 * (↑M)ᵀ)
M:SL(2, ℂ)x:ℂ⊢ 1 = (↑M)⁻¹ᵀ * 1 * (↑M)ᵀ
All goals completed! 🐙
Applying the morphism dualLeftLeftUnit to 1 returns dualLeftLeftUnitVal.
lemma dualLeftLeftUnit_apply_one : dualLeftLeftUnit (1 : ℂ) = dualLeftLeftUnitVal := ⊢ dualLeftLeftUnit 1 = dualLeftLeftUnitVal
⊢ 1 • dualLeftLeftUnitVal = dualLeftLeftUnitVal
All goals completed! 🐙
The right-dual-right unit δ^{dot a}_{dot a} as an element of
(rightHanded ⊗ dualRightHanded).V.
def rightDualRightUnitVal : RightHandedWeyl ⊗[ℂ] DualRightHandedWeyl :=
rightDualRightToMatrix.symm 1
Expansion of rightDualRightUnitVal into the basis.
⊢ ∑ i, ∑ j, 1 i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j =
RightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 + RightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1
All goals completed! 🐙
The right-dual-right unit δ^{dot a}_{dot a} as a morphism
𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ dualRightHanded, manifesting
the invariance under the SL(2,ℂ) action.
M:SL(2, ℂ)x:ℂ⊢ (↑M)ᴴ⁻¹ * (↑M)ᴴ = 1
All goals completed! 🐙lemma rightDualRightUnit_apply_one : rightDualRightUnit (1 : ℂ) = rightDualRightUnitVal := ⊢ rightDualRightUnit 1 = rightDualRightUnitVal
⊢ 1 • rightDualRightUnitVal = rightDualRightUnitVal
All goals completed! 🐙
The dual-right-right unit δ_{dot a}^{dot a} as an element of
(rightHanded ⊗ dualRightHanded).V.
def dualRightRightUnitVal : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl) :=
dualRightRightToMatrix.symm 1
Expansion of dualRightRightUnitVal into the basis.
⊢ ∑ i, ∑ j, 1 i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j =
DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 + DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1
All goals completed! 🐙
The dual-right-right unit δ_{dot a}^{dot a} as a morphism
𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualRightHanded ⊗ rightHanded, manifesting
the invariance under the SL(2,ℂ) action.
M:SL(2, ℂ)x:ℂ⊢ (↑M)ᴴ⁻¹ * (↑M)ᴴ = 1
All goals completed! 🐙lemma dualRightRightUnit_apply_one : dualRightRightUnit (1 : ℂ) = dualRightRightUnitVal := ⊢ dualRightRightUnit 1 = dualRightRightUnitVal
⊢ 1 • dualRightRightUnitVal = dualRightRightUnitVal
All goals completed! 🐙Contraction of the units
Contraction on the right with dualLeftLeftUnit does nothing.
lemma contr_dualLeftLeftUnit (x : LeftHandedWeyl) :
(TensorProduct.lid ℂ _ <|
leftDualContraction.toLinearMap.rTensor _ <|
(TensorProduct.assoc ℂ _ _ _).symm <|
x ⊗ₜ[ℂ] (dualLeftLeftUnit (1 : ℂ))) = x := x:LeftHandedWeyl⊢ (TensorProduct.lid ℂ LeftHandedWeyl)
((LinearMap.rTensor LeftHandedWeyl leftDualContraction.toLinearMap)
((TensorProduct.assoc ℂ LeftHandedWeyl DualLeftHandedWeyl LeftHandedWeyl).symm (x ⊗ₜ[ℂ] dualLeftLeftUnit 1))) =
x
x:LeftHandedWeylc:Fin 2 → ℂhc:∑ i, c i • LeftHandedWeyl.basis i = x⊢ (TensorProduct.lid ℂ LeftHandedWeyl)
((LinearMap.rTensor LeftHandedWeyl leftDualContraction.toLinearMap)
((TensorProduct.assoc ℂ LeftHandedWeyl DualLeftHandedWeyl LeftHandedWeyl).symm (x ⊗ₜ[ℂ] dualLeftLeftUnit 1))) =
x
c:Fin 2 → ℂ⊢ (TensorProduct.lid ℂ LeftHandedWeyl)
((LinearMap.rTensor LeftHandedWeyl leftDualContraction.toLinearMap)
((TensorProduct.assoc ℂ LeftHandedWeyl DualLeftHandedWeyl LeftHandedWeyl).symm
((∑ i, c i • LeftHandedWeyl.basis i) ⊗ₜ[ℂ] dualLeftLeftUnit 1))) =
∑ i, c i • LeftHandedWeyl.basis i
All goals completed! 🐙
Contraction on the right with leftDualLeftUnit does nothing.
lemma contr_leftDualLeftUnit (x : DualLeftHandedWeyl) :
(TensorProduct.lid ℂ _ <|
dualLeftContraction.toLinearMap.rTensor _ <|
(TensorProduct.assoc ℂ _ _ _).symm <|
x ⊗ₜ[ℂ] (leftDualLeftUnit (1 : ℂ))) = x := x:DualLeftHandedWeyl⊢ (TensorProduct.lid ℂ DualLeftHandedWeyl)
((LinearMap.rTensor DualLeftHandedWeyl dualLeftContraction.toLinearMap)
((TensorProduct.assoc ℂ DualLeftHandedWeyl LeftHandedWeyl DualLeftHandedWeyl).symm
(x ⊗ₜ[ℂ] leftDualLeftUnit 1))) =
x
x:DualLeftHandedWeylc:Fin 2 → ℂhc:∑ i, c i • DualLeftHandedWeyl.basis i = x⊢ (TensorProduct.lid ℂ DualLeftHandedWeyl)
((LinearMap.rTensor DualLeftHandedWeyl dualLeftContraction.toLinearMap)
((TensorProduct.assoc ℂ DualLeftHandedWeyl LeftHandedWeyl DualLeftHandedWeyl).symm
(x ⊗ₜ[ℂ] leftDualLeftUnit 1))) =
x
c:Fin 2 → ℂ⊢ (TensorProduct.lid ℂ DualLeftHandedWeyl)
((LinearMap.rTensor DualLeftHandedWeyl dualLeftContraction.toLinearMap)
((TensorProduct.assoc ℂ DualLeftHandedWeyl LeftHandedWeyl DualLeftHandedWeyl).symm
((∑ i, c i • DualLeftHandedWeyl.basis i) ⊗ₜ[ℂ] leftDualLeftUnit 1))) =
∑ i, c i • DualLeftHandedWeyl.basis i
All goals completed! 🐙
Contraction on the right with dualRightRightUnit does nothing.
lemma contr_dualRightRightUnit (x : RightHandedWeyl) :
(TensorProduct.lid ℂ _ <|
rightDualContraction.toLinearMap.rTensor _ <|
(TensorProduct.assoc ℂ _ _ _).symm <|
x ⊗ₜ[ℂ] (dualRightRightUnit (1 : ℂ))) = x := x:RightHandedWeyl⊢ (TensorProduct.lid ℂ RightHandedWeyl)
((LinearMap.rTensor RightHandedWeyl rightDualContraction.toLinearMap)
((TensorProduct.assoc ℂ RightHandedWeyl DualRightHandedWeyl RightHandedWeyl).symm
(x ⊗ₜ[ℂ] dualRightRightUnit 1))) =
x
x:RightHandedWeylc:Fin 2 → ℂhc:∑ i, c i • RightHandedWeyl.basis i = x⊢ (TensorProduct.lid ℂ RightHandedWeyl)
((LinearMap.rTensor RightHandedWeyl rightDualContraction.toLinearMap)
((TensorProduct.assoc ℂ RightHandedWeyl DualRightHandedWeyl RightHandedWeyl).symm
(x ⊗ₜ[ℂ] dualRightRightUnit 1))) =
x
c:Fin 2 → ℂ⊢ (TensorProduct.lid ℂ RightHandedWeyl)
((LinearMap.rTensor RightHandedWeyl rightDualContraction.toLinearMap)
((TensorProduct.assoc ℂ RightHandedWeyl DualRightHandedWeyl RightHandedWeyl).symm
((∑ i, c i • RightHandedWeyl.basis i) ⊗ₜ[ℂ] dualRightRightUnit 1))) =
∑ i, c i • RightHandedWeyl.basis i
All goals completed! 🐙
Contraction on the right with rightDualRightUnit does nothing.
lemma contr_rightDualRightUnit (x : DualRightHandedWeyl) :
(TensorProduct.lid ℂ _ <|
dualRightContraction.toLinearMap.rTensor _ <|
(TensorProduct.assoc ℂ _ _ _).symm <|
x ⊗ₜ[ℂ] (rightDualRightUnit (1 : ℂ))) = x := x:DualRightHandedWeyl⊢ (TensorProduct.lid ℂ DualRightHandedWeyl)
((LinearMap.rTensor DualRightHandedWeyl dualRightContraction.toLinearMap)
((TensorProduct.assoc ℂ DualRightHandedWeyl RightHandedWeyl DualRightHandedWeyl).symm
(x ⊗ₜ[ℂ] rightDualRightUnit 1))) =
x
x:DualRightHandedWeylc:Fin 2 → ℂhc:∑ i, c i • DualRightHandedWeyl.basis i = x⊢ (TensorProduct.lid ℂ DualRightHandedWeyl)
((LinearMap.rTensor DualRightHandedWeyl dualRightContraction.toLinearMap)
((TensorProduct.assoc ℂ DualRightHandedWeyl RightHandedWeyl DualRightHandedWeyl).symm
(x ⊗ₜ[ℂ] rightDualRightUnit 1))) =
x
c:Fin 2 → ℂ⊢ (TensorProduct.lid ℂ DualRightHandedWeyl)
((LinearMap.rTensor DualRightHandedWeyl dualRightContraction.toLinearMap)
((TensorProduct.assoc ℂ DualRightHandedWeyl RightHandedWeyl DualRightHandedWeyl).symm
((∑ i, c i • DualRightHandedWeyl.basis i) ⊗ₜ[ℂ] rightDualRightUnit 1))) =
∑ i, c i • DualRightHandedWeyl.basis i
All goals completed! 🐙Symmetry properties of the units
⊢ DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 + DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 =
(LinearMap.lTensor DualLeftHandedWeyl ↑(LinearEquiv.refl ℂ LeftHandedWeyl))
((TensorProduct.comm ℂ LeftHandedWeyl DualLeftHandedWeyl)
(LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 +
LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1))
All goals completed! 🐙⊢ LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 =
(LinearMap.lTensor LeftHandedWeyl ↑(LinearEquiv.refl ℂ DualLeftHandedWeyl))
((TensorProduct.comm ℂ DualLeftHandedWeyl LeftHandedWeyl)
(DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 +
DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1))
All goals completed! 🐙⊢ DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 + DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 =
(LinearMap.lTensor DualRightHandedWeyl ↑(LinearEquiv.refl ℂ RightHandedWeyl))
((TensorProduct.comm ℂ RightHandedWeyl DualRightHandedWeyl)
(RightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 +
RightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1))
All goals completed! 🐙⊢ RightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 + RightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 =
(LinearMap.lTensor RightHandedWeyl ↑(LinearEquiv.refl ℂ DualRightHandedWeyl))
((TensorProduct.comm ℂ DualRightHandedWeyl RightHandedWeyl)
(DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 +
DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1))
All goals completed! 🐙