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.LeftHanded
public import Physlib.Relativity.Fermions.Weyl.RightHanded
public import Physlib.Relativity.Fermions.Weyl.DualLeftHanded
public import Physlib.Relativity.Fermions.Weyl.DualRightHandedContraction of Weyl fermions
We define the contraction of Weyl fermions.
@[expose] public sectionContraction of Weyl fermions.
The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a dual-left-handed Weyl fermion.
r:ℂψ:LeftHandedWeylφ:DualLeftHandedWeyl⊢ r • (LeftHandedWeyl.toFin2ℂEquiv ψ ⬝ᵥ φ.toFin2ℂ) =
((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
All goals completed! 🐙The bi-linear map corresponding to contraction of a dual-left-handed Weyl fermion with a left-handed Weyl fermion.
ψ:DualLeftHandedWeylr:ℂφ:LeftHandedWeyl⊢ r • (ψ.toFin2ℂ ⬝ᵥ LeftHandedWeyl.toFin2ℂEquiv φ) = (RingHom.id ℂ) r • (ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ)
All goals completed! 🐙}
map_add' ψ ψ':= ψ:DualLeftHandedWeylψ':DualLeftHandedWeyl⊢ { toFun := fun φ => (ψ + ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } =
{ toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }
ψ:DualLeftHandedWeylψ':DualLeftHandedWeylφ:LeftHandedWeyl⊢ { toFun := fun φ => (ψ + ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
({ toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ })
φ
All goals completed! 🐙
map_smul' ψ ψ' := ψ:ℂψ':DualLeftHandedWeyl⊢ { toFun := fun φ => (ψ • ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } =
(RingHom.id ℂ) ψ • { toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }
ψ:ℂψ':DualLeftHandedWeylφ:LeftHandedWeyl⊢ { toFun := fun φ => (ψ • ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
((RingHom.id ℂ) ψ • { toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
All goals completed! 🐙The bi-linear map corresponding to contraction of a right-handed Weyl fermion with a dual-right-handed Weyl fermion.
r:ℂψ:RightHandedWeylφ:DualRightHandedWeyl⊢ r • (RightHandedWeyl.toFin2ℂEquiv ψ ⬝ᵥ φ.toFin2ℂ) =
((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
All goals completed! 🐙The bi-linear map corresponding to contraction of a dual-right-handed Weyl fermion with a right-handed Weyl fermion.
ψ:DualRightHandedWeylr:ℂφ:RightHandedWeyl⊢ r • (ψ.toFin2ℂ ⬝ᵥ RightHandedWeyl.toFin2ℂEquiv φ) = (RingHom.id ℂ) r • (ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ)
All goals completed! 🐙}
map_add' ψ ψ':= ψ:DualRightHandedWeylψ':DualRightHandedWeyl⊢ { toFun := fun φ => (ψ + ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } =
{ toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }
ψ:DualRightHandedWeylψ':DualRightHandedWeylφ:RightHandedWeyl⊢ { toFun := fun φ => (ψ + ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
({ toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ })
φ
All goals completed! 🐙
map_smul' ψ ψ' := ψ:ℂψ':DualRightHandedWeyl⊢ { toFun := fun φ => (ψ • ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } =
(RingHom.id ℂ) ψ • { toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }
ψ:ℂψ':DualRightHandedWeylφ:RightHandedWeyl⊢ { toFun := fun φ => (ψ • ψ').toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
((RingHom.id ℂ) ψ • { toFun := fun φ => ψ'.toFin2ℂ ⬝ᵥ φ.toFin2ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
All goals completed! 🐙The linear map from leftHandedWeyl ⊗ DualLeftHandedWeyl to ℂ given by summing over components of leftHandedWeyl and DualLeftHandedWeyl in the standard basis (i.e. the dot product). Physically, the contraction of a left-handed Weyl fermion with a dual-left-handed Weyl fermion. In index notation this is ψ^a φ_a.
M:SL(2, ℂ)ψ:LeftHandedWeylφ:DualLeftHandedWeyl⊢ ((↑M)⁻¹ * ↑M) *ᵥ ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
All goals completed! 🐙lemma leftDualContraction_hom_tmul (ψ : LeftHandedWeyl)
(φ : DualLeftHandedWeyl) :
leftDualContraction (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := ψ:LeftHandedWeylφ:DualLeftHandedWeyl⊢ leftDualContraction (ψ ⊗ₜ[ℂ] φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
All goals completed! 🐙i:Fin 2j:Fin 2⊢ (if j = i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (if ↑j = ↑i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (↑j = ↑i) = (↑i = ↑j)
All goals completed! 🐙The linear map from DualLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by summing over components of DualLeftHandedWeyl and leftHandedWeyl in the standard basis (i.e. the dot product). Physically, the contraction of a dual-left-handed Weyl fermion with a left-handed Weyl fermion. In index notation this is φ_a ψ^a.
M:SL(2, ℂ)φ:DualLeftHandedWeylψ:LeftHandedWeyl⊢ φ.toFin2ℂ ᵥ* ((↑M)⁻¹ * ↑M) ⬝ᵥ ψ.toFin2ℂ = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
All goals completed! 🐙lemma dualLeftContraction_hom_tmul (φ : DualLeftHandedWeyl) (ψ : LeftHandedWeyl) :
dualLeftContraction (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := φ:DualLeftHandedWeylψ:LeftHandedWeyl⊢ dualLeftContraction (φ ⊗ₜ[ℂ] ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
All goals completed! 🐙i:Fin 2j:Fin 2⊢ (if j = i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (if ↑j = ↑i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (↑j = ↑i) = (↑i = ↑j)
All goals completed! 🐙
The linear map from rightHandedWeyl ⊗ DualRightHandedWeyl to ℂ given by
summing over components of rightHandedWeyl and DualRightHandedWeyl in the
standard basis (i.e. the dot product).
The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
In index notation this is ψ^{dot a} φ_{dot a}.
M:SL(2, ℂ)ψ:RightHandedWeylφ:DualRightHandedWeylh1:(↑M)⁻¹ᴴ = ((↑M)⁻¹.map star)ᵀh2:(↑M)⁻¹.map star * (↑M).map star = 1⊢ 1 *ᵥ ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
All goals completed! 🐙lemma rightDualContraction_hom_tmul (ψ : RightHandedWeyl)
(φ : DualRightHandedWeyl) :
rightDualContraction (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := ψ:RightHandedWeylφ:DualRightHandedWeyl⊢ rightDualContraction (ψ ⊗ₜ[ℂ] φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
All goals completed! 🐙i:Fin 2j:Fin 2⊢ (if j = i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (if ↑j = ↑i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (↑j = ↑i) = (↑i = ↑j)
All goals completed! 🐙The linear map from DualRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by summing over components of DualRightHandedWeyl and rightHandedWeyl in the standard basis (i.e. the dot product). The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion. In index notation this is φ_{dot a} ψ^{dot a}.
M:SL(2, ℂ)φ:DualRightHandedWeylψ:RightHandedWeylh1:(↑M)⁻¹ᴴ = ((↑M)⁻¹.map star)ᵀh2:(↑M)⁻¹.map star * (↑M).map star = 1⊢ φ.toFin2ℂ ᵥ* 1 ⬝ᵥ ψ.toFin2ℂ = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
All goals completed! 🐙lemma dualRightContraction_hom_tmul (φ : DualRightHandedWeyl)
(ψ : RightHandedWeyl) :
dualRightContraction (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := φ:DualRightHandedWeylψ:RightHandedWeyl⊢ dualRightContraction (φ ⊗ₜ[ℂ] ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
All goals completed! 🐙i:Fin 2j:Fin 2⊢ (if j = i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (if ↑j = ↑i then 1 else 0) = if ↑i = ↑j then 1 else 0
i:Fin 2j:Fin 2⊢ (↑j = ↑i) = (↑i = ↑j)
All goals completed! 🐙Symmetry properties
All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙