Merge pull request #160 from HEPLean/informal_defs

feat: Add Lorentz group informal lemmas

HepLean/SpaceTime/LorentzGroup/Restricted.lean

@@ -3,6 +3,10 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
+import HepLean.SpaceTime.LorentzGroup.Basic
+import HepLean.SpaceTime.LorentzGroup.Proper
+import HepLean.SpaceTime.LorentzGroup.Orthochronous
+import HepLean.Meta.Informal
 /-!
 # The Restricted Lorentz Group
 
@@ -12,3 +16,20 @@ This file is currently a stub.
 /-! TODO: Add definition of the restricted Lorentz group. -/
 /-! TODO: Prove member of the restricted Lorentz group is combo of boost and rotation. -/
 /-! TODO: Prove restricted Lorentz group equivalent to connected component of identity. -/
+
+noncomputable section
+
+open Matrix
+open Complex
+open ComplexConjugate
+
+namespace LorentzGroup
+
+open minkowskiMetric
+
+informal_definition Restricted where
+  math :≈ "The subgroup of the Lorentz group consisting of elements which
+    are proper and orthochronous."
+  deps :≈ [``LorentzGroup, ``IsProper, ``IsOrthochronous]
+
+end LorentzGroup

HepLean/SpaceTime/SL2C/Basic.lean

@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 import HepLean.SpaceTime.LorentzGroup.Basic
 import Mathlib.RepresentationTheory.Basic
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
+import HepLean.SpaceTime.LorentzGroup.Restricted
+import HepLean.Meta.Informal
 /-!
 # The group SL(2, ℂ) and it's relation to the Lorentz group
 
@@ -122,6 +124,19 @@ In this section we will define this homomorphism.
 
 -/
 
+informal_lemma toLorentzGroup_det_one where
+  math :≈ "The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one."
+  deps :≈ [``toLorentzGroup]
+
+informal_lemma toLorentzGroup_timeComp_nonneg where
+  math :≈ "The time coponent of the image of `SL(2, ℂ)` in the Lorentz group is non-negative."
+  deps :≈ [``toLorentzGroup, ``LorentzGroup.timeComp]
+
+informal_lemma toRestrictedLorentzGroup where
+  math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
+  deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_timeComp_nonneg,
+    ``LorentzGroup.Restricted]
+
 /-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
 end
 end SL2C