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

• replace Finsupp.equivFunOnFinite here with Finsupp.linearEquivFunOnFinite.

HepLean.AnomalyCancellation.PureU1.Even.BasisLinear

• Replace the definition of join with a Mathlib definition, most likely Sum.elim.

HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear

• Replace the definition of join with a Mathlib definition, most likely Sum.elim.

HepLean.AnomalyCancellation.PureU1.Permutations

• Replace the definition of pairSwap with Equiv.swap.

HepLean.AnomalyCancellation.PureU1.VectorLike

• Define vector like ACC in the n-odd case.

HepLean.BeyondTheStandardModel.TwoHDM.Basic

• Prove bounded properties of the 2HDM potential.

HepLean.Lorentz.Algebra.Basis

• Define the standard basis of the Lorentz algebra.

HepLean.Lorentz.ComplexTensor.Basis

• Generalize basis_eq_FD.

HepLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr

• Work out why pauliCo_prod_basis_expand' is needed.

HepLean.Lorentz.ComplexVector.Basic

• Rename.
• Include relation to real Lorentz vectors.

HepLean.Lorentz.Group.Basic

• Show that the Lorentz is a Lie group.

HepLean.Lorentz.Group.Boosts

• Show that generalised boosts are in the restricted Lorentz group.

HepLean.Lorentz.Group.Orthochronous

• Prove topological properties of the Orthochronous Lorentz Group.

HepLean.Lorentz.Group.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.Lorentz.Group.Rotations

• Generalize the inclusion of rotations into LorentzGroup to abitary dimension.

HepLean.Lorentz.SL2C.Basic

• Define homomorphism from SL(2, ℂ) to the restricted Lorentz group.

HepLean.Mathematics.LinearMaps

• Replace the definitions in this file with Mathlib definitions.

HepLean.Meta.AllFilePaths

• Make this definition more functional in style.

HepLean.Meta.Informal

• Derive a means to extract informal definitions and informal lemmas.
• Can likely make this a bona-fide command.

HepLean.Meta.TransverseTactics

• Find a way to free the enviroment env in transverseTactics.

HepLean.SpaceTime.Basic

• SpaceTime should be refactored into a structure, to prevent casting.

HepLean.SpaceTime.CliffordAlgebra

• Prove algebra generated by gamma matrices is isomorphic to Clifford algebra.
• Define relations between the gamma matrices.

HepLean.StandardModel.Basic

• Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆.

HepLean.StandardModel.HiggsBoson.Basic

• Make HiggsBundle an associated bundle.

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.OverColor.Discrete

• Find a better place for this.