Merge pull request #297 from HEPLean/TODOList_Improve

refactor: Improve todos and remove ambiguous
HEPLean · Jan 24, 2025 · 2c51e87 · 2c51e87
2 parents 5347648 + 3740b5b
commit 2c51e87
Show file tree

Hide file tree

Showing 13 changed files with 26 additions and 17 deletions.
diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
@@ -14,9 +14,11 @@ 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 an ACC system from a gauge algebra and fermionic representations."
-TODO "Relate ACC Systems to algebraic varieties."
-TODO "Refactor whole file, and dependent files."
+TODO "Anomaly cancellation conditions can be derived formally from the gauge group
+  and fermionic representations using e.g. topological invariants. Include such a
+  definition."
+TODO "Anomaly cancellation conditions can be defined using algebraic varieties.
+  Link such an approach to the approach here."
 
 /-- A system of charges, specified by the number of charges. -/
 structure ACCSystemCharges where

diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -75,7 +75,8 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
   sum_of_anomaly_free_linear (fun i => f i) j
 
-TODO "replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`."
+TODO "The definition of `coordinateMap` here may be improved by replacing
+   `Finsupp.equivFunOnFinite` with `Finsupp.linearEquivFunOnFinite`. Investigate this."
 /-- The coordinate map for the basis. -/
 noncomputable
 def coordinateMap : (PureU1 n.succ).LinSols ≃ₗ[ℚ] Fin n →₀ ℚ where

diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -89,7 +89,7 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
     ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
   rfl
 
-TODO "Replace the definition of `pairSwap` with `Equiv.swap`."
+TODO "Remove `pairSwap`, and use the Mathlib defined function `Equiv.swap` instead."
 /-- The permutation which swaps i and j. -/
 def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
   toFun s :=

diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@@ -10,7 +10,6 @@ import HepLean.AnomalyCancellation.PureU1.Sorts
 For the `n`-even case we define the property of a charge assignment being vector like.
 
 -/
-TODO "Define vector like ACC in the `n`-odd case."
 universe v u
 
 open Nat

diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
@@ -388,7 +388,11 @@ lemma pauliMatrix_contr_lower_3_1_1 :
   · congr 2
     decide
 
-TODO "Work out why `pauliCo_prod_basis_expand'` is needed."
+TODO "Work out why `pauliCo_prod_basis_expand'` is needed, since it is exactly the same
+  as `pauliCo_prod_basis_expand` which is defined in another file. One will see that
+  replacing instances of `pauliCo_prod_basis_expand'` with `pauliCo_prod_basis_expand`
+  does not work."
+
 /-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
   It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
   `pauliMatrix_lower_basis_expand_prod` does not work. -/

diff --git a/HepLean/Lorentz/ComplexVector/Basic.lean b/HepLean/Lorentz/ComplexVector/Basic.lean
@@ -129,7 +129,6 @@ lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
   rw [LorentzGroup.toComplex_mulVec_ofReal]
   rfl
 
-TODO "Rename."
 lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
     (complexContr.ρ M) (complexContrBasis i) =
     ∑ j, (SL2C.toLorentzGroup M).1 j i •
@@ -141,6 +140,5 @@ lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
   simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
   rw [complexContrBasis_of_real]
 
-TODO "Include relation to real Lorentz vectors."
 end Lorentz
 end
diff --git a/HepLean/Lorentz/Group/Basic.lean b/HepLean/Lorentz/Group/Basic.lean
@@ -15,7 +15,7 @@ We define the Lorentz group.
 - http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
 
 -/
-TODO "Show that the Lorentz group is a Lie group."
+TODO "Define the Lie group structure on the Lorentz group."
 
 noncomputable section
 

diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean
@@ -21,7 +21,6 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`.
   https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
 
 -/
-TODO "Show that generalised boosts are in the restricted Lorentz group."
 noncomputable section
 
 namespace LorentzGroup
@@ -204,10 +203,14 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor
   refine hn _ ?_ h1
   simpa using (FuturePointing.one_add_metric_non_zero u v)
 
+TODO "Make `toLorentz` the definition of a generalised boost. This will involve
+  refactoring this file."
 /-- A generalised boost as an element of the Lorentz Group. -/
 def toLorentz (u v : FuturePointing d) : LorentzGroup d :=
   ⟨toMatrix u v, toMatrix_in_lorentzGroup u v⟩
 
+TODO "Show that generalised boosts are in the restricted Lorentz group."
+
 lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) := by
   refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)
   exact toMatrix_continuous u

diff --git a/HepLean/Lorentz/Group/Restricted.lean b/HepLean/Lorentz/Group/Restricted.lean
@@ -11,8 +11,10 @@ This file is currently a stub.
 
 -/
 TODO "Add definition of the restricted Lorentz group."
-TODO "Prove member of the restricted Lorentz group is combo of boost and rotation."
-TODO "Prove restricted Lorentz group equivalent to connected component of identity."
+TODO "Prove that every member of the restricted Lorentz group is
+  combiniation of a boost and a rotation."
+TODO "Prove restricted Lorentz group equivalent to connected component of identity
+  of the Lorentz group."
 
 noncomputable section
 

diff --git a/HepLean/Meta/AllFilePaths.lean b/HepLean/Meta/AllFilePaths.lean
@@ -13,7 +13,7 @@ import HepLean.Meta.TODO.Basic
 
 open Lean Elab System
 
-TODO "Make this definition more functional in style."
+TODO "Make this definition more functional in style. In other words, remove the for loop."
 
 /-- The recursive function underlying `allFilePaths`. -/
 partial def allFilePaths.go (prev : Array FilePath)

diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
@@ -15,7 +15,7 @@ This file introduce 4d Minkowski spacetime.
 
 noncomputable section
 
-TODO "SpaceTime should be refactored into a structure, to prevent casting."
+TODO "SpaceTime should be refactored into a structure, or similar, to prevent casting."
 
 /-- The space-time -/
 def SpaceTime : Type := Fin 4 → ℝ

diff --git a/HepLean/SpaceTime/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean
@@ -12,7 +12,6 @@ This file defines the 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/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@@ -13,7 +13,8 @@ import Mathlib.Analysis.InnerProductSpace.Adjoint
 # The action of the gauge group on the Higgs field
 
 -/
-TODO "Currently this only contains the action of the global gauge group. Generalize."
+TODO "Currently this only contains the action of the global gauge group. Generalize
+  to include the full action of the gauge group."
 noncomputable section
 
 namespace StandardModel