From b5a22f96850e552347ffc05bc45526d9c503364f Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 16:31:26 -0400 Subject: [PATCH] docs: Add todos --- HepLean/AnomalyCancellation/Basic.lean | 8 +++----- HepLean/SpaceTime/CliffordAlgebra.lean | 8 ++------ HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 1 + HepLean/SpaceTime/LorentzGroup/Basic.lean | 9 ++------- HepLean/SpaceTime/LorentzGroup/Rotations.lean | 5 +---- HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean | 5 +---- HepLean/SpaceTime/SL2C/Basic.lean | 5 +---- HepLean/StandardModel/Basic.lean | 6 +----- HepLean/StandardModel/HiggsBoson/TargetSpace.lean | 2 ++ scripts/find_TODOs.lean | 2 -- 10 files changed, 14 insertions(+), 37 deletions(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index c44b98f..1a298cf 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -13,12 +13,10 @@ This file defines the basic structures for the anomaly cancellation conditions. It defines a module structure on the charges, and the solutions to the linear ACCs. -## TODO - -- Derive ACC systems from gauge algebras and fermionic representations. -- Relate ACCSystems to algebraic varieties. - -/ +/-! TODO: Derive an ACC system from a guage algebra and fermionic representations. -/ +/-! TODO: Relate ACC Systems to algebraic varieties. -/ +/-! TODO: Refactor whole file, and dependent files. -/ /-- A system of charges, specified by the number of charges. -/ structure ACCSystemCharges where diff --git a/HepLean/SpaceTime/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean index 99fec60..94ce6f7 100644 --- a/HepLean/SpaceTime/CliffordAlgebra.lean +++ b/HepLean/SpaceTime/CliffordAlgebra.lean @@ -9,13 +9,9 @@ import Mathlib.Analysis.Complex.Basic This file defines the Gamma matrices. -## TODO - -- Prove that the algebra generated by the gamma matrices is isomorphic to the - Clifford algebra associated with spacetime. -- Include relations for gamma matrices. -/ - +/-! TODO: Prove algebra generated by gamma matrices is isomorphic to Clifford algebra. -/ +/-! TODO: Define relations between the gamma matrices. -/ namespace spaceTime open Complex diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean index 45f9f44..36ae0f9 100644 --- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean +++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean @@ -15,3 +15,4 @@ This file is waiting for Lorentz Tensors to be done formally, before it can be completed. -/ +/-! TODO: Define the standard basis of the Lorentz algebra. -/ diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 61cb6c0..e47cb6a 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -10,18 +10,13 @@ import HepLean.SpaceTime.LorentzVector.NormOne We define the Lorentz group. -## TODO - -- Show that the Lorentz is a Lie group. -- Prove that the restricted Lorentz group is equivalent to the connected component of the -identity. -- Define the continuous maps from `ℝ³` to `restrictedLorentzGroup` defining boosts. - ## References - http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf -/ +/-! TODO: Show that the Lorentz is a Lie group. -/ +/-! TODO: Prove restricted Lorentz group equivalent to connected component of identity. -/ noncomputable section diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean index cdc9558..feee657 100644 --- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean +++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean @@ -11,11 +11,8 @@ import Mathlib.Topology.Constructions This file describes the embedding of `SO(3)` into `LorentzGroup 3`. -## TODO - -Generalize to arbitrary dimensions. - -/ +/-! TODO: Generalize the inclusion of rotations into LorentzGroup to abitary dimension. -/ noncomputable section namespace LorentzGroup diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean index b8399a8..08e04ce 100644 --- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean +++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean @@ -13,11 +13,8 @@ and the vector space of 2×2-complex self-adjoint matrices. In this file we define this linear equivalence in `toSelfAdjointMatrix`. -## TODO - -If possible generalize to arbitrary dimensions. - -/ +/-! TODO: Generalize rep of Lorentz vector as a self-adjoint matrix to arbitary dimension. -/ namespace SpaceTime open Matrix diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean index e58d09b..352fe81 100644 --- a/HepLean/SpaceTime/SL2C/Basic.lean +++ b/HepLean/SpaceTime/SL2C/Basic.lean @@ -124,12 +124,9 @@ def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where The homomorphism `toLorentzGroup` restricts to a homomorphism to the restricted Lorentz group. In this section we will define this homomorphism. -### TODO - -Complete this section. - -/ +/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/ end end SL2C diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean index 4f67a57..9d954fa 100644 --- a/HepLean/StandardModel/Basic.lean +++ b/HepLean/StandardModel/Basic.lean @@ -11,12 +11,8 @@ import Mathlib.LinearAlgebra.Matrix.ToLin This file defines the basic properties of the standard model in particle physics. -## TODO - -- Change the gauge group to a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆. -(see e.g. pg 97 of http://www.damtp.cam.ac.uk/user/tong/gaugetheory/gt.pdf) - -/ +/-! TODO: Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆. -/ universe v u namespace StandardModel diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean index d562b72..4876ea7 100644 --- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean +++ b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean @@ -27,6 +27,8 @@ This file is a import of `SM.HiggsBoson.Basic`. - We use conventions given in: [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx] -/ +/-! TODO: Move potential to a seperate file, and combine with HiggsBoson.Basic. -/ + universe v u namespace StandardModel noncomputable section diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean index 9faf776..3b73281 100644 --- a/scripts/find_TODOs.lean +++ b/scripts/find_TODOs.lean @@ -17,8 +17,6 @@ This program finds all instances of `/ TODO: ...` (without the `<>`) in HepLe Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`, authored by Michael Rothgang. - -- -/ open Lean System Meta