Imports
/-
Copyright (c) 2026 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.DualRightHandedDuals for fermions
In this file we give the relationship between Weyl fermions and their duals.
@[expose] public sectionDuals of Weyl fermions
The dual of LeftHandedWeyl is DualLeftHandedWeyl, and the dual of RightHandedWeyl is
DualRightHandedWeyl.
The morphism between the representation leftHanded and the representation
dualLeftHanded defined by multiplying an element of
leftHanded by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].
M:SL(2, ℂ)ψ:LeftHandedWeyl⊢ !![0 * ↑M 0 0 + 1 * ↑M 1 0, 0 * ↑M 0 1 + 1 * ↑M 1 1; -1 * ↑M 0 0 + 0 * ↑M 1 0, -1 * ↑M 0 1 + 0 * ↑M 1 1] =
!![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 1;
!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 1] *
!![0, 1; -1, 0]
All goals completed! 🐙lemma LeftHandedWeyl.dual_hom_apply (ψ : LeftHandedWeyl) :
LeftHandedWeyl.dual ψ =
DualLeftHandedWeyl.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
The morphism from dualLeftHanded to
leftHanded defined by multiplying an element of
DualLeftHandedWeyl by the matrix εₐ₁ₐ₂ = !![0, -1; 1, 0].
M:SL(2, ℂ)ψ:DualLeftHandedWeyl⊢ !![0, -1; 1, 0] *
!![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 1;
!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 1] =
!![↑M 0 0 * 0 + ↑M 0 1 * 1, ↑M 0 0 * -1 + ↑M 0 1 * 0; ↑M 1 0 * 0 + ↑M 1 1 * 1, ↑M 1 0 * -1 + ↑M 1 1 * 0]
All goals completed! 🐙lemma DualLeftHandedWeyl.dual_hom_apply (ψ : DualLeftHandedWeyl) :
DualLeftHandedWeyl.dual ψ =
LeftHandedWeyl.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
The equivalence between the representation leftHanded and the representation
dualLeftHanded defined by multiplying an element of
leftHanded by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].
ψ:DualLeftHandedWeyl⊢ DualLeftHandedWeyl.toFin2ℂEquiv.symm ψ.toFin2ℂ = ψ
All goals completed! 🐙
leftHandedDualEquiv acting on an element ψ : leftHanded corresponds
to multiplying ψ by the matrix !![0, 1; -1, 0].
lemma LeftHandedWeyl.dualEquiv_hom_hom_apply (ψ : LeftHandedWeyl) :
LeftHandedWeyl.dualEquiv ψ =
DualLeftHandedWeyl.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
The inverse of leftHandedDualEquiv acting on an elementψ : dualLeftHanded corresponds
to multiplying ψ by the matrix !![0, -1; 1, 0].
lemma LeftHandedWeyl.dualEquiv_inv_hom_apply (ψ : DualLeftHandedWeyl) :
LeftHandedWeyl.dualEquiv.symm ψ =
LeftHandedWeyl.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
The linear equivalence between rightHandedWeyl and DualRightHandedWeyl given by multiplying
an element of rightHandedWeyl by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].
informal_definition RightHandedWeyl.dualEquiv where
deps := [``RightHandedWeyl, ``DualRightHandedWeyl]
tag := "6VZR4"
The linear equivalence rightHandedWeylDualEquiv is equivariant with respect to the action of
SL(2,C) on rightHandedWeyl and DualRightHandedWeyl.
informal_lemma RightHandedWeyl.dualEquiv_equivariant where
deps := [``RightHandedWeyl.dualEquiv]
tag := "6VZSG"