From 6d8ac0054d7a5469e7b0f3b483ef8a26291c0810 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 30 Jul 2024 16:07:16 -0400 Subject: [PATCH] feat: Add rising and lower indices --- HepLean/SpaceTime/LorentzTensor/Basic.lean | 153 ++++++++++++++-- .../SpaceTime/LorentzTensor/Contraction.lean | 115 +++++++++++- .../LorentzTensor/MulActionTensor.lean | 71 +++----- .../LorentzTensor/RisingLowering.lean | 171 ++++++++++++++++++ 4 files changed, 450 insertions(+), 60 deletions(-) create mode 100644 HepLean/SpaceTime/LorentzTensor/RisingLowering.lean diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 5cf9def..e883bd6 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -34,22 +34,58 @@ open TensorProduct variable {R : Type} [CommSemiring R] +namespace TensorStructure + /-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/ -def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] +def contrLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) : V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 := (TensorProduct.lid R _).toLinearMap ∘ₗ TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap +def contrRightAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] + [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) : + (V3 ⊗[R] V1) ⊗[R] V2 →ₗ[R] V3 := + (TensorProduct.rid R _).toLinearMap ∘ₗ + TensorProduct.map (LinearEquiv.refl R V3).toLinearMap f ∘ₗ + (TensorProduct.assoc R _ _ _).toLinearMap + + /-- An auxillary function to contract the vector space `V1` and `V2` in `V4 ⊗[R] V1 ⊗[R] V2 ⊗[R] V3`. -/ -def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] +def contrMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] (f : V1 ⊗[R] V2 →ₗ[R] R) : (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 := - (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ + (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrLeftAux f)) ∘ₗ (TensorProduct.assoc R _ _ _).toLinearMap +lemma contrRightAux_comp {V1 V2 V3 V4 V5 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] + [AddCommMonoid V4] [AddCommMonoid V5] [Module R V1] [Module R V2] [Module R V3] [Module R V2] [Module R V4] + [Module R V5] + (f : V2 ⊗[R] V3 →ₗ[R] R) (g : V4 ⊗[R] V5 →ₗ[R] R) : + (contrRightAux f ∘ₗ TensorProduct.map (LinearMap.id : V1 ⊗[R] V2 →ₗ[R] V1 ⊗[R] V2) + (contrRightAux g)) = + (contrRightAux g) ∘ₗ TensorProduct.map (contrMidAux f) LinearMap.id + ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap := by + apply TensorProduct.ext' + intro x y + refine TensorProduct.induction_on x (by simp) ?_ (fun x z h1 h2 => + by simp [add_tmul, LinearMap.map_add, h1, h2]) + intro x1 x2 + refine TensorProduct.induction_on y (by simp) ?_ (fun x z h1 h2 => + by simp [add_tmul, tmul_add, LinearMap.map_add, h1, h2]) + intro y x5 + refine TensorProduct.induction_on y (by simp) ?_ (fun x z h1 h2 => + by simp [add_tmul, tmul_add, LinearMap.map_add, h1, h2]) + intro x3 x4 + simp [contrRightAux, contrMidAux, contrLeftAux] + erw [TensorProduct.map_tmul] + simp only [LinearMapClass.map_smul, LinearMap.id_coe, id_eq, mk_apply, rid_tmul] + + +end TensorStructure + /-- An initial structure specifying a tensor system (e.g. a system in which you can define real Lorentz tensors or Einstein notation convention). -/ structure TensorStructure (R : Type) [CommSemiring R] where @@ -72,18 +108,14 @@ structure TensorStructure (R : Type) [CommSemiring R] where contrDual_symm : ∀ μ x y, (contrDual μ) (x ⊗ₜ[R] y) = (contrDual (τ μ)) (y ⊗ₜ[R] (Equiv.cast (congrArg ColorModule (τ_involutive μ).symm) x)) /-- The unit of the contraction. -/ - unit : (μ : Color) → ColorModule μ ⊗[R] ColorModule (τ μ) + unit : (μ : Color) → ColorModule (τ μ) ⊗[R] ColorModule μ /-- The unit is a right identity. -/ - unit_lid : ∀ μ (x : ColorModule μ), - TensorProduct.rid R _ - (TensorProduct.map (LinearEquiv.refl R (ColorModule μ)).toLinearMap - (contrDual μ ∘ₗ (TensorProduct.comm R _ _).toLinearMap) - ((TensorProduct.assoc R _ _ _) (unit μ ⊗ₜ[R] x))) = x + unit_rid : ∀ μ (x : ColorModule μ), TensorStructure.contrLeftAux (contrDual μ) (x ⊗ₜ[R] unit μ) = x /-- The metric for a given color. -/ metric : (μ : Color) → ColorModule μ ⊗[R] ColorModule μ /-- The metric contracted with its dual is the unit. -/ - metric_dual : ∀ (μ : Color), (contrDualMidAux (contrDual μ) - (metric μ ⊗ₜ[R] metric (τ μ))) = unit μ + metric_dual : ∀ (μ : Color), (TensorStructure.contrMidAux (contrDual μ) + (metric μ ⊗ₜ[R] metric (τ μ))) = TensorProduct.comm _ _ _ (unit μ) namespace TensorStructure @@ -92,7 +124,7 @@ variable (𝓣 : TensorStructure R) variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W] {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color} - {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color} + {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν η : 𝓣.Color} instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ @@ -107,6 +139,16 @@ instance : AddCommMonoid (𝓣.Tensor cX) := instance : Module R (𝓣.Tensor cX) := PiTensorProduct.instModule +/-! + +## Color + +Recall the `color` of an index describes the type of the index. + +For example, in a real Lorentz tensor the colors are `{up, down}`. + +-/ + /-- Equivalence of `ColorModule` given an equality of colors. -/ def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule ν where toFun := Equiv.cast (congrArg 𝓣.ColorModule h) @@ -120,6 +162,45 @@ def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModu left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x +/-- A relation on colors which is true if the two colors are equal or are duals. -/ +def colorRel (μ ν : 𝓣.Color) : Prop := μ = ν ∨ μ = 𝓣.τ ν + +/-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/ +def colorEquivRel : Equivalence 𝓣.colorRel where + refl := by + intro x + left + rfl + symm := by + intro x y h + rcases h with h | h + · left + exact h.symm + · right + subst h + exact (𝓣.τ_involutive y).symm + trans := by + intro x y z hxy hyz + rcases hxy with hxy | hxy <;> + rcases hyz with hyz | hyz <;> + subst hxy hyz + · left + rfl + · right + rfl + · right + rfl + · left + exact 𝓣.τ_involutive z + +/-- The structure of a setoid on colors, two colors are related if they are equal, + or dual. -/ +instance colorSetoid : Setoid 𝓣.Color := ⟨𝓣.colorRel, 𝓣.colorEquivRel⟩ + +/-- A map taking a color to its equivalence class in `colorSetoid`. -/ +def colorQuot (μ : 𝓣.Color) : Quotient 𝓣.colorSetoid := + Quotient.mk 𝓣.colorSetoid μ + lemma tensorProd_piTensorProd_ext {M : Type} [AddCommMonoid M] [Module R M] {f g : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] M} (h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q) @@ -479,6 +560,54 @@ lemma tensoratorEquiv_mapIso_tmul (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X) /-! +## contrDual properties + +-/ + +lemma contrDual_cast (h : μ = ν) (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ)) : + 𝓣.contrDual μ (x ⊗ₜ[R] y) = 𝓣.contrDual ν (𝓣.colorModuleCast h x ⊗ₜ[R] + 𝓣.colorModuleCast (congrArg 𝓣.τ h) y) := by + subst h + rfl + +/-- `𝓣.contrDual (𝓣.τ μ)` in terms of `𝓣.contrDual μ`. -/ +@[simp] +lemma contrDual_symm' (μ : 𝓣.Color) (x : 𝓣.ColorModule (𝓣.τ μ)) + (y : 𝓣.ColorModule (𝓣.τ (𝓣.τ μ))) : 𝓣.contrDual (𝓣.τ μ) (x ⊗ₜ[R] y) = + (𝓣.contrDual μ) ((𝓣.colorModuleCast (𝓣.τ_involutive μ) y) ⊗ₜ[R] x) := by + rw [𝓣.contrDual_symm, 𝓣.contrDual_cast (𝓣.τ_involutive μ)] + congr + simp [colorModuleCast] + +lemma contrDual_symm_contrRightAux (h : ν = η): + (𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ) = + contrRightAux (𝓣.contrDual (𝓣.τ (𝓣.τ μ))) ∘ₗ + (TensorProduct.congr (TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm)) + (𝓣.colorModuleCast ((𝓣.τ_involutive (𝓣.τ μ)).symm))).toLinearMap := by + apply TensorProduct.ext' + intro x y + refine TensorProduct.induction_on x (by simp) ?_ ?_ + · intro x z + simp [contrRightAux] + congr + simp [colorModuleCast] + simp [colorModuleCast] + · intro x z h1 h2 + simp [add_tmul, LinearMap.map_add, h1, h2] + +lemma contrDual_symm_contrRightAux_apply_tmul (h : ν = η) + (m : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule μ) (x : 𝓣.ColorModule (𝓣.τ μ)) : + 𝓣.colorModuleCast h (contrRightAux (𝓣.contrDual μ) (m ⊗ₜ[R] x)) = + contrRightAux (𝓣.contrDual (𝓣.τ (𝓣.τ μ))) + ((TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) (m)) ⊗ₜ + (𝓣.colorModuleCast (𝓣.τ_involutive (𝓣.τ μ)).symm x)) := by + trans ((𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ)) (m ⊗ₜ[R] x) + rfl + rw [contrDual_symm_contrRightAux] + rfl + +/-! + ## Splitting tensors into tensor products -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean index 782a131..bcaa215 100644 --- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Contraction.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 /-! # Contraction of indices @@ -30,9 +30,13 @@ We define a number of ways to contract indices of tensors: `𝓣.Tensor (Sum.elim cW cX) ⊗[R] 𝓣.Tensor (Sum.elim cY cZ) →ₗ[R] 𝓣.Tensor (Sum.elim cW cZ)` -/ + +/-! TODO: Define contraction based on an equivalence `(C ⊗ C) ⊗ P ≃ X` satisfying ... . -/ + noncomputable section open TensorProduct +open MulActionTensor variable {R : Type} [CommSemiring R] @@ -40,11 +44,14 @@ namespace TensorStructure variable (𝓣 : TensorStructure R) -variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] +variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W] + [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P] {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 /-! # Contractions of vectors @@ -55,7 +62,7 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [ `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in `𝓣.ColorModule η`. -/ def contrDualLeft {ν η : 𝓣.Color} : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η →ₗ[R] 𝓣.ColorModule η := - contrDualLeftAux (𝓣.contrDual ν) + contrLeftAux (𝓣.contrDual ν) /-- The contraction of a vector in `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν` with a vector in `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in @@ -63,7 +70,7 @@ def contrDualLeft {ν η : 𝓣.Color} : def contrDualMid {μ ν η : 𝓣.Color} : (𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν) ⊗[R] (𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η) →ₗ[R] 𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule η := - contrDualMidAux (𝓣.contrDual ν) + contrMidAux (𝓣.contrDual ν) /-- A linear map taking tensors mapped with the same index set to the product of paired tensors. -/ def pairProd : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cX2 →ₗ[R] @@ -248,4 +255,104 @@ def contrElim (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) : (TensorProduct.congr (𝓣.tensoratorEquiv cW cX).symm (𝓣.tensoratorEquiv cY cZ).symm).toLinearMap +/-! + +## Group acting on contraction + +-/ + +@[simp] +lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) : + 𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by + apply TensorProduct.ext' + refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by + intro a b hx hy y + simp [map_add, add_tmul, hx, hy]) + intro rx fx + refine fun y ↦ PiTensorProduct.induction_on' y ?_ (by + intro a b hx hy + simp at hx hy + simp [map_add, tmul_add, hx, hy]) + intro ry fy + simp [contrAll, TensorProduct.smul_tmul] + apply congrArg + apply congrArg + simp [contrAll'] + apply congrArg + simp [pairProd] + change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) = + (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) + rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod, + PiTensorProduct.map_tprod] + simp only [mk_apply] + apply congrArg + funext x + rw [← repColorModule_colorModuleCast_apply] + nth_rewrite 2 [← contrDual_inv (c x) g] + rfl + +@[simp] +lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) + (g : G) (x : 𝓣.Tensor c ⊗ 𝓣.Tensor d) : + 𝓣.contrAll e h (TensorProduct.map (𝓣.rep g) (𝓣.rep g) x) = 𝓣.contrAll e h x := by + change (𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x = _ + rw [contrAll_rep] + +@[simp] +lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) + (g : G) (x : 𝓣.Tensor c) (y : 𝓣.Tensor d) : + 𝓣.contrAll e h ((g • x) ⊗ₜ[R] (g • y)) = 𝓣.contrAll e h (x ⊗ₜ[R] y) := by + nth_rewrite 2 [← @contrAll_rep_apply R _ 𝓣 _ _ _ G] + rfl + +/-! + +## Contraction based on specification + +-/ + +lemma contr_cond (e : (C ⊕ C) ⊕ P ≃ X) : + cX = Sum.elim (Sum.elim (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inr)) ( + cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm := by + rw [Equiv.eq_comp_symm] + funext x + match x with + | Sum.inl (Sum.inl x) => rfl + | Sum.inl (Sum.inr x) => rfl + | Sum.inr x => rfl + +/-- Contraction of indices based on an equivalence `(C ⊕ C) ⊕ P ≃ X`. The indices + in `C` are contracted pair-wise, whilst the indices in `P` are preserved. -/ +def contr (e : (C ⊕ C) ⊕ P ≃ X) + (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr) : + 𝓣.Tensor cX →ₗ[R] 𝓣.Tensor (cX ∘ e ∘ Sum.inr) := + (TensorProduct.lid R _).toLinearMap ∘ₗ + (TensorProduct.map (𝓣.contrAll (Equiv.refl C) (by simpa using h)) LinearMap.id) ∘ₗ + (TensorProduct.congr (𝓣.tensoratorEquiv _ _).symm (LinearEquiv.refl R _)).toLinearMap ∘ₗ + (𝓣.tensoratorEquiv _ _).symm.toLinearMap ∘ₗ + (𝓣.mapIso e.symm (𝓣.contr_cond e)).toLinearMap + +/-- The contraction of indices via `contr` is equivariant. -/ +@[simp] +lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X) + (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr) + (g : G) (x : 𝓣.Tensor cX) : 𝓣.contr e h (g • x) = g • 𝓣.contr e h x := by + simp only [contr, TensorProduct.congr, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_symm, + LinearEquiv.refl_symm, LinearEquiv.ofLinear_toLinearMap, LinearEquiv.comp_coe, + LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply, + rep_mapIso_apply, rep_tensoratorEquiv_symm_apply] + rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp] + rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp] + rw [LinearMap.comp_assoc, rep_tensoratorEquiv_symm, ← LinearMap.comp_assoc] + simp only [contrAll_rep, LinearMap.comp_id, LinearMap.id_comp] + have h1 {M N A B : Type} [AddCommMonoid M] [AddCommMonoid N] + [AddCommMonoid A] [AddCommMonoid B] [Module R M] [Module R N] [Module R A] [Module R B] + (f : M →ₗ[R] N) (g : A →ₗ[R] B) : TensorProduct.map f g + = TensorProduct.map (LinearMap.id) g ∘ₗ TensorProduct.map f (LinearMap.id) := + ext rfl + rw [h1] + simp only [LinearMap.coe_comp, Function.comp_apply, rep_lid_apply] + rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp] + rfl + end TensorStructure diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean index 7116e7c..2753b5f 100644 --- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean +++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.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.Contraction +import HepLean.SpaceTime.LorentzTensor.Basic import Mathlib.RepresentationTheory.Basic /-! @@ -124,10 +124,10 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) : @[simp] lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) : - g • (𝓣.mapIso e h x) = (𝓣.mapIso e h) (g • x) := by + (𝓣.mapIso e h) (g • x) = g • (𝓣.mapIso e h x) := by trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x - rfl simp + rfl @[simp] lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) : @@ -170,54 +170,37 @@ lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) nth_rewrite 1 [← rep_tensoratorEquiv_apply] rfl -/-! - -## Group acting on contraction - --/ +lemma rep_tensoratorEquiv_symm (g : G) : + (𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g = (TensorProduct.map (𝓣.rep g) (𝓣.rep 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) @[simp] -lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) : - 𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by - apply TensorProduct.ext' - refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by - intro a b hx hy y - simp [map_add, add_tmul, hx, hy]) - intro rx fx - refine fun y ↦ PiTensorProduct.induction_on' y ?_ (by - intro a b hx hy - simp at hx hy - simp [map_add, tmul_add, hx, hy]) - intro ry fy - simp [contrAll, TensorProduct.smul_tmul] - apply congrArg - apply congrArg - simp [contrAll'] - apply congrArg - simp [pairProd] - change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) = - (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) - rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod, - PiTensorProduct.map_tprod] - simp only [mk_apply] - apply congrArg - funext x - rw [← repColorModule_colorModuleCast_apply] - nth_rewrite 2 [← contrDual_inv (c x) g] +lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) : + (𝓣.tensoratorEquiv cX cY).symm ((𝓣.rep g) x) = + (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) ((𝓣.tensoratorEquiv cX cY).symm x) := by + trans ((𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g) x + rfl + rw [rep_tensoratorEquiv_symm] rfl @[simp] -lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) - (g : G) (x : 𝓣.Tensor c ⊗ 𝓣.Tensor d) : - 𝓣.contrAll e h (TensorProduct.map (𝓣.rep g) (𝓣.rep g) x) = 𝓣.contrAll e h x := by - change (𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x = _ - rw [contrAll_rep] +lemma rep_lid (g : G) : TensorProduct.lid R (𝓣.Tensor cX) ∘ₗ + (TensorProduct.map (LinearMap.id) (𝓣.rep g)) = (𝓣.rep g) ∘ₗ + (TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap := by + apply TensorProduct.ext' + intro r y + simp @[simp] -lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) - (g : G) (x : 𝓣.Tensor c) (y : 𝓣.Tensor d) : - 𝓣.contrAll e h ((g • x) ⊗ₜ[R] (g • y)) = 𝓣.contrAll e h (x ⊗ₜ[R] y) := by - nth_rewrite 2 [← @contrAll_rep_apply R _ G] +lemma rep_lid_apply (g : G) (x : R ⊗[R] 𝓣.Tensor cX) : + (TensorProduct.lid R (𝓣.Tensor cX)) ((TensorProduct.map (LinearMap.id) (𝓣.rep g)) x) = + (𝓣.rep g) ((TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap x) := by + trans ((TensorProduct.lid R (𝓣.Tensor cX)) ∘ₗ (TensorProduct.map (LinearMap.id) (𝓣.rep g))) x + rfl + rw [rep_lid] rfl end TensorStructure diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean new file mode 100644 index 0000000..048651c --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean @@ -0,0 +1,171 @@ +/- +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 + +We use the term `dualize` to describe the more general version of rising and lowering of indices. + +In particular, rising and lowering indices corresponds taking the color of that index +to its dual. + +-/ + +noncomputable section + +open TensorProduct + +variable {R : Type} [CommSemiring R] + +namespace TensorStructure + +variable (𝓣 : TensorStructure R) + +variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] + [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W] + [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P] + {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 +open MulActionTensor + +/-! + +## Properties of the unit + +-/ + +/-! TODO: Move -/ + +lemma unit_lhs_eq (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ) ⊗[R] 𝓣.ColorModule μ) : + contrLeftAux (𝓣.contrDual μ) (x ⊗ₜ[R] y) = + (contrRightAux (𝓣.contrDual (𝓣.τ μ))) ((TensorProduct.comm R _ _) y + ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) := by + refine TensorProduct.induction_on y (by simp) ?_ (fun z1 z2 h1 h2 => ?_) + intro x1 x2 + simp only [contrRightAux, LinearEquiv.refl_toLinearMap, comm_tmul, colorModuleCast, + Equiv.cast_symm, LinearEquiv.coe_mk, Equiv.cast_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, contrDual_symm', cast_cast, + cast_eq, rid_tmul] + rfl + simp [LinearMap.map_add, add_tmul] + rw [← h1, ← h2, tmul_add, LinearMap.map_add] + + +@[simp] +lemma unit_lid : (contrRightAux (𝓣.contrDual (𝓣.τ μ))) ((TensorProduct.comm R _ _) (𝓣.unit μ) + ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) = x := by + have h1 := 𝓣.unit_rid μ x + rw [← unit_lhs_eq] + exact h1 + +/-! + +## Properties of the metric + +-/ + +@[simp] +lemma metric_cast (h : μ = ν) : + (TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast h)) (𝓣.metric μ) = + 𝓣.metric ν := by + subst h + erw [congr_refl_refl] + simp only [LinearEquiv.refl_apply] + + + +@[simp] +lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ ) : + (contrRightAux (𝓣.contrDual μ)) (𝓣.metric μ ⊗ₜ[R] + ((contrRightAux (𝓣.contrDual (𝓣.τ μ))) + (𝓣.metric (𝓣.τ μ) ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm x)))) = x := by + change (contrRightAux (𝓣.contrDual μ) ∘ₗ TensorProduct.map (LinearMap.id) + (contrRightAux (𝓣.contrDual (𝓣.τ μ)))) (𝓣.metric μ + ⊗ₜ[R] 𝓣.metric (𝓣.τ μ) ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm x)) = _ + rw [contrRightAux_comp] + simp + rw [𝓣.metric_dual] + simp only [unit_lid] + +/-! + +## Dualizing + +-/ + +def dualizeSymm (μ : 𝓣.Color) : 𝓣.ColorModule (𝓣.τ μ) →ₗ[R] 𝓣.ColorModule μ := + contrRightAux (𝓣.contrDual μ) ∘ₗ + TensorProduct.lTensorHomToHomLTensor R _ _ _ (𝓣.metric μ ⊗ₜ[R] LinearMap.id) + +def dualizeFun (μ : 𝓣.Color) : 𝓣.ColorModule μ →ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := + 𝓣.dualizeSymm (𝓣.τ μ) ∘ₗ (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm).toLinearMap + +def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := by + refine LinearEquiv.ofLinear (𝓣.dualizeFun μ) (𝓣.dualizeSymm μ) ?_ ?_ + · apply LinearMap.ext + intro x + simp [dualizeFun, dualizeSymm, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq, + contrDual_symm_contrRightAux_apply_tmul, metric_cast] + · apply LinearMap.ext + intro x + simp only [dualizeSymm, dualizeFun, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq, + metric_contrRight_unit] + +def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by + refine LinearEquiv.ofLinear + (PiTensorProduct.map (fun x => (𝓣.dualizeModule (cX x)).toLinearMap)) + (PiTensorProduct.map (fun x => (𝓣.dualizeModule (cX x)).symm.toLinearMap)) ?_ ?_ + all_goals + apply LinearMap.ext + refine fun x ↦ 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.map _) ((PiTensorProduct.tprod R) fx)) = _ + rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod] + apply congrArg + 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] + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => rfl + +lemma dualize_cond' (e : C ⊕ P ≃ X) : + Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) = + (Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm) ∘ ⇑e := by + funext x + match x with + | Sum.inl x => simp + | Sum.inr x => simp + +/-! TODO: Show that `dualize` is equivariant with respect to the group action. -/ + +def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R] + 𝓣.Tensor (Sum.elim (𝓣.τ ∘ cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm) := + 𝓣.mapIso e.symm (𝓣.dualize_cond e) ≪≫ₗ + (𝓣.tensoratorEquiv _ _).symm ≪≫ₗ + TensorProduct.congr 𝓣.dualizeAll (LinearEquiv.refl _ _) ≪≫ₗ + (𝓣.tensoratorEquiv _ _) ≪≫ₗ + 𝓣.mapIso e (𝓣.dualize_cond' e) + +end TensorStructure + +end