TODO List
This is an automatically generated list of TODOs appearing as /-! TODO:...
in HepLean.
Please feel free to contribute to the completion of these tasks.
HepLean.AnomalyCancellation.Basic
- Derive an ACC system from a guage algebra and fermionic representations.
- Relate ACC Systems to algebraic varieties.
- Refactor whole file, and dependent files.
HepLean.AnomalyCancellation.PureU1.BasisLinear
HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
HepLean.AnomalyCancellation.PureU1.Permutations
HepLean.AnomalyCancellation.PureU1.VectorLike
HepLean.BeyondTheStandardModel.TwoHDM.Basic
HepLean.Mathematics.LinearMaps
HepLean.Meta.AllFilePaths
HepLean.Meta.Informal
- Derive a means to extract informal definitions and informal lemmas.
- Can likely make this a bona-fide command.
HepLean.Meta.TransverseTactics
HepLean.SpaceTime.CliffordAlgebra
- Prove algebra generated by gamma matrices is isomorphic to Clifford algebra.
- Define relations between the gamma matrices.
HepLean.SpaceTime.LorentzAlgebra.Basis
HepLean.SpaceTime.LorentzGroup.Basic
HepLean.SpaceTime.LorentzGroup.Boosts
HepLean.SpaceTime.LorentzGroup.Orthochronous
HepLean.SpaceTime.LorentzGroup.Restricted
- Add definition of the restricted Lorentz group.
- Prove member of the restricted Lorentz group is combo of boost and rotation.
- Prove restricted Lorentz group equivalent to connected component of identity.
HepLean.SpaceTime.LorentzGroup.Rotations
HepLean.SpaceTime.LorentzTensor.Real.Basic
HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
HepLean.SpaceTime.LorentzVector.Covariant
HepLean.SpaceTime.SL2C.Basic
HepLean.StandardModel.Basic
HepLean.StandardModel.HiggsBoson.Basic
HepLean.StandardModel.HiggsBoson.GaugeAction
- Currently this only contains the action of the global gauge group. Generalize.
- Define the global gauge action on HiggsField.
- Prove
⟪φ1, φ2⟫_H
invariant under the global gauge action. (norm_map_of_mem_unitary) - Prove invariance of potential under global gauge action.
HepLean.Tensors.Basic
- Replace with dependent type version of
MultilinearMap.domCoprod
when in Mathlib. - Replace with dependent type version of
PiTensorProduct.tmulEquiv
when in Mathlib. - Delete the content of this section.
HepLean.Tensors.EinsteinNotation.RisingLowering
HepLean.Tensors.IndexNotation.ColorIndexList.Basic
HepLean.Tensors.IndexNotation.IndexList.Basic
HepLean.Tensors.IndexNotation.IndexList.CountId
HepLean.Tensors.IndexNotation.IndexList.Equivs
HepLean.Tensors.IndexNotation.IndexList.Normalize
HepLean.Tensors.IndexNotation.IndexString
HepLean.Tensors.IndexNotation.TensorIndex
- Introduce a way to change an index from e.g.
ᵘ¹
toᵘ²
. - Show that the product is well defined with respect to Rel.
- Prove properties regarding the interaction of
ProdCond
andRel
.