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.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.CliffordAlgebra

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

HepLean.SpaceTime.LorentzAlgebra.Basis

• Define the standard basis of the Lorentz algebra.

HepLean.SpaceTime.LorentzGroup.Basic

• Show that the Lorentz is a Lie group.

HepLean.SpaceTime.LorentzGroup.Boosts

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

HepLean.SpaceTime.LorentzGroup.Orthochronous

• Prove topological properties of the Orthochronous Lorentz Group.

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

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

HepLean.SpaceTime.LorentzTensor.Real.Basic

• Set up the notation 𝓛𝓣ℝ or similar.

HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix

• Generalize rep of Lorentz vector as a self-adjoint matrix to arbitrary dimension.

HepLean.SpaceTime.LorentzVector.Covariant

• Define equivariant map between contravariant and covariant lorentz tensors.

HepLean.SpaceTime.SL2C.Basic

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

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

• Prove dualizing indices for Einstein tensors does nothing.

HepLean.Tensors.IndexNotation.ColorIndexList.Basic

• orderEmbOfFin_univ should be replaced with a mathlib lemma if possible.

HepLean.Tensors.IndexNotation.IndexList.Basic

• Replace with Mathlib lemma.

HepLean.Tensors.IndexNotation.IndexList.CountId

• Replace with mathlib lemma.

HepLean.Tensors.IndexNotation.IndexList.Equivs

• Replace with a mathlib lemma.
• Replace with a mathlib lemma.

HepLean.Tensors.IndexNotation.IndexList.Normalize

• Replace with Mathlib lemma.
• Replace with Mathlib lemma.

HepLean.Tensors.IndexNotation.IndexString

• Move.

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 and Rel.

HepLean.Tensors.MulActionTensor

• Add preservation of the unit, and the metric.

HepLean.Tensors.RisingLowering

• Move