From 8b2c853fd83b3a044c157ad02e961449d371dd67 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 31 Jul 2024 07:29:59 -0400
Subject: [PATCH] feat: equivariance of rising and lowering indices

---
 .../SpaceTime/LorentzTensor/Contraction.lean  |  4 +-
 .../LorentzTensor/MulActionTensor.lean        | 66 +++++++++++++++----
 .../LorentzTensor/RisingLowering.lean         | 62 ++++++++++++++++-
 3 files changed, 115 insertions(+), 17 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
index fed8eab..e08da05 100644
--- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
@@ -287,9 +287,9 @@ lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (
   simp only [mk_apply]
   apply congrArg
   funext x
-  rw [← repColorModule_colorModuleCast_apply]
+  rw [← colorModuleCast_equivariant_apply]
   nth_rewrite 2 [← contrDual_inv (c x) g]
-  rfl
+  simp
 
 @[simp]
 lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
index 46e9f14..c5de9da 100644
--- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
@@ -27,6 +27,9 @@ class MulActionTensor (G : Type) [Monoid G] (𝓣 : TensorStructure R) where
   /-- The contraction of a vector with its dual is invariant under the group action. -/
   contrDual_inv : ∀ μ g, 𝓣.contrDual μ ∘ₗ
     TensorProduct.map (repColorModule μ g) (repColorModule (𝓣.τ μ) g) = 𝓣.contrDual μ
+  /-- The invariance of the metric under the group action. -/
+  metric_inv : ∀ μ g, (TensorProduct.map (repColorModule μ g) (repColorModule μ g)) (𝓣.metric μ) =
+    𝓣.metric μ
 
 namespace MulActionTensor
 
@@ -50,6 +53,9 @@ def compHom (f : H →* G) : MulActionTensor H 𝓣 where
   contrDual_inv μ h := by
     simp only [MonoidHom.coe_comp, Function.comp_apply]
     rw [contrDual_inv]
+  metric_inv μ h := by
+    simp only [MonoidHom.coe_comp, Function.comp_apply]
+    rw [metric_inv]
 
 /-- The trivial `MulActionTensor` defined via trivial representations. -/
 def trivial : MulActionTensor G 𝓣 where
@@ -57,6 +63,9 @@ def trivial : MulActionTensor G 𝓣 where
   contrDual_inv μ g := by
     simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
     rfl
+  metric_inv μ g := by
+    simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
+    rfl
 
 end MulActionTensor
 
@@ -74,6 +83,40 @@ variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [De
 
 /-!
 
+# Equivariance properties involving modules
+
+-/
+
+@[simp]
+lemma contrDual_equivariant_tmul (g : G) (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ)) :
+    (𝓣.contrDual μ ((repColorModule μ g x) ⊗ₜ[R] (repColorModule (𝓣.τ μ) g y))) =
+    𝓣.contrDual μ (x ⊗ₜ[R] y) := by
+  trans (𝓣.contrDual μ ∘ₗ
+      TensorProduct.map (repColorModule μ g) (repColorModule (𝓣.τ μ) g)) (x ⊗ₜ[R] y)
+  rfl
+  rw [contrDual_inv]
+
+@[simp]
+lemma colorModuleCast_equivariant_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
+    (𝓣.colorModuleCast h) (repColorModule μ g x) =
+    (repColorModule ν g) (𝓣.colorModuleCast h x) := by
+  subst h
+  simp [colorModuleCast]
+
+@[simp]
+lemma contrRightAux_contrDual_equivariant_tmul (g : G) (m : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule μ)
+    (x : 𝓣.ColorModule (𝓣.τ μ)) : (contrRightAux (𝓣.contrDual μ))
+    ((TensorProduct.map (repColorModule ν g) (repColorModule μ g) m) ⊗ₜ[R]
+    (repColorModule (𝓣.τ μ) g x)) =
+    repColorModule ν g ((contrRightAux (𝓣.contrDual μ)) (m ⊗ₜ[R] x)) := by
+  refine TensorProduct.induction_on m (by simp) ?_ ?_
+  · intro y z
+    simp [contrRightAux]
+  · intro x z h1 h2
+    simp [add_tmul, LinearMap.map_add, h1, h2]
+
+/-!
+
 ## Representation of tensor products
 
 -/
@@ -89,19 +132,13 @@ def rep : Representation R G (𝓣.Tensor cX) where
 
 local infixl:101 " • " => 𝓣.rep
 
-lemma repColorModule_colorModuleCast_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
-    (repColorModule ν g) (𝓣.colorModuleCast h x) =
-    (𝓣.colorModuleCast h) (repColorModule μ g x) := by
-  subst h
-  simp [colorModuleCast]
-
 @[simp]
 lemma repColorModule_colorModuleCast (h : μ = ν) (g : G) :
     (repColorModule ν g) ∘ₗ (𝓣.colorModuleCast h).toLinearMap =
     (𝓣.colorModuleCast h).toLinearMap ∘ₗ (repColorModule μ g) := by
   apply LinearMap.ext
   intro x
-  simp [repColorModule_colorModuleCast_apply]
+  simp [colorModuleCast_equivariant_apply]
 
 @[simp]
 lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
@@ -112,7 +149,7 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
   simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
     Function.comp_apply]
   erw [mapIso_tprod]
-  simp [rep, repColorModule_colorModuleCast_apply]
+  simp [rep, colorModuleCast_equivariant_apply]
   change (PiTensorProduct.map fun x => (repColorModule (cY x)) g)
     ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (x (e.symm i))) =
     (𝓣.mapIso e h) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) x))
@@ -120,7 +157,7 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
   apply congrArg
   funext i
   subst h
-  simp [repColorModule_colorModuleCast_apply]
+  simp [colorModuleCast_equivariant_apply]
 
 @[simp]
 lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) :
@@ -143,7 +180,7 @@ lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
 
 -/
 
-lemma rep_tensoratorEquiv (g : G) :
+lemma tensoratorEquiv_equivariant (g : G) :
     (𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.rep g ∘ₗ
     (𝓣.tensoratorEquiv cX cY).toLinearMap := by
   apply tensorProd_piTensorProd_ext
@@ -156,18 +193,19 @@ lemma rep_tensoratorEquiv (g : G) :
   | Sum.inl x => rfl
   | Sum.inr x => rfl
 
-lemma rep_tensoratorEquiv_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
+@[simp]
+lemma tensoratorEquiv_equivariant_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
     (𝓣.tensoratorEquiv cX cY) ((TensorProduct.map (𝓣.rep g) (𝓣.rep g)) x)
     = (𝓣.rep g) ((𝓣.tensoratorEquiv cX cY) x) := by
   trans ((𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x
   rfl
-  rw [rep_tensoratorEquiv]
+  rw [tensoratorEquiv_equivariant]
   rfl
 
 lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
     (𝓣.tensoratorEquiv cX cY) ((g • x) ⊗ₜ[R] (g • y)) =
     g • ((𝓣.tensoratorEquiv cX cY) (x ⊗ₜ[R] y)) := by
-  nth_rewrite 1 [← rep_tensoratorEquiv_apply]
+  nth_rewrite 1 [← tensoratorEquiv_equivariant_apply]
   rfl
 
 lemma rep_tensoratorEquiv_symm (g : G) :
@@ -175,7 +213,7 @@ lemma rep_tensoratorEquiv_symm (g : G) :
     (𝓣.tensoratorEquiv cX cY).symm.toLinearMap := by
   rw [LinearEquiv.eq_comp_toLinearMap_symm, LinearMap.comp_assoc,
     LinearEquiv.toLinearMap_symm_comp_eq]
-  exact Eq.symm (rep_tensoratorEquiv 𝓣 g)
+  exact Eq.symm (tensoratorEquiv_equivariant 𝓣 g)
 
 @[simp]
 lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) :
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index 450b099..ed869d9 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -3,7 +3,7 @@ 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.Basic
+import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 /-!
 
 # Rising and Lowering of indices
@@ -31,6 +31,9 @@ variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype
   {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
   {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
 
+variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
+local infixl:101 " • " => 𝓣.rep
+
 /-!
 
 ## Properties of the unit
@@ -120,6 +123,27 @@ def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorMo
       Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq,
       metric_contrRight_unit]
 
+@[simp]
+lemma dualizeModule_equivariant (g : G) :
+    (𝓣.dualizeModule μ) ∘ₗ ((MulActionTensor.repColorModule μ) g) =
+    (MulActionTensor.repColorModule (𝓣.τ μ) g) ∘ₗ (𝓣.dualizeModule μ) := by
+  apply LinearMap.ext
+  intro x
+  simp only [dualizeModule, dualizeFun, dualizeSymm, LinearEquiv.ofLinear_toLinearMap,
+    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, colorModuleCast_equivariant_apply,
+    lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq]
+  nth_rewrite 1 [← MulActionTensor.metric_inv (𝓣.τ μ) g]
+  simp
+
+@[simp]
+lemma dualizeModule_equivariant_apply (g : G) (x : 𝓣.ColorModule μ) :
+    (𝓣.dualizeModule μ) ((MulActionTensor.repColorModule μ) g x) =
+    (MulActionTensor.repColorModule (𝓣.τ μ) g) (𝓣.dualizeModule μ x) := by
+  trans ((𝓣.dualizeModule μ) ∘ₗ ((MulActionTensor.repColorModule μ) g)) x
+  rfl
+  rw [dualizeModule_equivariant]
+  rfl
+
 /-- Dualizes the color of all indicies of a tensor by contraction with the metric. -/
 def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
   refine LinearEquiv.ofLinear
@@ -141,6 +165,24 @@ def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
     apply congrArg
     simp
 
+@[simp]
+lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@rep R _ G _ 𝓣 _ X cX g)
+    = 𝓣.rep g ∘ₗ (𝓣.dualizeAll.toLinearMap) := by
+  apply LinearMap.ext
+  intro x
+  simp [dualizeAll]
+  refine PiTensorProduct.induction_on' x ?_ (by
+      intro a b hx a
+      simp [map_add, add_tmul, hx]
+      simp_all only [Function.comp_apply, LinearMap.coe_comp, LinearMap.id_coe, id_eq])
+  intro rx fx
+  simp
+  apply congrArg
+  change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) _) =
+    (𝓣.rep g) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fx))
+  rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
+  simp
+
 lemma dualize_cond (e : C ⊕ P ≃ X) :
     cX = Sum.elim (cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm := by
   rw [Equiv.eq_comp_symm]
@@ -169,6 +211,24 @@ def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R]
   (𝓣.tensoratorEquiv _ _) ≪≫ₗ
   𝓣.mapIso e (𝓣.dualize_cond' e)
 
+/-- Dualizing indices is equivariant with respect to the group action. This is the
+  applied version of this statement. -/
+@[simp]
+lemma dualize_equivariant_apply (e : C ⊕ P ≃ X) (g : G) (x : 𝓣.Tensor cX) :
+    𝓣.dualize e (g • x) = g • (𝓣.dualize e x) := by
+  simp only [dualize, TensorProduct.congr, LinearEquiv.refl_toLinearMap, LinearEquiv.refl_symm,
+    LinearEquiv.trans_apply, rep_mapIso_apply, rep_tensoratorEquiv_symm_apply,
+    LinearEquiv.ofLinear_apply]
+  rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
+  simp only [dualizeAll_equivariant, LinearMap.id_comp]
+  have h1 {M N A B C : Type} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid A]
+      [AddCommMonoid B] [AddCommMonoid C] [Module R M] [Module R N] [Module R A] [Module R B]
+      [Module R C] (f : M →ₗ[R] N) (g : A →ₗ[R] B) (h : B →ₗ[R] C) : TensorProduct.map (h ∘ₗ g) f
+      = TensorProduct.map h f ∘ₗ TensorProduct.map g (LinearMap.id) :=
+    ext rfl
+  rw [h1, LinearMap.coe_comp, Function.comp_apply]
+  simp only [tensoratorEquiv_equivariant_apply, rep_mapIso_apply]
+
 end TensorStructure
 
 end