Skip to content

auto-task(Fermion.dirac): record TODO to add Dirac fermion representations and Color #1317

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jstoobysmith wants to merge 2 commits into
base: master
Choose a base branch
from
Open

auto-task(Fermion.dirac): record TODO to add Dirac fermion representations and Color #1317

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a282077
auto-task(Fermion.dirac): record TODO to add Dirac fermion representa…
jstoobysmith Jun 29, 2026
5e23ce1
feat: Fix axion addition
jstoobysmith Jul 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,12 @@ TODO "Rename the Weyl fermion representations `leftHandedRep`, `dualLeftHandedRe
respectively, so that each representation lives in the namespace of the module it
acts on, and update all references accordingly."

TODO "Define the Dirac and dual-Dirac fermion representations `Fermion.dirac` and
`Fermion.dualDirac` (built from the left- and right-handed Weyl representations
`leftHandedRep`/`rightHandedRep` and their duals), and incorporate them into
`complexLorentzTensor` by adding the corresponding `complexLorentzTensor.Color`
constructors."

/-- The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
In index notation corresponds to a Weyl fermion with indices ψ^a. -/
def leftHandedRep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where
Expand Down
Loading