From ea4327aff59fde778912eb081ed0847eb114af44 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Jun 2024 16:00:07 -0400
Subject: [PATCH 1/3] feat: space-time and self-adjoint matrices

---
 HepLean.lean                               |  1 +
 HepLean/SpaceTime/AsSelfAdjointMatrix.lean | 93 ++++++++++++++++++++++
 HepLean/SpaceTime/Basic.lean               |  5 ++
 HepLean/SpaceTime/LorentzGroup/Basic.lean  |  2 +
 4 files changed, 101 insertions(+)
 create mode 100644 HepLean/SpaceTime/AsSelfAdjointMatrix.lean

diff --git a/HepLean.lean b/HepLean.lean
index 2ca63bf..429a466 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -56,6 +56,7 @@ import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
 import HepLean.GroupTheory.SO3.Basic
+import HepLean.SpaceTime.AsSelfAdjointMatrix
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
 import HepLean.SpaceTime.FourVelocity
diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
new file mode 100644
index 0000000..2701e19
--- /dev/null
+++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.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.Metric
+import HepLean.SpaceTime.FourVelocity
+import Mathlib.GroupTheory.SpecificGroups.KleinFour
+import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
+/-!
+# Spacetime as a self-adjoint matrix
+
+The main result of this file is a linear equivalence `spaceTimeToHerm` between the vector space
+of space-time points and the vector space of 2×2-complex self-adjoint matrices.
+
+-/
+namespace spaceTime
+
+open Matrix
+open MatrixGroups
+open Complex
+
+/-- A 2×2-complex matrix formed from a space-time point. -/
+@[simp]
+def toMatrix (x : spaceTime) : Matrix (Fin 2) (Fin 2) ℂ :=
+  !![x 0 + x 3, x 1 - x 2 * I ; x 1 + x 2 * I, x 0 - x 3]
+
+/-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/
+lemma toMatrix_isSelfAdjoint (x : spaceTime) : IsSelfAdjoint x.toMatrix := by
+  rw [isSelfAdjoint_iff, star_eq_conjTranspose, ← Matrix.ext_iff]
+  intro i j
+  fin_cases i <;> fin_cases j <;>
+    simp [toMatrix, conj_ofReal]
+  ring
+
+/-- A self-adjoint matrix formed from a space-time point. -/
+@[simps!]
+def toSelfAdjointMatrix' (x : spaceTime) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
+  ⟨x.toMatrix, toMatrix_isSelfAdjoint x⟩
+
+/-- A self-adjoint matrix formed from a space-time point. -/
+@[simp]
+noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : spaceTime :=
+  ![1/2 * (x.1 0 0 + x.1 1 1).re, (x.1 1 0).re, (x.1 1 0).im , (x.1 0 0 - x.1 1 1).re/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
+  toFun := toSelfAdjointMatrix'
+  invFun := fromSelfAdjointMatrix'
+  left_inv x := by
+    simp only [fromSelfAdjointMatrix', one_div, Fin.isValue, toSelfAdjointMatrix'_coe, of_apply,
+      cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons,
+      head_fin_const, add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
+      I_im, mul_one, sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel,
+      half_add_self]
+    funext i
+    fin_cases i <;> field_simp
+    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,
+      Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, ofReal_div, ofReal_sub,
+      cons_val_one, cons_val_two, re_add_im]
+    ext i j
+    fin_cases i <;> fin_cases j <;>
+      field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal]
+    exact conj_eq_iff_re.mp (congrArg (fun M => M 0 0) $ selfAdjoint.mem_iff.mp x.2 )
+    have h01 := congrArg (fun M => M 0 1) $ selfAdjoint.mem_iff.mp x.2
+    simp only [Fin.isValue, star_apply, RCLike.star_def] at h01
+    rw [← h01]
+    rw [RCLike.conj_eq_re_sub_im]
+    simp only [Fin.isValue, RCLike.re_to_complex, RCLike.im_to_complex, RCLike.I_to_complex]
+    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,
+      AddSubmonoid.mk_add_mk, of_add_of, add_cons, head_cons, tail_cons, empty_add_empty,
+      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
+    ext i j
+    fin_cases i <;> fin_cases j <;>
+      field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, add_apply]
+      <;> ring
+  map_smul' r x := by
+    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
+
+end spaceTime
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index f63058a..59fef79 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -89,6 +89,11 @@ lemma explicit (x : spaceTime) : x = ![x 0, x 1, x 2, x 3] := by
   funext i
   fin_cases i <;> rfl
 
+@[simp]
+lemma add_apply (x y : spaceTime) (i : Fin 4) : (x + y) i = x i + y i := rfl
+
+@[simp]
+lemma smul_apply (x : spaceTime) (a : ℝ) (i : Fin 4) : (a • x) i = a * x i := rfl
 
 end spaceTime
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index e083022..d628d8f 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.FourVelocity
 import Mathlib.GroupTheory.SpecificGroups.KleinFour
+import Mathlib.Geometry.Manifold.Algebra.LieGroup
+import Mathlib.Analysis.Matrix
 /-!
 # The Lorentz Group
 

From eb21428c3ec25daa4d1a12de2dc7bb552243f82c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Jun 2024 16:03:53 -0400
Subject: [PATCH 2/3] fix: Build error

---
 HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
index 09bccb2..c0b720b 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
@@ -65,7 +65,7 @@ lemma σ_comm (α β γ δ : Fin 4) :
   change σMat α β * σ γ δ -  σ γ δ * σ α β = _
   funext a b
   simp only [σ_coe, sub_apply, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid,
-    Submodule.coe_smul_of_tower, add_apply, smul_apply, σMat, smul_eq_mul]
+    Submodule.coe_smul_of_tower, Matrix.add_apply, Matrix.smul_apply, σMat, smul_eq_mul]
   rw [σMat_mul, σMat_mul, η_symmetric α γ, η_symmetric α δ, η_symmetric β γ, η_symmetric β δ]
   ring
 
@@ -77,7 +77,7 @@ lemma eq_span_σ (Λ : lorentzAlgebra) :
   fin_cases a <;> fin_cases b <;>
     simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, AddSubmonoid.coe_add,
      Submodule.coe_smul_of_tower, σ_coe,
-     add_apply, smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true,
+     Matrix.add_apply, Matrix.smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true,
      one_apply_ne, η_explicit, of_apply, cons_val_zero,
      mul_zero, one_apply_eq, mul_one, sub_neg_eq_add,
      zero_add, smul_eq_mul, Fin.reduceEq, cons_val_one, vecHead, vecTail,
@@ -121,7 +121,7 @@ noncomputable def σCoordinateMap : lorentzAlgebra ≃ₗ[ℝ] Fin 6 →₀ ℝ
     fin_cases i <;> simp only  [Fin.isValue, Set.Finite.toFinset_setOf, ne_eq, Finsupp.coe_mk,
     Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, AddSubmonoid.coe_add,
      Submodule.coe_toAddSubmonoid, Submodule.coe_smul_of_tower, σ_coe,
-     add_apply, smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true,
+     Matrix.add_apply, Matrix.smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true,
      one_apply_ne, η_explicit, of_apply, cons_val', cons_val_zero, empty_val',
      cons_val_fin_one, vecCons_const, mul_zero, one_apply_eq, mul_one, sub_neg_eq_add,
      zero_add, smul_eq_mul, Fin.reduceEq, cons_val_one, vecHead, vecTail, Nat.succ_eq_add_one,

From fbda420da9ccb9fadd91df2f4a0c1d39f6ebf1dd Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Jun 2024 16:08:59 -0400
Subject: [PATCH 3/3] refactor: Lint

---
 HepLean/SpaceTime/AsSelfAdjointMatrix.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
index 2701e19..23a1b2e 100644
--- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
@@ -23,7 +23,7 @@ open Complex
 /-- A 2×2-complex matrix formed from a space-time point. -/
 @[simp]
 def toMatrix (x : spaceTime) : Matrix (Fin 2) (Fin 2) ℂ :=
-  !![x 0 + x 3, x 1 - x 2 * I ; x 1 + x 2 * I, x 0 - x 3]
+  !![x 0 + x 3, x 1 - x 2 * I; x 1 + x 2 * I, x 0 - x 3]
 
 /-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/
 lemma toMatrix_isSelfAdjoint (x : spaceTime) : IsSelfAdjoint x.toMatrix := by