diff --git a/Physlib/Relativity/LorentzGroup/API-map.yaml b/Physlib/Relativity/LorentzGroup/API-map.yaml new file mode 100644 index 000000000..d3d0365ed --- /dev/null +++ b/Physlib/Relativity/LorentzGroup/API-map.yaml @@ -0,0 +1,61 @@ +version: v0.1 + +Title: "Lorentz Group" + +Overview: | + The Lorentz group is the group of matrices preserving the Minkowski metric, + defined as matrices satisfying Λ * dual Λ = 1. It is the key symmetry group + of Minkowski spacetime, used throughout the library to define Lorentz tensors, + fermions, and the electromagnetic potential. + +ParentAPIs: + - Physlib/Relativity/MinkowskiMatrix.lean + +References: + - "Lorentz Transformations, Rotations, and Boosts, Jaffe. https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf" + +Requirements: + + - description: LorentzGroup is defined as the set of matrices satisfying Λ * dual Λ = 1 + done: true + location: Physlib/Relativity/LorentzGroup/Basic.lean (LorentzGroup) + + - description: Instance as a group + done: true + location: Physlib/Relativity/LorentzGroup/Basic.lean (lorentzGroupIsGroup) + + - description: Instance as a Lie group + done: false + location: N/A + + - description: Inclusion of boosts + done: true + location: Physlib/Relativity/LorentzGroup/Boosts/Basic.lean (boost) + + - description: Inclusion of rotations + done: true + location: Physlib/Relativity/LorentzGroup/Rotations.lean (Rotations) + + - description: Different membership conditions + done: true + location: Physlib/Relativity/LorentzGroup/Basic.lean (mem_iff_self_mul_dual, mem_iff_dual_mul_self, mem_iff_transpose, mem_iff_neg_mem, mem_iff_transpose_mul_minkowskiMatrix_mul_self) + + - description: Definition of proper Lorentz transforms + done: true + location: Physlib/Relativity/LorentzGroup/Proper.lean (IsProper) + + - description: Definition of orthochronous Lorentz transforms + done: true + location: Physlib/Relativity/LorentzGroup/Orthochronous/Basic.lean (IsOrthochronous) + + - description: Definition of the restricted Lorentz group + done: true + location: Physlib/Relativity/LorentzGroup/Restricted/Basic.lean (restricted) + + - description: Prove topological properties of the Orthochronous Lorentz Group + done: false + location: N/A + + - description: Prove that every member of the restricted Lorentz group is a combination of a boost and a rotation + done: false + location: N/A