PhysLean/docs/_data/TODO.yml

##
# 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