diff --git a/HepLean.lean b/HepLean.lean index 840ed79..8e6ee22 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -76,6 +76,7 @@ import HepLean.SpaceTime.LorentzTensor.Fin import HepLean.SpaceTime.LorentzTensor.MulActionTensor import HepLean.SpaceTime.LorentzTensor.Notation import HepLean.SpaceTime.LorentzTensor.Real.Basic +import HepLean.SpaceTime.LorentzTensor.RisingLowering import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix import HepLean.SpaceTime.LorentzVector.Basic import HepLean.SpaceTime.LorentzVector.Contraction diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index e883bd6..8bfb6f7 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -44,6 +44,7 @@ def contrLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCom TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap +/-- An auxillary function to contract the vector space `V1` and `V2` in `(V3 ⊗[R] V1) ⊗[R] V2`. -/ 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 := @@ -51,7 +52,6 @@ def contrRightAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCo 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 contrMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] @@ -60,30 +60,28 @@ def contrMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddC (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) : +lemma contrRightAux_comp {V1 V2 V3 V4 V5 : Type} [AddCommMonoid V1] [AddCommMonoid V2] + [AddCommMonoid V3] [AddCommMonoid V4] [AddCommMonoid V5] [Module R V1] [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 => + 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 => + 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 => + 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 @@ -110,7 +108,8 @@ structure TensorStructure (R : Type) [CommSemiring R] where /-- The unit of the contraction. -/ unit : (μ : Color) → ColorModule (τ μ) ⊗[R] ColorModule μ /-- The unit is a right identity. -/ - unit_rid : ∀ μ (x : ColorModule μ), TensorStructure.contrLeftAux (contrDual μ) (x ⊗ₜ[R] unit μ) = 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. -/ @@ -166,7 +165,7 @@ def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModu 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 +lemma colorRel_equivalence : Equivalence 𝓣.colorRel where refl := by intro x left @@ -195,7 +194,7 @@ def colorEquivRel : Equivalence 𝓣.colorRel where /-- The structure of a setoid on colors, two colors are related if they are equal, or dual. -/ -instance colorSetoid : Setoid 𝓣.Color := ⟨𝓣.colorRel, 𝓣.colorEquivRel⟩ +instance colorSetoid : Setoid 𝓣.Color := ⟨𝓣.colorRel, 𝓣.colorRel_equivalence⟩ /-- A map taking a color to its equivalence class in `colorSetoid`. -/ def colorQuot (μ : 𝓣.Color) : Quotient 𝓣.colorSetoid := @@ -579,14 +578,15 @@ lemma contrDual_symm' (μ : 𝓣.Color) (x : 𝓣.ColorModule (𝓣.τ μ)) congr simp [colorModuleCast] -lemma contrDual_symm_contrRightAux (h : ν = η): +lemma contrDual_symm_contrRightAux (h : ν = η) : (𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ) = contrRightAux (𝓣.contrDual (𝓣.τ (𝓣.τ μ))) ∘ₗ - (TensorProduct.congr (TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm)) + (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) ?_ ?_ + refine TensorProduct.induction_on x (by simp) ?_ ?_ · intro x z simp [contrRightAux] congr @@ -598,9 +598,9 @@ lemma contrDual_symm_contrRightAux (h : ν = η): 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 + 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] diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean index bcaa215..fed8eab 100644 --- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean @@ -347,7 +347,7 @@ lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X) 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 + (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] diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean index 2753b5f..46e9f14 100644 --- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean +++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean @@ -124,7 +124,7 @@ 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) : - (𝓣.mapIso e h) (g • x) = g • (𝓣.mapIso e h x) := by + (𝓣.mapIso e h) (g • x) = g • (𝓣.mapIso e h x) := by trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x simp rfl @@ -171,7 +171,7 @@ lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) rfl lemma rep_tensoratorEquiv_symm (g : G) : - (𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g = (TensorProduct.map (𝓣.rep g) (𝓣.rep 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] @@ -187,9 +187,9 @@ lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) rfl @[simp] -lemma rep_lid (g : G) : TensorProduct.lid R (𝓣.Tensor cX) ∘ₗ +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 + (TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap := by apply TensorProduct.ext' intro r y simp diff --git a/HepLean/SpaceTime/LorentzTensor/Notation.lean b/HepLean/SpaceTime/LorentzTensor/Notation.lean index f21fcf0..7990f0d 100644 --- a/HepLean/SpaceTime/LorentzTensor/Notation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Notation.lean @@ -27,4 +27,7 @@ Further we plan to make easy to define tensors with indices. E.g. `(ψ : Tenᵘ For `(ψ : Tenᵘ¹ᵘ²ᵤ₃)`, if one writes e.g. `ψᵤ₁ᵘ²ᵤ₃`, this should correspond to a lowering of the first index of `ψ`. +Further, it will be nice if we can have implicit contractions of indices + e.g. in Weyl fermions. + -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index 2196328..745565e 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -75,10 +75,10 @@ def realLorentzTensor (d : ℕ) : TensorStructure ℝ where match μ with | .up => LorentzVector.unitUp | .down => LorentzVector.unitDown - unit_lid μ := + unit_rid μ := match μ with - | .up => LorentzVector.unitUp_lid - | .down => LorentzVector.unitDown_lid + | .up => LorentzVector.unitUp_rid + | .down => LorentzVector.unitDown_rid metric μ := match μ with | realTensor.ColorType.up => asProdLorentzVector diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean index 048651c..450b099 100644 --- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean +++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean @@ -4,7 +4,6 @@ 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 @@ -32,10 +31,6 @@ 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 -open MulActionTensor - /-! ## Properties of the unit @@ -45,10 +40,10 @@ open MulActionTensor /-! TODO: Move -/ lemma unit_lhs_eq (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ) ⊗[R] 𝓣.ColorModule μ) : - contrLeftAux (𝓣.contrDual μ) (x ⊗ₜ[R] y) = + 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 => ?_) + 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, @@ -58,10 +53,9 @@ lemma unit_lhs_eq (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ) 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 + ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) = x := by have h1 := 𝓣.unit_rid μ x rw [← unit_lhs_eq] exact h1 @@ -80,18 +74,17 @@ lemma metric_cast (h : μ = ν) : erw [congr_refl_refl] simp only [LinearEquiv.refl_apply] - - @[simp] -lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ ) : - (contrRightAux (𝓣.contrDual μ)) (𝓣.metric μ ⊗ₜ[R] +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 + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, + map_tmul, LinearMap.id_coe, id_eq] rw [𝓣.metric_dual] simp only [unit_lid] @@ -101,13 +94,19 @@ lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ ) : -/ -def dualizeSymm (μ : 𝓣.Color) : 𝓣.ColorModule (𝓣.τ μ) →ₗ[R] 𝓣.ColorModule μ := - contrRightAux (𝓣.contrDual μ) ∘ₗ +/-- Takes a vector with index with dual color to a vector with index the underlying color. + Obtained by contraction with the metric. -/ +def dualizeSymm (μ : 𝓣.Color) : 𝓣.ColorModule (𝓣.τ μ) →ₗ[R] 𝓣.ColorModule μ := + contrRightAux (𝓣.contrDual μ) ∘ₗ TensorProduct.lTensorHomToHomLTensor R _ _ _ (𝓣.metric μ ⊗ₜ[R] LinearMap.id) -def dualizeFun (μ : 𝓣.Color) : 𝓣.ColorModule μ →ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := +/-- Takes a vector to a vector with the dual color index. + Obtained by contraction with the metric. -/ +def dualizeFun (μ : 𝓣.Color) : 𝓣.ColorModule μ →ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := 𝓣.dualizeSymm (𝓣.τ μ) ∘ₗ (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm).toLinearMap +/-- Equivalence between the module with a color `μ` and the module with color + `𝓣.τ μ` obtained by contraction with the metric. -/ def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := by refine LinearEquiv.ofLinear (𝓣.dualizeFun μ) (𝓣.dualizeSymm μ) ?_ ?_ · apply LinearMap.ext @@ -121,6 +120,7 @@ def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorMo Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq, metric_contrRight_unit] +/-- 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 (PiTensorProduct.map (fun x => (𝓣.dualizeModule (cX x)).toLinearMap)) @@ -132,7 +132,8 @@ def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by simp [map_add, add_tmul, hx] simp_all only [Function.comp_apply, LinearMap.coe_comp, LinearMap.id_coe, id_eq]) intro rx fx - simp + simp only [Function.comp_apply, PiTensorProduct.tprodCoeff_eq_smul_tprod, + LinearMapClass.map_smul, LinearMap.coe_comp, LinearMap.id_coe, id_eq] apply congrArg change (PiTensorProduct.map _) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fx)) = _ @@ -158,6 +159,8 @@ lemma dualize_cond' (e : C ⊕ P ≃ X) : /-! TODO: Show that `dualize` is equivariant with respect to the group action. -/ +/-- Given an equivalence `C ⊕ P ≃ X` dualizes those indices of a tensor which correspond to + `C` whilst leaving the indices `P` invariant. -/ 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) ≪≫ₗ diff --git a/HepLean/SpaceTime/LorentzVector/Contraction.lean b/HepLean/SpaceTime/LorentzVector/Contraction.lean index 0e0001c..21c6e3a 100644 --- a/HepLean/SpaceTime/LorentzVector/Contraction.lean +++ b/HepLean/SpaceTime/LorentzVector/Contraction.lean @@ -115,37 +115,32 @@ lemma contrDownUp_tmul_eq_dotProduct {x : CovariantLorentzVector d} {y : Lorentz /-- The unit of the contraction of contravariant Lorentz vector and a covariant Lorentz vector. -/ -def unitUp : LorentzVector d ⊗[ℝ] CovariantLorentzVector d := - ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i +def unitUp : CovariantLorentzVector d ⊗[ℝ] LorentzVector d := + ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i -lemma unitUp_lid (x : LorentzVector d) : - TensorProduct.rid ℝ _ - (TensorProduct.map (LinearEquiv.refl ℝ _).toLinearMap - (contrUpDown ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap) - ((TensorProduct.assoc ℝ _ _ _) (unitUp ⊗ₜ[ℝ] x))) = x := by - simp only [LinearEquiv.refl_toLinearMap, unitUp] - rw [sum_tmul] - simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.sum_singleton, map_add, assoc_tmul, map_sum, map_tmul, LinearMap.id_coe, id_eq, - LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul, - contrUpDown_stdBasis_left, rid_tmul, decomp_stdBasis'] +lemma unitUp_rid (x : LorentzVector d) : + TensorStructure.contrLeftAux contrUpDown (x ⊗ₜ[ℝ] unitUp) = x := by + simp only [unitUp, LinearEquiv.refl_toLinearMap] + rw [tmul_sum] + simp only [TensorStructure.contrLeftAux, LinearEquiv.refl_toLinearMap, Fintype.sum_sum_type, + Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, map_add, + LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul, + contrUpDown_stdBasis_left, LinearMap.id_coe, id_eq, lid_tmul, map_sum, decomp_stdBasis'] /-- The unit of the contraction of covariant Lorentz vector and a contravariant Lorentz vector. -/ -def unitDown : CovariantLorentzVector d ⊗[ℝ] LorentzVector d := - ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i +def unitDown : LorentzVector d ⊗[ℝ] CovariantLorentzVector d := + ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i -lemma unitDown_lid (x : CovariantLorentzVector d) : - TensorProduct.rid ℝ _ - (TensorProduct.map (LinearEquiv.refl ℝ _).toLinearMap - (contrDownUp ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap) - ((TensorProduct.assoc ℝ _ _ _) (unitDown ⊗ₜ[ℝ] x))) = x := by - simp only [LinearEquiv.refl_toLinearMap, unitDown] - rw [sum_tmul] - simp only [contrDownUp, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, - Fin.isValue, Finset.sum_singleton, map_add, assoc_tmul, map_sum, map_tmul, LinearMap.id_coe, - id_eq, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul, - contrUpDown_stdBasis_right, rid_tmul, CovariantLorentzVector.decomp_stdBasis'] +lemma unitDown_rid (x : CovariantLorentzVector d) : + TensorStructure.contrLeftAux contrDownUp (x ⊗ₜ[ℝ] unitDown) = x := by + simp only [unitDown, LinearEquiv.refl_toLinearMap] + rw [tmul_sum] + simp only [TensorStructure.contrLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap, + Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton, map_add, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + assoc_symm_tmul, map_tmul, comm_tmul, contrUpDown_stdBasis_right, LinearMap.id_coe, id_eq, + lid_tmul, map_sum, CovariantLorentzVector.decomp_stdBasis'] /-! @@ -175,6 +170,7 @@ end LorentzVector namespace minkowskiMatrix open LorentzVector +open TensorStructure open scoped minkowskiMatrix variable {d : ℕ} @@ -188,37 +184,39 @@ def asProdCovariantLorentzVector : CovariantLorentzVector d ⊗[ℝ] CovariantLo @[simp] lemma contrLeft_asProdLorentzVector (x : CovariantLorentzVector d) : - contrDualLeftAux contrDownUp (x ⊗ₜ[ℝ] asProdLorentzVector) = + contrLeftAux contrDownUp (x ⊗ₜ[ℝ] asProdLorentzVector) = ∑ μ, ((η μ μ * x μ) • LorentzVector.stdBasis μ) := by simp only [asProdLorentzVector] rw [tmul_sum] rw [map_sum] refine Finset.sum_congr rfl (fun μ _ => ?_) - simp only [contrDualLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap, tmul_smul, map_smul, + simp only [contrLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap, tmul_smul, map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul, comm_tmul, contrUpDown_stdBasis_right, LinearMap.id_coe, id_eq, lid_tmul] exact smul_smul (η μ μ) (x μ) (e μ) @[simp] lemma contrLeft_asProdCovariantLorentzVector (x : LorentzVector d) : - contrDualLeftAux contrUpDown (x ⊗ₜ[ℝ] asProdCovariantLorentzVector) = + contrLeftAux contrUpDown (x ⊗ₜ[ℝ] asProdCovariantLorentzVector) = ∑ μ, ((η μ μ * x μ) • CovariantLorentzVector.stdBasis μ) := by simp only [asProdCovariantLorentzVector] rw [tmul_sum] rw [map_sum] refine Finset.sum_congr rfl (fun μ _ => ?_) - simp only [contrDualLeftAux, LinearEquiv.refl_toLinearMap, tmul_smul, LinearMapClass.map_smul, + simp only [contrLeftAux, LinearEquiv.refl_toLinearMap, tmul_smul, LinearMapClass.map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul, contrUpDown_stdBasis_left, LinearMap.id_coe, id_eq, lid_tmul] exact smul_smul (η μ μ) (x μ) (CovariantLorentzVector.stdBasis μ) @[simp] lemma asProdLorentzVector_contr_asCovariantProdLorentzVector : - (contrDualMidAux (contrUpDown) (asProdLorentzVector ⊗ₜ[ℝ] asProdCovariantLorentzVector)) - = @unitUp d := by - simp only [contrDualMidAux, LinearEquiv.refl_toLinearMap, asProdLorentzVector, LinearMap.coe_comp, + (contrMidAux (contrUpDown) (asProdLorentzVector ⊗ₜ[ℝ] asProdCovariantLorentzVector)) + = TensorProduct.comm ℝ _ _ (@unitUp d) := by + simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdLorentzVector, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] rw [sum_tmul, map_sum, map_sum, unitUp] + simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton, map_add, comm_tmul, map_sum] refine Finset.sum_congr rfl (fun μ _ => ?_) rw [← tmul_smul, TensorProduct.assoc_tmul] simp only [map_tmul, LinearMap.id_coe, id_eq, contrLeft_asProdCovariantLorentzVector] @@ -239,11 +237,13 @@ lemma asProdLorentzVector_contr_asCovariantProdLorentzVector : @[simp] lemma asProdCovariantLorentzVector_contr_asProdLorentzVector : - (contrDualMidAux (contrDownUp) (asProdCovariantLorentzVector ⊗ₜ[ℝ] asProdLorentzVector)) - = @unitDown d := by - simp only [contrDualMidAux, LinearEquiv.refl_toLinearMap, asProdCovariantLorentzVector, + (contrMidAux (contrDownUp) (asProdCovariantLorentzVector ⊗ₜ[ℝ] asProdLorentzVector)) + = TensorProduct.comm ℝ _ _ (@unitDown d) := by + simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdCovariantLorentzVector, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] rw [sum_tmul, map_sum, map_sum, unitDown] + simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton, map_add, comm_tmul, map_sum] refine Finset.sum_congr rfl (fun μ _ => ?_) rw [smul_tmul, TensorProduct.assoc_tmul] simp only [tmul_smul, LinearMapClass.map_smul, map_tmul, LinearMap.id_coe, id_eq,