-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #291 from HEPLean/Docs
Create TODO.yml
- Loading branch information
Showing
1 changed file
with
190 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,190 @@ | ||
| ## | ||
| # This file is generated by the `lake exe TODO_to_yml mkFile` command. | ||
| # Do not edit manually. | ||
| - content: "Refactor whole file, and dependent files." | ||
| file: HepLean.AnomalyCancellation.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L19 | ||
| line: 19 | ||
|
|
||
| - content: "Relate ACC Systems to algebraic varieties." | ||
| file: HepLean.AnomalyCancellation.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L18 | ||
| line: 18 | ||
|
|
||
| - content: "Derive an ACC system from a guage algebra and fermionic representations." | ||
| file: HepLean.AnomalyCancellation.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/Basic.lean#L17 | ||
| line: 17 | ||
|
|
||
| - content: "replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`." | ||
| file: HepLean.AnomalyCancellation.PureU1.BasisLinear | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean#L78 | ||
| line: 78 | ||
|
|
||
| - content: "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`." | ||
| file: HepLean.AnomalyCancellation.PureU1.Even.BasisLinear | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean#L619 | ||
| line: 619 | ||
|
|
||
| - content: "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`." | ||
| file: HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean#L626 | ||
| line: 626 | ||
|
|
||
| - content: "Replace the definition of `pairSwap` with `Equiv.swap`." | ||
| file: HepLean.AnomalyCancellation.PureU1.Permutations | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/Permutations.lean#L92 | ||
| line: 92 | ||
|
|
||
| - content: "Define vector like ACC in the `n`-odd case." | ||
| file: HepLean.AnomalyCancellation.PureU1.VectorLike | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/AnomalyCancellation/PureU1/VectorLike.lean#L13 | ||
| line: 13 | ||
|
|
||
| - content: "Prove bounded properties of the 2HDM potential. | ||
| See e.g. https://inspirehep.net/literature/201299 and | ||
| https://arxiv.org/pdf/hep-ph/0605184." | ||
| file: HepLean.BeyondTheStandardModel.TwoHDM.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean#L148 | ||
| line: 148 | ||
|
|
||
| - content: "Define the standard basis of the Lorentz algebra." | ||
| file: HepLean.Lorentz.Algebra.Basis | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Algebra/Basis.lean#L19 | ||
| line: 19 | ||
|
|
||
| - content: "Generalize `basis_eq_FD`." | ||
| file: HepLean.Lorentz.ComplexTensor.Basis | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexTensor/Basis.lean#L51 | ||
| line: 51 | ||
|
|
||
| - content: "Work out why `pauliCo_prod_basis_expand'` is needed." | ||
| file: HepLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean#L391 | ||
| line: 391 | ||
|
|
||
| - content: "Include relation to real Lorentz vectors." | ||
| file: HepLean.Lorentz.ComplexVector.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexVector/Basic.lean#L144 | ||
| line: 144 | ||
|
|
||
| - content: "Rename." | ||
| file: HepLean.Lorentz.ComplexVector.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/ComplexVector/Basic.lean#L132 | ||
| line: 132 | ||
|
|
||
| - content: "Show that the Lorentz group is a Lie group." | ||
| file: HepLean.Lorentz.Group.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Basic.lean#L18 | ||
| line: 18 | ||
|
|
||
| - content: "Show that generalised boosts are in the restricted Lorentz group." | ||
| file: HepLean.Lorentz.Group.Boosts | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Boosts.lean#L24 | ||
| line: 24 | ||
|
|
||
| - content: "Prove topological properties of the Orthochronous Lorentz Group." | ||
| file: HepLean.Lorentz.Group.Orthochronous | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Orthochronous.lean#L15 | ||
| line: 15 | ||
|
|
||
| - content: "Prove restricted Lorentz group equivalent to connected component of identity." | ||
| file: HepLean.Lorentz.Group.Restricted | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L15 | ||
| line: 15 | ||
|
|
||
| - content: "Add definition of the restricted Lorentz group." | ||
| file: HepLean.Lorentz.Group.Restricted | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L13 | ||
| line: 13 | ||
|
|
||
| - content: "Prove member of the restricted Lorentz group is combo of boost and rotation." | ||
| file: HepLean.Lorentz.Group.Restricted | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Restricted.lean#L14 | ||
| line: 14 | ||
|
|
||
| - content: "Generalize the inclusion of rotations into LorentzGroup to abitary dimension." | ||
| file: HepLean.Lorentz.Group.Rotations | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/Group/Rotations.lean#L14 | ||
| line: 14 | ||
|
|
||
| - content: "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group." | ||
| file: HepLean.Lorentz.SL2C.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Lorentz/SL2C/Basic.lean#L315 | ||
| line: 315 | ||
|
|
||
| - content: "Replace the definitions in this file with Mathlib definitions." | ||
| file: HepLean.Mathematics.LinearMaps | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Mathematics/LinearMaps.lean#L17 | ||
| line: 17 | ||
|
|
||
| - content: "Make this definition more functional in style." | ||
| file: HepLean.Meta.AllFilePaths | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/AllFilePaths.lean#L16 | ||
| line: 16 | ||
|
|
||
| - content: "Can likely make this a bona-fide command." | ||
| file: HepLean.Meta.Informal.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/Informal/Basic.lean#L20 | ||
| line: 20 | ||
|
|
||
| - content: "Find a way to free the environment `env` in `transverseTactics`. | ||
| This leads to memory problems when using `transverseTactics` directly in loops." | ||
| file: HepLean.Meta.TransverseTactics | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Meta/TransverseTactics.lean#L78 | ||
| line: 78 | ||
|
|
||
| - content: "Split the following two lemmas up into smaller parts." | ||
| file: HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean#L374 | ||
| line: 374 | ||
|
|
||
| - content: "SpaceTime should be refactored into a structure, to prevent casting." | ||
| file: HepLean.SpaceTime.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/Basic.lean#L18 | ||
| line: 18 | ||
|
|
||
| - content: "Prove algebra generated by gamma matrices is isomorphic to Clifford algebra." | ||
| file: HepLean.SpaceTime.CliffordAlgebra | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/CliffordAlgebra.lean#L14 | ||
| line: 14 | ||
|
|
||
| - content: "Define relations between the gamma matrices." | ||
| file: HepLean.SpaceTime.CliffordAlgebra | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/SpaceTime/CliffordAlgebra.lean#L15 | ||
| line: 15 | ||
|
|
||
| - content: "Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆." | ||
| file: HepLean.StandardModel.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/Basic.lean#L15 | ||
| line: 15 | ||
|
|
||
| - content: "Make `HiggsBundle` an associated bundle." | ||
| file: HepLean.StandardModel.HiggsBoson.Basic | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/Basic.lean#L82 | ||
| line: 82 | ||
|
|
||
| - content: "Define the global gauge action on HiggsField." | ||
| file: HepLean.StandardModel.HiggsBoson.GaugeAction | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L239 | ||
| line: 239 | ||
|
|
||
| - content: "Prove invariance of potential under global gauge action." | ||
| file: HepLean.StandardModel.HiggsBoson.GaugeAction | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L241 | ||
| line: 241 | ||
|
|
||
| - content: "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)" | ||
| file: HepLean.StandardModel.HiggsBoson.GaugeAction | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L240 | ||
| line: 240 | ||
|
|
||
| - content: "Currently this only contains the action of the global gauge group. Generalize." | ||
| file: HepLean.StandardModel.HiggsBoson.GaugeAction | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/StandardModel/HiggsBoson/GaugeAction.lean#L16 | ||
| line: 16 | ||
|
|
||
| - content: "Find a better place for this." | ||
| file: HepLean.Tensors.OverColor.Discrete | ||
| githubLink: https://github.com/HEPLean/HepLean/blob/master/HepLean/Tensors/OverColor/Discrete.lean#L159 | ||
| line: 159 |