API: Lorentz Group #885
Description
Key data structure
The key data structure here is the Lorentz group, which is the key symmetry group of Minkowski SpaceTime.
- is defined
Need
This API is needed throughout the project, we use it to define Lorentz tensors which are the foundations to the definition of SpaceTime and many other quantities in the project, such as fermions, the Electromangetic potential etc.
Requirements
- Instance as a group
- Instance as a Lie group
- Inclusion of boosts
- Inclusion of rotations
- Different membership conditions
- Definition of proper Lorentz transforms
- Definition of orthochronous Lorentz transforms
- Definition of the restricted Lorentz group
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Relativity/LorentzGroup