From 7648f25d73d3cd871d15672bcda205bc84f31765 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 15 Jul 2024 16:57:06 -0400
Subject: [PATCH] refactor: Move LorentzTensor

---
 .../LorentzTensor/{ => Real}/Basic.lean       | 29 ++++---------------
 .../LorentzTensor/Real/LorentzAction.lean     | 18 ++++++++++++
 2 files changed, 24 insertions(+), 23 deletions(-)
 rename HepLean/SpaceTime/LorentzTensor/{ => Real}/Basic.lean (95%)
 create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean

diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
similarity index 95%
rename from HepLean/SpaceTime/LorentzTensor/Basic.lean
rename to HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index fee2c0a..e67832e 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.LinearAlgebra.Matrix.Trace
 /-!
 
-# Lorentz Tensors
+# Real Lorentz Tensors
 
 In this file we define real Lorentz tensors.
 
@@ -23,11 +23,6 @@ This will relation should be made explicit in the future.
 -/
 /-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
 /-! TODO: Generalize to maps into Lorentz tensors. -/
-/-!
-
-## Real Lorentz tensors
-
--/
 
 /-- The possible `colors` of an index for a RealLorentzTensor.
  There are two possiblities, `up` and `down`. -/
@@ -348,23 +343,11 @@ def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPo
 
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
 def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
-    ((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where
-  toFun x := match x with
-    | Sum.inl x => Sum.inl (Sum.inl x)
-    | Sum.inr ⟨0, PUnit.unit⟩ => Sum.inl (Sum.inr PUnit.unit)
-    | Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨i, Nat.succ_lt_succ_iff.mp h⟩, PUnit.unit⟩
-  invFun x := match x with
-    | Sum.inl (Sum.inl x) => Sum.inl x
-    | Sum.inl (Sum.inr PUnit.unit) => Sum.inr ⟨0, PUnit.unit⟩
-    | Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨Nat.succ i, Nat.succ_lt_succ h⟩, PUnit.unit⟩
-  left_inv x := by match x with
-    | Sum.inl x => rfl
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => rfl
-  right_inv x := by match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr PUnit.unit) => rfl
-    | Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => rfl
+    (X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit :=
+  trans (Equiv.sumCongr (Equiv.refl _) $ (Equiv.sigmaPUnit (Fin n.succ)).trans
+  (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm).trans
+  (Equiv.sumCongr finOneEquiv (Equiv.sigmaPUnit (Fin n)).symm)))
+  (Equiv.sumAssoc _ _ _).symm
 
 /-- Unmark the first marked index of a marked thensor. -/
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
new file mode 100644
index 0000000..e320251
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -0,0 +1,18 @@
+/-
+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.LorentzTensor.Real.Basic
+/-!
+
+# Lorentz group action on Real Lorentz Tensors
+
+We define the action of the Lorentz group on Real Lorentz Tensors.
+
+This file is currently a stub.
+-/
+
+namespace RealLorentzTensor
+
+end RealLorentzTensor