feat: Homomorphism from SL(2, C) to Lorentz Group

HepLean/SpaceTime/AsSelfAdjointMatrix.lean

@@ -45,19 +45,17 @@ noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2
 
 /-- The linear equivalence between the vector-space `spaceTime` and self-adjoint
   2×2-complex matrices. -/
-noncomputable def spaceTimeToHerm : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
+noncomputable def toSelfAdjointMatrix : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
   toFun := toSelfAdjointMatrix'
   invFun := fromSelfAdjointMatrix'
   left_inv x := by
-    simp only [fromSelfAdjointMatrix', one_div, Fin.isValue, toSelfAdjointMatrix'_coe, of_apply,
+    simp only [fromSelfAdjointMatrix', one_div, toSelfAdjointMatrix'_coe, of_apply, cons_val',
-      cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons,
+      cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons, head_fin_const,
-      head_fin_const, add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
+      add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,
-      I_im, mul_one, sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel,
+      sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel, half_add_self]
-      half_add_self]
+    field_simp [spaceTime]
-    funext i
+    ext1 x
-    fin_cases i <;> field_simp
+    fin_cases x <;> rfl
-    rfl
-    rfl
   right_inv x := by
     simp only [toSelfAdjointMatrix', toMatrix, fromSelfAdjointMatrix', one_div, Fin.isValue, add_re,
       sub_re, cons_val_zero, ofReal_mul, ofReal_inv, ofReal_ofNat, ofReal_add, cons_val_three,
@@ -73,19 +71,22 @@ noncomputable def spaceTimeToHerm : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (F
     rfl
     exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 )
   map_add' x y  := by
-    simp only [toSelfAdjointMatrix', toMatrix, Fin.isValue, add_apply, ofReal_add,
+    ext i j : 2
-      AddSubmonoid.mk_add_mk, of_add_of, add_cons, head_cons, tail_cons, empty_add_empty,
+    simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val',
-      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
+      cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply]
-    ext i j
+    fin_cases i <;> fin_cases j <;> simp <;> ring
-    fin_cases i <;> fin_cases j <;>
-      field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, add_apply]
-      <;> ring
   map_smul' r x := by
+    ext i j : 2
     simp only [toSelfAdjointMatrix', toMatrix, Fin.isValue, smul_apply, ofReal_mul,
       RingHom.id_apply]
-    ext i j
     fin_cases i <;> fin_cases j <;>
       field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, smul_apply]
        <;> ring
 
+lemma det_eq_ηLin (x : spaceTime) : det (toSelfAdjointMatrix x).1 = ηLin x x := by
+  simp [toSelfAdjointMatrix, ηLin_expand]
+  ring_nf
+  simp only [Fin.isValue, I_sq, mul_neg, mul_one]
+  ring
+
 end spaceTime

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.FourVelocity
+import HepLean.SpaceTime.AsSelfAdjointMatrix
 import Mathlib.GroupTheory.SpecificGroups.KleinFour
 import Mathlib.Geometry.Manifold.Algebra.LieGroup
 import Mathlib.Analysis.Matrix
@@ -45,6 +46,30 @@ namespace PreservesηLin
 
 variable  (Λ : Matrix (Fin 4) (Fin 4) ℝ)
 
+lemma iff_norm : PreservesηLin Λ ↔
+    ∀ (x : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ x) = ηLin x x := by
+  refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
+  have hp := h (x + y)
+  have hn := h (x - y)
+  rw [mulVec_add] at hp
+  rw [mulVec_sub] at hn
+  simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
+  rw [ηLin_symm (Λ *ᵥ y) (Λ *ᵥ x), ηLin_symm y x] at hp hn
+  linear_combination hp / 4 + -1 * hn / 4
+
+lemma iff_det_selfAdjoint : PreservesηLin Λ ↔
+    ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)),
+    det ((toSelfAdjointMatrix ∘ toLin stdBasis stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
+    = det x.1 := by
+  rw [iff_norm]
+  apply Iff.intro
+  intro h x
+  have h1 := congrArg ofReal $ h (toSelfAdjointMatrix.symm x)
+  simpa [← det_eq_ηLin] using h1
+  intro h x
+  have h1 := h (toSelfAdjointMatrix x)
+  simpa [det_eq_ηLin] using h1
+
 lemma iff_on_right : PreservesηLin Λ ↔
     ∀ (x y : spaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by
   apply Iff.intro
@@ -74,14 +99,13 @@ lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
   rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
     ← mul_assoc, transpose_one] at h1
   rw [iff_matrix' Λ.transpose, ← h1]
-  rw [← mul_assoc, ← mul_assoc]
+  noncomm_ring
-  exact Matrix.mul_assoc (Λᵀ * η) Λᵀᵀ η
   intro h
   have h1 := congrArg transpose ((iff_matrix Λ.transpose).mp h)
   rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
     ← mul_assoc, transpose_one, transpose_transpose] at h1
   rw [iff_matrix', ← h1]
-  repeat rw [← mul_assoc]
+  noncomm_ring
 
 /-- The lift of a matrix which preserves `ηLin` to an invertible matrix. -/
 def liftGL {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : GL (Fin 4) ℝ :=

HepLean/SpaceTime/Metric.lean

@@ -182,9 +182,7 @@ lemma ηLin_expand (x y : spaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 *
 
 lemma ηLin_expand_self (x : spaceTime) : ηLin x x = x 0 ^ 2 - ‖x.space‖ ^ 2 := by
   rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three, ηLin_expand]
-  simp only [Fin.isValue, space, cons_val_zero, RCLike.inner_apply, conj_trivial, cons_val_one,
+  noncomm_ring
-    head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons]
-  ring
 
 lemma time_elm_sq_of_ηLin (x : spaceTime) : x 0 ^ 2 = ηLin x x + ‖x.space‖ ^ 2 := by
   rw [ηLin_expand_self]
@@ -197,9 +195,7 @@ lemma ηLin_leq_time_sq (x : spaceTime) : ηLin x x ≤ x 0 ^ 2 := by
 lemma ηLin_space_inner_product (x y : spaceTime) :
     ηLin x y = x 0 * y 0 - ⟪x.space, y.space⟫_ℝ  := by
   rw [ηLin_expand, @PiLp.inner_apply, Fin.sum_univ_three]
-  simp only [Fin.isValue, space, cons_val_zero, RCLike.inner_apply, conj_trivial, cons_val_one,
+  noncomm_ring
-    head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons]
-  ring
 
 lemma ηLin_ge_abs_inner_product (x y : spaceTime) :
     x 0 * y 0 - ‖⟪x.space, y.space⟫_ℝ‖ ≤ (ηLin x y)  := by

HepLean/SpaceTime/SL2C/Basic.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzGroup.Basic
+import Mathlib.RepresentationTheory.Basic
+/-!
+# The group SL(2, ℂ) and it's relation to the Lorentz group
+
+The aim of this file is to give the relationship between `SL(2, ℂ)` and the Lorentz group.
+
+## TODO
+
+This file is a working progress.
+
+-/
+namespace spaceTime
+
+open Matrix
+open MatrixGroups
+open Complex
+
+namespace SL2C
+
+open spaceTime
+
+noncomputable section
+
+/-- Given an element  `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to
+ itself defined by  `A ↦ M * A * Mᴴ`. -/
+@[simps!]
+def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
+    selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
+  toFun A := ⟨M.1 * A.1 * Matrix.conjTranspose M,
+    by
+      noncomm_ring [selfAdjoint.mem_iff, star_eq_conjTranspose,
+        conjTranspose_mul, conjTranspose_conjTranspose,
+        (star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]⟩
+  map_add' A B := by
+    noncomm_ring [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, AddSubmonoid.mk_add_mk,
+      Subtype.mk.injEq]
+  map_smul' r A := by
+    noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
+      RingHom.id_apply]
+
+/-- The representation of  `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by
+   `M A ↦ M * A * Mᴴ`. -/
+@[simps!]
+def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
+  toFun := toLinearMapSelfAdjointMatrix
+  map_one' := by
+    noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul,
+      conjTranspose_one, mul_one, Subtype.coe_eta]
+  map_mul' M N := by
+    ext x i j : 3
+    noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, mul_assoc,
+      conjTranspose_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply]
+
+/-- The representation of  `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and
+  `repSelfAdjointMatrix`. -/
+def repSpaceTime : Representation ℝ SL(2, ℂ) spaceTime where
+  toFun M := toSelfAdjointMatrix.symm.comp ((repSelfAdjointMatrix M).comp
+    toSelfAdjointMatrix.toLinearMap)
+  map_one' := by
+    ext
+    simp
+  map_mul' M N := by
+    ext x : 3
+    simp
+
+/-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/
+@[simps!]
+def toLorentzGroupElem (M : SL(2, ℂ)) : 𝓛 :=
+  ⟨LinearMap.toMatrix stdBasis stdBasis (repSpaceTime M) ,
+   by simp [repSpaceTime, PreservesηLin.iff_det_selfAdjoint]⟩
+
+/-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/
+@[simps!]
+def toLorentzGroup : SL(2, ℂ) →* 𝓛 where
+  toFun := toLorentzGroupElem
+  map_one' := by
+    simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one]
+    rfl
+  map_mul' M N := by
+    apply Subtype.eq
+    simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul,
+      lorentzGroupIsGroup_mul_coe]
+
+end
+end SL2C
+
+end spaceTime