DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Move LorentzTensor

Browse source
This commit is contained in:
jstoobysmith 2024-07-15 16:57:06 -04:00
parent 51696d20be
commit 7648f25d73
2 changed files with 24 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

29
HepLean/SpaceTime/LorentzTensor/Basic.lean → HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
View file

@ -9,7 +9,7 @@ import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.LinearAlgebra.Matrix.Trace import Mathlib.LinearAlgebra.Matrix.Trace
/-! /-!
# Lorentz Tensors # Real Lorentz Tensors
In this file we define 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: Do complex tensors, with Van der Waerden notation for fermions. -/
/-! TODO: Generalize to maps into Lorentz tensors. -/ /-! TODO: Generalize to maps into Lorentz tensors. -/
/-!
## Real Lorentz tensors
-/
/-- The possible `colors` of an index for a RealLorentzTensor. /-- The possible `colors` of an index for a RealLorentzTensor.
There are two possiblities, `up` and `down`. -/ 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. -/ /-- 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) ≃ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where (X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit :=
toFun x := match x with trans (Equiv.sumCongr (Equiv.refl _) $ (Equiv.sigmaPUnit (Fin n.succ)).trans
| Sum.inl x => Sum.inl (Sum.inl x) (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm).trans
| Sum.inr ⟨0, PUnit.unit⟩ => Sum.inl (Sum.inr PUnit.unit) (Equiv.sumCongr finOneEquiv (Equiv.sigmaPUnit (Fin n)).symm)))
| Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨i, Nat.succ_lt_succ_iff.mp h⟩, PUnit.unit⟩ (Equiv.sumAssoc _ _ _).symm
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
/-- Unmark the first marked index of a marked thensor. -/ /-- Unmark the first marked index of a marked thensor. -/
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n := def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=

18
HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean Normal file
View file

@ -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