From 05e1dda58c86406fefdce98a70eea0a371e5f4c6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 16 Jul 2024 09:45:03 -0400 Subject: [PATCH] feat: add action on Lorentz group --- .../SpaceTime/LorentzTensor/Real/Basic.lean | 5 + .../LorentzTensor/Real/LorentzAction.lean | 136 +++++++++++++++++- 2 files changed, 140 insertions(+), 1 deletion(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index e67832e..b9f01e3 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -41,6 +41,11 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor. | RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d) | RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d) +instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) := + match μ with + | RealLorentzTensor.Colors.up => instDecidableEqSum + | RealLorentzTensor.Colors.down => instDecidableEqSum + /-- An `IndexValue` is a set of actual values an index can take. e.g. for a 3-tensor (0, 1, 2). -/ @[simp] diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean index e320251..3e34ca0 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean @@ -4,15 +4,149 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzTensor.Real.Basic +import HepLean.SpaceTime.LorentzGroup.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. +The Lorentz action is currently only defined for finite and decidable types `X`. + -/ namespace RealLorentzTensor +variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors) +variable (Λ Λ' : LorentzGroup d) +open LorentzGroup +open BigOperators + +instance : Fintype (IndexValue d c) := Pi.fintype +variable {μ : Colors} + +/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a + color `μ`. + + Thought of as the representation of the Lorentz group for that color index. -/ +def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (ColorsIndex d μ) ℝ where + toFun Λ := match μ with + | .up => fun i j => Λ.1 i j + | .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j + map_one' := by + match μ with + | .up => + simp only [lorentzGroupIsGroup_one_coe] + ext i j + simp only [OfNat.ofNat, One.one, ColorsIndex] + congr + | .down => + simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one] + ext i j + simp only [OfNat.ofNat, One.one, ColorsIndex] + congr + map_mul' Λ Λ' := by + match μ with + | .up => + ext i j + simp only [lorentzGroupIsGroup_mul_coe] + | .down => + ext i j + simp only [transpose, mul_inv_rev, lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe, + Matrix.transpose_mul, Matrix.transpose_apply] + rfl + +/-- A real number which occurs in the definition of -/ +@[simp] +def prodColorMatrixOnIndexValue (i j : IndexValue d c) : ℝ := + ∏ x, colorMatrix (c x) Λ (i x) (j x) + +lemma one_prodColorMatrixOnIndexValue_on_diag (i : IndexValue d c) : + prodColorMatrixOnIndexValue c 1 i i = 1 := by + simp only [prodColorMatrixOnIndexValue] + rw [Finset.prod_eq_one] + intro x _ + simp only [colorMatrix, MonoidHom.map_one, Matrix.one_apply] + rfl + +lemma one_prodColorMatrixOnIndexValue_off_diag {i j : IndexValue d c} (hij : j ≠ i) : + prodColorMatrixOnIndexValue c 1 i j = 0 := by + simp only [prodColorMatrixOnIndexValue] + obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij + rw [@Finset.prod_eq_zero _ _ _ _ _ x] + exact Finset.mem_univ x + simp only [map_one] + exact Matrix.one_apply_ne' hijx + +lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) : + prodColorMatrixOnIndexValue c (Λ * Λ') i j = + ∑ (k : IndexValue d c), + ∏ x, (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) := by + have h1 : ∑ (k : IndexValue d c), ∏ x, + (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) = + ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by + rw [Finset.prod_sum] + simp only [Finset.prod_attach_univ, Finset.sum_univ_pi] + apply Finset.sum_congr + simp only [IndexValue, Fintype.piFinset_univ] + intro x _ + rfl + rw [h1] + simp only [prodColorMatrixOnIndexValue, map_mul] + exact Finset.prod_congr rfl (fun x _ => rfl) + +/-- Action of the Lorentz group on the set of Real Lorentz Tensors indexed by `X`. -/ +def lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where + smul Λ T := {color := T.color, + coord := fun i => ∑ j, prodColorMatrixOnIndexValue T.color Λ i j * T.coord j} + one_smul T := by + refine ext' rfl ?_ + funext i + simp only [HSMul.hSMul, map_one] + erw [Finset.sum_eq_single_of_mem i] + rw [one_prodColorMatrixOnIndexValue_on_diag] + simp only [one_mul, IndexValue] + rfl + exact Finset.mem_univ i + intro j _ hij + rw [one_prodColorMatrixOnIndexValue_off_diag] + simp only [zero_mul] + exact hij + mul_smul Λ Λ' T := by + refine ext' rfl ?_ + simp only [HSMul.hSMul] + funext i + have h1 : ∑ j : IndexValue d T.color, prodColorMatrixOnIndexValue T.color (Λ * Λ') i j + * T.coord j = ∑ j : IndexValue d T.color, ∑ (k : IndexValue d T.color), + (∏ x, ((colorMatrix (T.color x) Λ (i x) (k x)) * + (colorMatrix (T.color x) Λ' (k x) (j x)))) * T.coord j := by + refine Finset.sum_congr rfl (fun j _ => ?_) + rw [mul_prodColorMatrixOnIndexValue, Finset.sum_mul] + rw [h1] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl (fun j _ => ?_) + rw [Finset.mul_sum] + refine Finset.sum_congr rfl (fun k _ => ?_) + simp only [prodColorMatrixOnIndexValue, IndexValue] + rw [← mul_assoc] + congr + rw [Finset.prod_mul_distrib] + rfl + +/-! + +## The Lorentz action on constructors + +-/ + + + + + + + + + + + end RealLorentzTensor