From 0d2d4ffc1d7b47faf8e2f46920a6fece8bf8086c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 18 Jul 2024 08:36:56 -0400 Subject: [PATCH] feat: Add multiplicative unit --- HepLean.lean | 1 + .../SpaceTime/LorentzTensor/Real/Basic.lean | 12 ++ .../LorentzTensor/Real/Multiplication.lean | 57 ++++- .../Real/MultiplicationUnit.lean | 195 ++++++++++++++++++ .../LorentzVector/AsSelfAdjointMatrix.lean | 2 +- HepLean/SpaceTime/LorentzVector/Basic.lean | 11 +- 6 files changed, 264 insertions(+), 14 deletions(-) create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean diff --git a/HepLean.lean b/HepLean.lean index b603d99..4cf002a 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -74,6 +74,7 @@ import HepLean.SpaceTime.LorentzTensor.Real.Basic import HepLean.SpaceTime.LorentzTensor.Real.Constructors import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction import HepLean.SpaceTime.LorentzTensor.Real.Multiplication +import HepLean.SpaceTime.LorentzTensor.Real.MultiplicationUnit import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix import HepLean.SpaceTime.LorentzVector.Basic import HepLean.SpaceTime.LorentzVector.NormOne diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index 00f48ff..15c753f 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -182,6 +182,18 @@ lemma indexValueIso_refl (d : ℕ) (i : X → Colors) : /-! +## Dual isomorphism for index values + +-/ + +/-- The isomorphism between the index values of a color map and its dual. -/ +@[simps!] +def indexValueDualIso (d : ℕ) {i j : X → Colors} (h : i = τ ∘ j) : + IndexValue d i ≃ IndexValue d j := + (Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ))) + +/-! + ## Extensionality -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean index 0c1b5bb..6cc5629 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean @@ -15,7 +15,6 @@ marked index. This is equivalent to contracting two Lorentz tensors. We prove various results about this multiplication. -/ -/-! TODO: Add unit to the multiplication. -/ /-! TODO: Generalize to contracting any marked index of a marked tensor. -/ /-! TODO: Set up a good notation for the multiplication. -/ @@ -39,6 +38,54 @@ def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue $ colorsIndexDualCast h x)) +/-! + +## Expressions for multiplication + +-/ +/-! TODO: Where appropriate write these expresions in terms of `indexValueDualIso`. -/ +lemma mul_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) + (h : T.markedColor 0 = τ (S.markedColor 0)) : + (mul T S h).coord = fun i => ∑ x, + T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, + oneMarkedIndexValue $ colorsIndexDualCast (color_eq_dual_symm h) x)) * + S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue x)) := by + funext i + rw [← Equiv.sum_comp (colorsIndexDualCast h)] + apply Finset.sum_congr rfl (fun x _ => ?_) + congr + rw [← colorsIndexDualCast_symm] + exact (Equiv.apply_eq_iff_eq_symm_apply (colorsIndexDualCast h)).mp rfl + +lemma mul_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) + (h : T.markedColor 0 = τ (S.markedColor 0)) : + (mul T S h).coord = fun i => ∑ j, + T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) * + S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, + (oneMarkedIndexValue $ (colorsIndexDualCast h) $ oneMarkedIndexValue.symm j))) := by + funext i + rw [← Equiv.sum_comp (oneMarkedIndexValue)] + rfl + +lemma mul_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) + (h : T.markedColor 0 = τ (S.markedColor 0)) : + (mul T S h).coord = fun i => ∑ j, + T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, + oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm j)) * + S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) := by + funext i + rw [mul_colorsIndex_right] + rw [← Equiv.sum_comp (oneMarkedIndexValue)] + apply Finset.sum_congr rfl (fun x _ => ?_) + congr + exact Eq.symm (colorsIndexDualCast_symm h) + +/-! + +## Properties of multiplication + +-/ + /-- Multiplication is well behaved with regard to swapping tensors. -/ lemma mul_symm {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) (h : T.markedColor 0 = τ (S.markedColor 0)) : @@ -49,14 +96,12 @@ lemma mul_symm {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) | inl _ => rfl | inr _ => rfl · funext i - rw [mapIso_apply_coord, mul_coord, mul_coord] - erw [← Equiv.sum_comp (colorsIndexDualCast h).symm] + rw [mul_colorsIndex_right] refine Fintype.sum_congr _ _ (fun x => ?_) rw [mul_comm] - congr - · exact Equiv.apply_symm_apply (colorsIndexDualCast h) x - · exact colorsIndexDualCast_symm h + rfl +/-- Multiplication commutes with `mapIso`. -/ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃ W) (g : Y ≃ Z) (h : T.markedColor 0 = τ (S.markedColor 0)) : mapIso d (Equiv.sumCongr f g) (mul T S h) = mul (mapIso d (Equiv.sumCongr f (Equiv.refl _)) T) diff --git a/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean b/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean new file mode 100644 index 0000000..9791a6d --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean @@ -0,0 +1,195 @@ +/- +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.Constructors +/-! + +# Unit of multiplication of Real Lorentz Tensors + +The definition of the unit is akin to the definition given in + +[Raynor][raynor2021graphical] + +for modular operads. + +The main results of this file are: + +- `mulUnit_right`: The multiplicative unit acts as a right unit for the multiplication of Lorentz + tensors. +- `mulUnit_left`: The multiplicative unit acts as a left unit for the multiplication of Lorentz + tensors. +- `mulUnit_lorentzAction`: The multiplicative unit is invariant under Lorentz transformations. + +-/ + +namespace RealLorentzTensor + +variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] + (T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors} + +open Marked + +/-! + +## Unit of multiplication + +-/ + +/-- The unit for the multiplication of Lorentz tensors. -/ +def mulUnit (d : ℕ) (μ : Colors) : Marked d (Fin 1) 1 := + match μ with + | .up => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm) + (ofMatUpDown 1) + | .down => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm) + (ofMatDownUp 1) + +lemma mulUnit_up_coord : (mulUnit d Colors.up).coord = fun i => + (1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (i (Sum.inl 0)) (i (Sum.inr 0)) := by + rfl + +lemma mulUnit_down_coord : (mulUnit d Colors.down).coord = fun i => + (1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (i (Sum.inl 0)) (i (Sum.inr 0)) := by + rfl + +@[simp] +lemma mulUnit_markedColor (μ : Colors) : (mulUnit d μ).markedColor 0 = τ μ := by + cases μ + case up => rfl + case down => rfl + +lemma mulUnit_dual_markedColor (μ : Colors) : τ ((mulUnit d μ).markedColor 0) = μ := by + cases μ + case up => rfl + case down => rfl + +@[simp] +lemma mulUnit_unmarkedColor (μ : Colors) : (mulUnit d μ).unmarkedColor 0 = μ := by + cases μ + case up => rfl + case down => rfl + +lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) : + (mulUnit d μ).unmarkedColor = τ ∘ (mulUnit d μ).markedColor := by + funext x + fin_cases x + simp only [Fin.zero_eta, Fin.isValue, mulUnit_unmarkedColor, Function.comp_apply, + mulUnit_markedColor] + exact color_eq_dual_symm rfl + +lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) : + (mulUnit d μ).coord (splitIndexValue.symm (i, + indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i)) = 1 := by + cases μ + case' up => rw [mulUnit_up_coord] + case' down => rw [mulUnit_down_coord] + all_goals + simp only [mulUnit] + symm + simp_all only [Fin.isValue, Matrix.one_apply] + split + rfl + next h => exact False.elim (h rfl) + +lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue) + (b : (mulUnit d μ).MarkedIndexValue) + (hb : b ≠ indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i) : + (mulUnit d μ).coord (splitIndexValue.symm (i, b)) = 0 := by + match μ with + | Colors.up => + rw [mulUnit_up_coord] + simp only [mulUnit, Matrix.one_apply, Fin.isValue, ite_eq_right_iff, one_ne_zero, imp_false, + ne_eq] + by_contra h + have h1 : (indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked (Colors.up)) i) = b := by + funext a + fin_cases a + exact h + exact hb (id (Eq.symm h1)) + | Colors.down => + rw [mulUnit_down_coord] + simp only [mulUnit, Matrix.one_apply, Fin.isValue, ite_eq_right_iff, one_ne_zero, imp_false, + ne_eq] + by_contra h + have h1 : (indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked (Colors.down)) i) = b := by + funext a + fin_cases a + exact h + exact hb (id (Eq.symm h1)) + +lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) : + mul T (mulUnit d μ) (h.trans (mulUnit_dual_markedColor μ).symm) = T := by + refine ext ?_ ?_ + · funext a + match a with + | .inl _ => rfl + | .inr 0 => + simp only [Fin.isValue, mul_color, Sum.elim_inr, mulUnit_unmarkedColor] + exact h.symm + funext i + rw [mul_indexValue_right] + change ∑ j, + T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, _)) * + (mulUnit d μ).coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) = _ + let y := indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) (indexValueSumEquiv i).2 + erw [Finset.sum_eq_single_of_mem y] + rw [mulUnit_coord_diag] + simp only [Fin.isValue, mul_one] + apply congrArg + funext a + match a with + | .inl a => + change (indexValueSumEquiv i).1 a = _ + rfl + | .inr 0 => + change oneMarkedIndexValue + ((colorsIndexDualCast (Eq.trans h (Eq.symm (mulUnit_dual_markedColor μ)))).symm + (oneMarkedIndexValue.symm y)) 0 = _ + rw [indexValueIso_eq_symm, indexValueIso_symm_apply'] + simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, colorsIndexCast, + Equiv.coe_fn_symm_mk, indexValueDualIso_apply, Equiv.trans_apply, Equiv.cast_apply, + Equiv.symm_trans_apply, Equiv.cast_symm, Equiv.symm_symm, Equiv.apply_symm_apply, cast_cast, + Equiv.coe_fn_mk, Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, mul_color, + Sum.elim_inr, Equiv.refl_apply, cast_inj, y] + rfl + exact Finset.mem_univ y + intro b _ hab + rw [mul_eq_zero] + apply Or.inr + exact mulUnit_coord_off_diag μ (indexValueSumEquiv i).2 b hab + +lemma mulUnit_left (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) : + mul (mulUnit d μ) T ((mulUnit_markedColor μ).trans (congrArg τ h.symm)) = + mapIso d (Equiv.sumComm X (Fin 1)) T := by + rw [← mul_symm, mulUnit_right] + exact h + +lemma mulUnit_lorentzAction (μ : Colors) (Λ : LorentzGroup d) : + Λ • mulUnit d μ = mulUnit d μ := by + match μ with + | Colors.up => + rw [mulUnit] + simp only [Nat.reduceAdd] + rw [← lorentzAction_mapIso] + rw [lorentzAction_ofMatUpDown] + repeat apply congrArg + rw [mul_one] + change (Λ * Λ⁻¹).1 = 1 + rw [mul_inv_self Λ] + rfl + | Colors.down => + rw [mulUnit] + simp only [Nat.reduceAdd] + rw [← lorentzAction_mapIso] + rw [lorentzAction_ofMatDownUp] + repeat apply congrArg + rw [mul_one] + change ((LorentzGroup.transpose Λ⁻¹) * LorentzGroup.transpose Λ).1 = 1 + have inv_transpose : (LorentzGroup.transpose Λ⁻¹) = (LorentzGroup.transpose Λ)⁻¹ := by + simp [LorentzGroup.transpose] + rw [inv_transpose] + rw [inv_mul_self] + rfl + +end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean index c5e2237..5007783 100644 --- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean +++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith import HepLean.SpaceTime.MinkowskiMetric import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! -# Spacetime as a self-adjoint matrix +# Lorentz vector as a self-adjoint matrix There is a linear equivalence between the vector space of space-time points and the vector space of 2×2-complex self-adjoint matrices. diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean index ce829c0..c8979f8 100644 --- a/HepLean/SpaceTime/LorentzVector/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -15,6 +15,7 @@ In this file we define a Lorentz vector (in 4d, this is more often called a 4-ve One of the most important example of a Lorentz vector is SpaceTime. -/ +/-! TODO: Define action of the Lorentz group. -/ /- The number of space dimensions . -/ variable (d : ℕ) @@ -37,9 +38,7 @@ instance : TopologicalSpace (LorentzVector d) := namespace LorentzVector -variable {d : ℕ} - -variable (v : LorentzVector d) +variable {d : ℕ} (v : LorentzVector d) /-- The space components. -/ @[simp] @@ -103,10 +102,8 @@ def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where @[simp] def spaceReflection : LorentzVector d := spaceReflectionLin v -lemma spaceReflection_space : v.spaceReflection.space = - v.space := by - rfl +lemma spaceReflection_space : v.spaceReflection.space = - v.space := rfl -lemma spaceReflection_time : v.spaceReflection.time = v.time := by - rfl +lemma spaceReflection_time : v.spaceReflection.time = v.time := rfl end LorentzVector