TODO list

This file is created automatically using `TODO ...` commands within PhysLean. Feel free to tackle any of the items here.

In: PhysLean.Mathematics.LinearMaps

Replace the definitions in this file with Mathlib definitions.

In: PhysLean.Meta.AllFilePaths

Make this definition more functional in style. In other words, remove the for loop.

In: PhysLean.Meta.TransverseTactics

Find a way to free the environment `env` in `transverseTactics`. This leads to memory problems when using `transverseTactics` directly in loops.

In: PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic

Prove bounded properties of the 2HDM potential. See e.g. https://inspirehep.net/literature/201299 and https://arxiv.org/pdf/hep-ph/0605184.

In: PhysLean.Particles.StandardModel.Basic

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

In: PhysLean.Particles.StandardModel.HiggsBoson.Basic

Make `HiggsBundle` an associated bundle.

In: PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction

Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)

In: PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction

Currently this only contains the action of the global gauge group. Generalize to include the full action of the gauge group.

In: PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction

Define the global gauge action on HiggsField.

In: PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction

Prove invariance of potential under global gauge action.

In: PhysLean.QFT.AnomalyCancellation.Basic

Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here.

In: PhysLean.QFT.AnomalyCancellation.Basic

Anomaly cancellation conditions can be derived formally from the gauge group and fermionic representations using e.g. topological invariants. Include such a definition.

In: PhysLean.QFT.AnomalyCancellation.PureU1.BasisLinear

The definition of `coordinateMap` here may be improved by replacing `Finsupp.equivFunOnFinite` with `Finsupp.linearEquivFunOnFinite`. Investigate this.

In: PhysLean.QFT.AnomalyCancellation.PureU1.Even.BasisLinear

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

In: PhysLean.QFT.AnomalyCancellation.PureU1.Odd.BasisLinear

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

In: PhysLean.QFT.AnomalyCancellation.PureU1.Permutations

Remove `pairSwap`, and use the Mathlib defined function `Equiv.swap` instead.

In: PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder

Split the following two lemmas up into smaller parts.

In: PhysLean.QuantumMechanics.FiniteTarget.Basic

Define a smooth structure on `FiniteTarget`.

In: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic

The momentum operator should be moved to a more general file.

In: PhysLean.Relativity.Lorentz.Algebra.Basis

Define the standard basis of the Lorentz algebra.

In: PhysLean.Relativity.Lorentz.Bispinors.Basic

To increase the speed of these files `(vecNodeE complexLorentzTensor .up p).tensor | μ` is written out expliclity. Notation should be introduced so that we can just write `p | μ` or similar without slowing things down. This can be done by redefining bispinors in terms of actual tensors.

In: PhysLean.Relativity.Lorentz.ComplexTensor.Basis

Replace basisVector in this file with TensorSpecies.tensorBasis. All of the results here should be generalized to TensorSpecies.tensorBasis.

In: PhysLean.Relativity.Lorentz.Group.Basic

Define the Lie group structure on the Lorentz group.

In: PhysLean.Relativity.Lorentz.Group.Boosts

Show that generalised boosts are in the restricted Lorentz group.

In: PhysLean.Relativity.Lorentz.Group.Boosts

Make `toLorentz` the definition of a generalised boost. This will involve refactoring this file.

In: PhysLean.Relativity.Lorentz.Group.Orthochronous

Prove topological properties of the Orthochronous Lorentz Group.

In: PhysLean.Relativity.Lorentz.Group.Restricted

Add definition of the restricted Lorentz group.

In: PhysLean.Relativity.Lorentz.Group.Restricted

Prove restricted Lorentz group equivalent to connected component of identity of the Lorentz group.

In: PhysLean.Relativity.Lorentz.Group.Restricted

Prove that every member of the restricted Lorentz group is combiniation of a boost and a rotation.

In: PhysLean.Relativity.Lorentz.Group.Rotations

Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension.

In: PhysLean.Relativity.Lorentz.SL2C.Basic

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

In: PhysLean.Relativity.SpaceTime.Basic

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

In: PhysLean.Relativity.SpaceTime.CliffordAlgebra

Prove algebra generated by gamma matrices is isomorphic to Clifford algebra.

In: PhysLean.Relativity.Tensors.OverColor.Discrete

Find a better place for this.

In: PhysLean.Relativity.Tensors.Tree.Basic

Fill in the other relationships between tensor trees and tensor basis.