diff --git a/HepLean.lean b/HepLean.lean index 4cf002a..f0338a0 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -70,11 +70,7 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.LorentzGroup.Restricted import HepLean.SpaceTime.LorentzGroup.Rotations -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.LorentzTensor.Basic import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix import HepLean.SpaceTime.LorentzVector.Basic import HepLean.SpaceTime.LorentzVector.NormOne diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean new file mode 100644 index 0000000..6916a37 --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -0,0 +1,826 @@ +/- +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 Mathlib.LinearAlgebra.PiTensorProduct +import Mathlib.RepresentationTheory.Basic +/-! + +# Structure of Lorentz Tensors + +In this file we set up the basic structures we will use to define Lorentz tensors. + +## References + +-- For modular operads see: [Raynor][raynor2021graphical] + +-/ + +noncomputable section + +open TensorProduct + +variable {R : Type} [CommSemiring R] + +/-- An initial structure specifying a tensor system (e.g. a system in which you can + define real Lorentz tensors). -/ +structure PreTensorStructure (R : Type) [CommSemiring R] where + /-- The allowed colors of indices. + For example for a real Lorentz tensor these are `{up, down}`. -/ + Color : Type + /-- To each color we associate a module. -/ + ColorModule : Color → Type + /-- A map taking every color to its dual color. -/ + τ : Color → Color + /-- The map `τ` is an involution. -/ + τ_involutive : Function.Involutive τ + /-- Each `ColorModule` has the structure of an additive commutative monoid. -/ + colorModule_addCommMonoid : ∀ μ, AddCommMonoid (ColorModule μ) + /-- Each `ColorModule` has the structure of a module over `R`. -/ + colorModule_module : ∀ μ, Module R (ColorModule μ) + /-- The contraction of a vector with a vector with dual color. -/ + contrDual : ∀ μ, ColorModule μ ⊗[R] ColorModule (τ μ) →ₗ[R] R + +namespace PreTensorStructure + +variable (𝓣 : PreTensorStructure 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} + +instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ + +instance : Module R (𝓣.ColorModule μ) := 𝓣.colorModule_module μ + +/-- The type of tensors given a map from an indexing set `X` to the type of colors, + specifying the color of that index. -/ +def Tensor (c : X → 𝓣.Color) : Type := ⨂[R] x, 𝓣.ColorModule (c x) + +instance : AddCommMonoid (𝓣.Tensor cX) := + PiTensorProduct.instAddCommMonoid fun i => 𝓣.ColorModule (cX i) + +instance : Module R (𝓣.Tensor cX) := PiTensorProduct.instModule + +/-- Equivalence of `ColorModule` given an equality of colors. -/ +def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule ν where + toFun x := Equiv.cast (congrArg 𝓣.ColorModule h) x + invFun x := (Equiv.cast (congrArg 𝓣.ColorModule h)).symm x + map_add' x y := by + subst h + rfl + map_smul' x y := by + subst h + rfl + 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 + +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) + = g (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)) : f = g := 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 only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, LinearMapClass.map_smul] + apply congrArg + simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul] + exact congrArg (HSMul.hSMul rx) (h fx fy) + +/-! + +## Mapping isomorphisms + +-/ + +/-- An linear equivalence of tensor spaces given a color-preserving equivalence of indexing sets. -/ +def mapIso {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) : + 𝓣.Tensor c ≃ₗ[R] 𝓣.Tensor d := + (PiTensorProduct.reindex R _ e) ≪≫ₗ + (PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp))) + +lemma mapIso_trans_cond {e : X ≃ Y} {e' : Y ≃ Z} (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') : + cX = cZ ∘ (e.trans e') := by + funext a + subst h h' + simp + +@[simp] +lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') : + (𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') := by + refine LinearEquiv.toLinearMap_inj.mp ?_ + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro x + simp only [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, + LinearEquiv.trans_apply, PiTensorProduct.reindex_tprod, Equiv.symm_trans_apply] + change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cY x)) e') + ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) _)) = + (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cX x)) (e.trans e')) _) + rw [PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod, + PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod, PiTensorProduct.congr] + simp [colorModuleCast] + +@[simp] +lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') + (T : 𝓣.Tensor cX) : + (𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') T := by + rw [← LinearEquiv.trans_apply, mapIso_trans] + +@[simp] +lemma mapIso_symm (e : X ≃ Y) (h : cX = cY ∘ e) : + (𝓣.mapIso e h).symm = 𝓣.mapIso e.symm ((Equiv.eq_comp_symm e cY cX).mpr h.symm) := by + refine LinearEquiv.toLinearMap_inj.mp ?_ + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro x + simp [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, + LinearEquiv.symm_apply_apply, PiTensorProduct.reindex_tprod] + change (PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cX x)) e).symm + ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _).symm ((PiTensorProduct.tprod R) x)) = + (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cY x)) e.symm) + ((PiTensorProduct.tprod R) x)) + rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod, PiTensorProduct.congr_symm_tprod, + LinearEquiv.symm_apply_eq, PiTensorProduct.reindex_tprod] + apply congrArg + funext i + simp only [colorModuleCast, Equiv.cast_symm, LinearEquiv.coe_symm_mk, + Equiv.symm_symm_apply, LinearEquiv.coe_mk] + rw [← Equiv.symm_apply_eq] + simp only [Equiv.cast_symm, Equiv.cast_apply, cast_cast] + apply cast_eq_iff_heq.mpr + rw [Equiv.apply_symm_apply] + +@[simp] +lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : cX = cX) = LinearEquiv.refl R _ := by + refine LinearEquiv.toLinearMap_inj.mp ?_ + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro x + simp only [mapIso, Equiv.refl_symm, Equiv.refl_apply, PiTensorProduct.reindex_refl, + LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply, + LinearEquiv.refl_apply, LinearEquiv.refl_toLinearMap, LinearMap.id, LinearMap.coe_mk, + AddHom.coe_mk, id_eq] + change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) ((PiTensorProduct.tprod R) x) = _ + rw [PiTensorProduct.congr_tprod] + rfl + +@[simp] +lemma mapIso_tprod {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) + (f : (i : X) → 𝓣.ColorModule (c i)) : (𝓣.mapIso e h) (PiTensorProduct.tprod R f) = + (PiTensorProduct.tprod R (fun i => 𝓣.colorModuleCast (by rw [h]; simp) (f (e.symm i)))) := by + simp [mapIso] + change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R _ e) ((PiTensorProduct.tprod R) f)) = _ + rw [PiTensorProduct.reindex_tprod] + exact PiTensorProduct.congr_tprod (fun y => 𝓣.colorModuleCast _) fun i => f (e.symm i) + +/-! + +## Pure tensors + +This section is needed since: `PiTensorProduct.tmulEquiv` is not defined for dependent types. +Hence we need to construct a version of it here. + +-/ + +/-- The type of pure tensors, i.e. of the form `v1 ⊗ v2 ⊗ v3 ⊗ ...`. -/ +abbrev PureTensor (c : X → 𝓣.Color) := (x : X) → 𝓣.ColorModule (c x) + +/-- A pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` constructed from a pure tensor + in `𝓣.PureTensor cX` and a pure tensor in `𝓣.PureTensor cY`. -/ +def elimPureTensor (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) : 𝓣.PureTensor (Sum.elim cX cY) := + fun x => + match x with + | Sum.inl x => p x + | Sum.inr x => q x + +@[simp] +lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) + (y : Y) (r : 𝓣.ColorModule (cY y)) : 𝓣.elimPureTensor p (Function.update q y r) = + Function.update (𝓣.elimPureTensor p q) (Sum.inr y) r := by + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => + change Function.update q y r x = _ + simp only [Function.update, Sum.inr.injEq, Sum.elim_inr] + split_ifs + rename_i h + subst h + simp_all only + rfl + +@[simp] +lemma elimPureTensor_update_left (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) + (x : X) (r : 𝓣.ColorModule (cX x)) : 𝓣.elimPureTensor (Function.update p x r) q = + Function.update (𝓣.elimPureTensor p q) (Sum.inl x) r := by + funext y + match y with + | Sum.inl y => + change (Function.update p x r) y = _ + simp only [Function.update, Sum.inl.injEq, Sum.elim_inl] + split_ifs + rename_i h + subst h + simp_all only + rfl + | Sum.inr y => rfl + +/-- The projection of a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` onto a pure tensor in + `𝓣.PureTensor cX`. -/ +def inlPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cX := fun x => p (Sum.inl x) + +/-- The projection of a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` onto a pure tensor in + `𝓣.PureTensor cY`. -/ +def inrPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cY := fun y => p (Sum.inr y) + +@[simp] +lemma inlPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X) + (v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) : + 𝓣.inlPureTensor (Function.update f (Sum.inl x) v1) = + Function.update (𝓣.inlPureTensor f) x v1 := by + funext y + simp [inlPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl] + split + next h => + subst h + simp_all only + rfl + +@[simp] +lemma inrPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X) + (v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) : + 𝓣.inrPureTensor (Function.update f (Sum.inl x) v1) = (𝓣.inrPureTensor f) := by + funext x + simp [inrPureTensor, Function.update] + +@[simp] +lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y) + (v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) : + 𝓣.inrPureTensor (Function.update f (Sum.inr y) v1) = + Function.update (𝓣.inrPureTensor f) y v1 := by + funext y + simp [inrPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl] + split + next h => + subst h + simp_all only + rfl + +@[simp] +lemma inlPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y) + (v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) : + 𝓣.inlPureTensor (Function.update f (Sum.inr y) v1) = (𝓣.inlPureTensor f) := by + funext x + simp [inlPureTensor, Function.update] + +/-- The multilinear map taking pure tensors a `𝓣.PureTensor cX` and a pure tensor in + `𝓣.PureTensor cY`, and constructing a tensor in `𝓣.Tensor (Sum.elim cX cY))`. -/ +def elimPureTensorMulLin : MultilinearMap R (fun i => 𝓣.ColorModule (cX i)) + (MultilinearMap R (fun x => 𝓣.ColorModule (cY x)) (𝓣.Tensor (Sum.elim cX cY))) where + toFun p := { + toFun := fun q => PiTensorProduct.tprod R (𝓣.elimPureTensor p q) + map_add' := fun m x v1 v2 => by + simp [Sum.elim_inl, Sum.elim_inr] + map_smul' := fun m x r v => by + simp [Sum.elim_inl, Sum.elim_inr]} + map_add' p x v1 v2 := by + apply MultilinearMap.ext + intro y + simp + map_smul' p x r v := by + apply MultilinearMap.ext + intro y + simp + +/-! + +## tensorator + +-/ + +/-! TODO: Replace with dependent type version of `MultilinearMap.domCoprod` when in Mathlib. -/ +/-- The multi-linear map taking a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` and constructing + a vector in `𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY`. -/ +def domCoprod : MultilinearMap R (fun x => 𝓣.ColorModule (Sum.elim cX cY x)) + (𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) where + toFun f := (PiTensorProduct.tprod R (𝓣.inlPureTensor f)) ⊗ₜ + (PiTensorProduct.tprod R (𝓣.inrPureTensor f)) + map_add' f xy v1 v2:= by + match xy with + | Sum.inl x => simp [← TensorProduct.add_tmul] + | Sum.inr y => simp [← TensorProduct.tmul_add] + map_smul' f xy r p := by + match xy with + | Sum.inl x => simp [TensorProduct.tmul_smul, TensorProduct.smul_tmul] + | Sum.inr y => simp [TensorProduct.tmul_smul, TensorProduct.smul_tmul] + +/-- The linear map combining two tensors into a single tensor + via the tensor product i.e. `v1 v2 ↦ v1 ⊗ v2`. -/ +def tensoratorSymm : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] 𝓣.Tensor (Sum.elim cX cY) := by + refine TensorProduct.lift { + toFun := fun a ↦ + PiTensorProduct.lift <| + PiTensorProduct.lift (𝓣.elimPureTensorMulLin) a, + map_add' := fun a b ↦ by simp + map_smul' := fun r a ↦ by simp} + +/-! TODO: Replace with dependent type version of `PiTensorProduct.tmulEquiv` when in Mathlib. -/ +/-- Splitting a tensor in `𝓣.Tensor (Sum.elim cX cY)` into the tensor product of two tensors. -/ +def tensorator : 𝓣.Tensor (Sum.elim cX cY) →ₗ[R] 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY := + PiTensorProduct.lift 𝓣.domCoprod + +/-- An equivalence formed by taking the tensor product of tensors. -/ +def tensoratorEquiv (c : X → 𝓣.Color) (d : Y → 𝓣.Color) : + 𝓣.Tensor c ⊗[R] 𝓣.Tensor d ≃ₗ[R] 𝓣.Tensor (Sum.elim c d) := + LinearEquiv.ofLinear (𝓣.tensoratorSymm) (𝓣.tensorator) + (by + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro p + simp [tensorator, tensoratorSymm, domCoprod] + change (PiTensorProduct.lift _) ((PiTensorProduct.tprod R) _) = + LinearMap.id ((PiTensorProduct.tprod R) p) + rw [PiTensorProduct.lift.tprod] + simp [elimPureTensorMulLin, elimPureTensor] + change (PiTensorProduct.tprod R) _ = _ + apply congrArg + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => rfl) + (by + apply tensorProd_piTensorProd_ext + intro p q + simp [tensorator, tensoratorSymm] + change (PiTensorProduct.lift 𝓣.domCoprod) + ((PiTensorProduct.lift (𝓣.elimPureTensorMulLin p)) ((PiTensorProduct.tprod R) q)) =_ + rw [PiTensorProduct.lift.tprod] + simp [elimPureTensorMulLin] + rfl) + +@[simp] +lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) : + (𝓣.tensoratorEquiv cX cY) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) = + (PiTensorProduct.tprod R) (𝓣.elimPureTensor p q) := by + simp only [tensoratorEquiv, tensoratorSymm, tensorator, domCoprod, LinearEquiv.ofLinear_apply, + lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod] + exact PiTensorProduct.lift.tprod q + +lemma tensoratorEquiv_mapIso_cond {e : X ≃ Y} {e' : Z ≃ Y} {e'' : W ≃ X} + (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') : + Sum.elim bW cZ = Sum.elim cX cY ∘ ⇑(e''.sumCongr e') := by + subst h h' h'' + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => rfl + +@[simp] +lemma tensoratorEquiv_mapIso (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X) + (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') : + (TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ (𝓣.tensoratorEquiv cX cY) + = (𝓣.tensoratorEquiv bW cZ) + ≪≫ₗ (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h'')) := by + apply LinearEquiv.toLinearMap_inj.mp + apply tensorProd_piTensorProd_ext + intro p q + simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, mapIso_tprod, + tensoratorEquiv_tmul_tprod, Equiv.sumCongr_symm, Equiv.sumCongr_apply] + apply congrArg + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => rfl + +@[simp] +lemma tensoratorEquiv_mapIso_apply (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X) + (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'') + (x : 𝓣.Tensor cW ⊗[R] 𝓣.Tensor cZ) : + (𝓣.tensoratorEquiv cX cY) ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) x) = + (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h'')) + ((𝓣.tensoratorEquiv cW cZ) x) := by + trans ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ + (𝓣.tensoratorEquiv cX cY)) x + rfl + rw [tensoratorEquiv_mapIso] + rfl + exact e + exact h + +lemma tensoratorEquiv_mapIso_tmul (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X) + (h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'') + (x : 𝓣.Tensor cW) (y : 𝓣.Tensor cZ) : + (𝓣.tensoratorEquiv cX cY) ((𝓣.mapIso e'' h'' x) ⊗ₜ[R] (𝓣.mapIso e' h' y)) = + (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h'')) + ((𝓣.tensoratorEquiv cW cZ) (x ⊗ₜ y)) := by + rw [← tensoratorEquiv_mapIso_apply] + rfl + exact e + exact h + +/-! + +## Splitting tensors into tensor products + +-/ + +/-- The decomposition of a set into a direct sum based on the image of an injection. -/ +def decompEmbedSet (f : Y ↪ X) : + X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Y := + (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <| + (Equiv.sumComm _ _).trans <| + Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <| + (Function.Embedding.toEquivRange f).symm + +/-- The restriction of a map from an indexing set to the space to the complement of the image + of an embedding. -/ +def decompEmbedColorLeft (c : X → 𝓣.Color) (f : Y ↪ X) : + {x // x ∈ (Finset.image f Finset.univ)ᶜ} → 𝓣.Color := + (c ∘ (decompEmbedSet f).symm) ∘ Sum.inl + +/-- The restriction of a map from an indexing set to the space to the image + of an embedding. -/ +def decompEmbedColorRight (c : X → 𝓣.Color) (f : Y ↪ X) : Y → 𝓣.Color := + (c ∘ (decompEmbedSet f).symm) ∘ Sum.inr + +lemma decompEmbed_cond (c : X → 𝓣.Color) (f : Y ↪ X) : c = + (Sum.elim (𝓣.decompEmbedColorLeft c f) (𝓣.decompEmbedColorRight c f)) ∘ decompEmbedSet f := by + simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl + +/-- Decomposes a tensor into a tensor product of two tensors + one which has indices in the image of the given embedding, and the other has indices in + the complement of that image. -/ +def decompEmbed (f : Y ↪ X) : + 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.decompEmbedColorLeft cX f) ⊗[R] 𝓣.Tensor (cX ∘ f) := + (𝓣.mapIso (decompEmbedSet f) (𝓣.decompEmbed_cond cX f)) ≪≫ₗ + (𝓣.tensoratorEquiv (𝓣.decompEmbedColorLeft cX f) (𝓣.decompEmbedColorRight cX f)).symm + +/-! + +## Contraction + +-/ + +/-- 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] + ⨂[R] x, 𝓣.ColorModule (cX x) ⊗[R] 𝓣.ColorModule (cX2 x) := + TensorProduct.lift ( + PiTensorProduct.map₂ (fun x => + TensorProduct.mk R (𝓣.ColorModule (cX x)) (𝓣.ColorModule (cX2 x)))) + +lemma mkPiAlgebra_equiv (e : X ≃ Y) : + (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) = + (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R Y R)) ∘ₗ + (PiTensorProduct.reindex R _ e).toLinearMap := by + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro x + simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.lift.tprod, + MultilinearMap.mkPiAlgebra_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + PiTensorProduct.reindex_tprod, Equiv.prod_comp] + +/-- Given a tensor in `𝓣.Tensor cX` and a tensor in `𝓣.Tensor (𝓣.τ ∘ cX)`, the element of + `R` formed by contracting all of their indices. -/ +def contrAll' : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor (𝓣.τ ∘ cX) →ₗ[R] R := + (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) ∘ₗ + (PiTensorProduct.map (fun x => 𝓣.contrDual (cX x))) ∘ₗ + (𝓣.pairProd) + +lemma contrAll'_mapIso_cond {e : X ≃ Y} (h : cX = cY ∘ e) : + 𝓣.τ ∘ cY = (𝓣.τ ∘ cX) ∘ ⇑e.symm := by + subst h + exact (Equiv.eq_comp_symm e (𝓣.τ ∘ cY) (𝓣.τ ∘ cY ∘ ⇑e)).mpr rfl + +@[simp] +lemma contrAll'_mapIso (e : X ≃ Y) (h : c = cY ∘ e) : + 𝓣.contrAll' ∘ₗ + (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap = + 𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl R _) + (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h))).toLinearMap := 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'] + rw [mkPiAlgebra_equiv e] + apply congrArg + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] + apply congrArg + rw [← LinearEquiv.symm_apply_eq] + rw [PiTensorProduct.reindex_symm] + rw [← PiTensorProduct.map_reindex] + subst h + simp only [Equiv.symm_symm_apply, Function.comp_apply] + apply congrArg + rw [pairProd, pairProd] + simp only [Function.comp_apply, lift.tmul, LinearMapClass.map_smul, LinearMap.smul_apply] + apply congrArg + change _ = ((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (cY (e x))) + (𝓣.ColorModule (𝓣.τ (cY (e x))))) + ((PiTensorProduct.tprod R) fx)) + ((𝓣.mapIso e.symm _) ((PiTensorProduct.tprod R) fy)) + rw [mapIso_tprod] + simp only [Equiv.symm_symm_apply, Function.comp_apply] + rw [PiTensorProduct.map₂_tprod_tprod] + change PiTensorProduct.reindex R _ e.symm + ((PiTensorProduct.map₂ _ + ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (fx (e.symm i)))) + ((PiTensorProduct.tprod R) fy)) = _ + rw [PiTensorProduct.map₂_tprod_tprod] + simp only [Equiv.symm_symm_apply, Function.comp_apply, mk_apply] + erw [PiTensorProduct.reindex_tprod] + apply congrArg + funext i + simp only [Equiv.symm_symm_apply] + congr + simp [colorModuleCast] + apply cast_eq_iff_heq.mpr + rw [Equiv.symm_apply_apply] + +@[simp] +lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : c = cY ∘ e) (x : 𝓣.Tensor c) + (y : 𝓣.Tensor (𝓣.τ ∘ cY)) : 𝓣.contrAll' ((𝓣.mapIso e h) x ⊗ₜ[R] y) = + 𝓣.contrAll' (x ⊗ₜ[R] (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h) y)) := by + change (𝓣.contrAll' ∘ₗ + (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap) (x ⊗ₜ[R] y) = _ + rw [contrAll'_mapIso] + rfl + +/-- The contraction of all the indices of two tensors with dual colors. -/ +def contrAll {c : X → 𝓣.Color} {d : Y → 𝓣.Color} + (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) : 𝓣.Tensor c ⊗[R] 𝓣.Tensor d →ₗ[R] R := + 𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _) + (𝓣.mapIso e.symm (by subst h; funext a; simp; rw [𝓣.τ_involutive]))).toLinearMap + +lemma contrAll_symm_cond {e : X ≃ Y} (h : c = 𝓣.τ ∘ cY ∘ e) : + cY = 𝓣.τ ∘ c ∘ ⇑e.symm := by + subst h + ext1 x + simp only [Function.comp_apply, Equiv.apply_symm_apply] + rw [𝓣.τ_involutive] + +lemma contrAll_mapIso_right_cond {e : X ≃ Y} {e' : Z ≃ Y} + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : c = 𝓣.τ ∘ cZ ∘ ⇑(e.trans e'.symm) := by + subst h h' + ext1 x + simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply] + +@[simp] +lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y) + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) : + 𝓣.contrAll e h (x ⊗ₜ[R] 𝓣.mapIso e' h' z) = + 𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') (x ⊗ₜ[R] z) := by + rw [contrAll, contrAll] + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul, + LinearEquiv.refl_apply, mapIso_mapIso] + congr + +@[simp] +lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y) + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : 𝓣.contrAll e h ∘ₗ + (TensorProduct.congr (LinearEquiv.refl R (𝓣.Tensor c)) (𝓣.mapIso e' h')).toLinearMap + = 𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') := by + apply TensorProduct.ext' + intro x y + exact 𝓣.contrAll_mapIso_right_tmul e e' h h' x y + +lemma contrAll_mapIso_left_cond {e : X ≃ Y} {e' : Z ≃ X} + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') : cZ = 𝓣.τ ∘ cY ∘ ⇑(e'.trans e) := by + subst h h' + ext1 x + simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply] + +@[simp] +lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X} + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) : + 𝓣.contrAll e h (𝓣.mapIso e' h' x ⊗ₜ[R] y) = + 𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') (x ⊗ₜ[R] y) := by + rw [contrAll, contrAll] + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul, + LinearEquiv.refl_apply, contrAll'_mapIso_tmul, mapIso_mapIso] + congr + +@[simp] +lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X} + (h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') : + 𝓣.contrAll e h ∘ₗ + (TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor cY))).toLinearMap + = 𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') := by + apply TensorProduct.ext' + intro x y + exact 𝓣.contrAll_mapIso_left_tmul h h' x y + +end PreTensorStructure + +/-! TODO: Add unit here. -/ +/-- A `PreTensorStructure` with the additional constraint that `contrDua` is symmetric. -/ +structure TensorStructure (R : Type) [CommSemiring R] extends PreTensorStructure R where + /-- The symmetry condition on `contrDua`. -/ + contrDual_symm : ∀ μ, + (contrDual μ) ∘ₗ (TensorProduct.comm R (ColorModule (τ μ)) (ColorModule μ)).toLinearMap = + (contrDual (τ μ)) ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _) + (toPreTensorStructure.colorModuleCast (by rw[toPreTensorStructure.τ_involutive]))).toLinearMap + +namespace TensorStructure + +open PreTensorStructure + +variable (𝓣 : TensorStructure R) + +variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] + [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] + {c c₂ : X → 𝓣.Color} {d : Y → 𝓣.Color} {b : Z → 𝓣.Color} {d' : Y' → 𝓣.Color} {μ ν: 𝓣.Color} + +end TensorStructure + +/-- A `TensorStructure` with a group action. -/ +structure GroupTensorStructure (R : Type) [CommSemiring R] + (G : Type) [Group G] extends TensorStructure R where + /-- For each color `μ` a representation of `G` on `ColorModule μ`. -/ + repColorModule : (μ : Color) → Representation R G (ColorModule μ) + /-- 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 μ + +namespace GroupTensorStructure +open TensorStructure +open PreTensorStructure + +variable {G : Type} [Group G] + +variable (𝓣 : GroupTensorStructure R G) + +variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] + [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] + {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color} + +/-- The representation of the group `G` on the vector space of tensors. -/ +def rep : Representation R G (𝓣.Tensor cX) where + toFun g := PiTensorProduct.map (fun x => 𝓣.repColorModule (cX x) g) + map_one' := by + simp_all only [_root_.map_one, PiTensorProduct.map_one] + map_mul' g g' := by + simp_all only [_root_.map_mul] + exact PiTensorProduct.map_mul _ _ + +local infixl:78 " • " => 𝓣.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] +lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) : + (𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap = (𝓣.mapIso e h).toLinearMap ∘ₗ 𝓣.rep g := by + apply PiTensorProduct.ext + apply MultilinearMap.ext + intro x + simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply] + erw [mapIso_tprod] + simp [rep, repColorModule_colorModuleCast_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)) + rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod] + rw [mapIso_tprod] + apply congrArg + funext i + subst h + simp [repColorModule_colorModuleCast_apply] + +@[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 + trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x + rfl + simp + +@[simp] +lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) : + g • (PiTensorProduct.tprod R f) = PiTensorProduct.tprod R (fun x => + 𝓣.repColorModule (cX x) g (f x)) := by + simp [rep] + change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) f) = _ + rw [PiTensorProduct.map_tprod] + +/-! + +## Group acting on tensor products + +-/ + +lemma rep_tensoratorEquiv (g : G) : + (𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.rep g ∘ₗ + (𝓣.tensoratorEquiv cX cY).toLinearMap := by + apply tensorProd_piTensorProd_ext + intro p q + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_tmul, rep_tprod, + tensoratorEquiv_tmul_tprod] + apply congrArg + funext x + match x with + | Sum.inl x => rfl + | Sum.inr x => rfl + +lemma rep_tensoratorEquiv_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] + 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] + rfl + +/-! + +## 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] + rfl + +end GroupTensorStructure + +end diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean deleted file mode 100644 index 751335e..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ /dev/null @@ -1,661 +0,0 @@ -/- -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 Mathlib.Logic.Function.CompTypeclasses -import Mathlib.Data.Real.Basic -import Mathlib.Data.Fintype.BigOperators -import Mathlib.Logic.Equiv.Fin -import Mathlib.Tactic.FinCases -import Mathlib.Logic.Equiv.Fintype -/-! - -# Real Lorentz Tensors - -In this file we define real Lorentz tensors. - -We implicitly follow the definition of a modular operad. -This will relation should be made explicit in the future. - -## References - --- For modular operads see: [Raynor][raynor2021graphical] - --/ -/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/ -/-! TODO: Generalize to maps into Lorentz tensors. -/ - -/-- The possible `colors` of an index for a RealLorentzTensor. - There are two possiblities, `up` and `down`. -/ -inductive RealLorentzTensor.Colors where - | up : RealLorentzTensor.Colors - | down : RealLorentzTensor.Colors - -/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/ -def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type := - match μ with - | RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d - | RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d - -instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) := - match μ with - | 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). -/ -def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : - Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x) - -/-- A Lorentz Tensor defined by its coordinate map. -/ -structure RealLorentzTensor (d : ℕ) (X : Type) where - /-- The color associated to each index of the tensor. -/ - color : X → RealLorentzTensor.Colors - /-- The coordinate map for the tensor. -/ - coord : RealLorentzTensor.IndexValue d color → ℝ - -namespace RealLorentzTensor -open Matrix -universe u1 -variable {d : ℕ} {X Y Z : Type} (c : X → Colors) - -/-! - -## Colors - --/ - -/-- The involution acting on colors. -/ -def τ : Colors → Colors - | Colors.up => Colors.down - | Colors.down => Colors.up - -/-- The map τ is an involution. -/ -@[simp] -lemma τ_involutive : Function.Involutive τ := by - intro x - cases x <;> rfl - -lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ := - (Function.Involutive.eq_iff τ_involutive).mp h.symm - -/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/ -def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x - -/-- An equivalence of `ColorsIndex` types given an equality of colors. -/ -def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) : - ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ := - Equiv.cast (congrArg (ColorsIndex d) h) - -/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/ -def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}: - ColorsIndex d μ ≃ ColorsIndex d (τ μ) where - toFun x := - match μ with - | RealLorentzTensor.Colors.up => x - | RealLorentzTensor.Colors.down => x - invFun x := - match μ with - | RealLorentzTensor.Colors.up => x - | RealLorentzTensor.Colors.down => x - left_inv x := by cases μ <;> rfl - right_inv x := by cases μ <;> rfl - -/-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/ -def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) : - ColorsIndex d μ ≃ ColorsIndex d ν := - (colorsIndexCast h).trans colorsIndexDualCastSelf.symm - -lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) : - (colorsIndexDualCast h).symm = - @colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by - match μ, ν with - | Colors.up, Colors.down => rfl - | Colors.down, Colors.up => rfl - -/-! - -## Index values - --/ - -instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype - -instance [Fintype X] : DecidableEq (IndexValue d c) := - Fintype.decidablePiFintype - -/-! - -## Induced isomorphisms between IndexValue sets - --/ - -/-- An isomorphism of the type of index values given an isomorphism of sets. -/ -@[simps!] -def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) : - IndexValue d i ≃ IndexValue d j := - (Equiv.piCongrRight (fun μ => colorsIndexCast (congrFun h μ))).trans $ - Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f - -lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} - (h : i = j ∘ f) (y : IndexValue d j) (x : X) : - (indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by - rfl - -@[simp] -lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors} - {j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) : - (indexValueIso d f h).trans (indexValueIso d g h') = - indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by - have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm = - (indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by - subst h' h - exact Equiv.coe_inj.mp rfl - simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1 - -lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : - (indexValueIso d f h).symm = - indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h))) := by - ext i : 1 - rw [← Equiv.symm_apply_eq] - funext y - rw [indexValueIso_symm_apply', indexValueIso_symm_apply'] - simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast] - apply cast_eq_iff_heq.mpr - rw [Equiv.apply_symm_apply] - -lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : - indexValueIso d f h = - (indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h)))).symm := by - rw [indexValueIso_symm] - rfl - -@[simp] -lemma indexValueIso_refl (d : ℕ) (i : X → Colors) : - indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by - rfl - -/-! - -## 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 - --/ - -lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color) - (h' : T₁.coord = fun i => T₂.coord (indexValueIso d (Equiv.refl X) h i)) : - T₁ = T₂ := by - cases T₁ - cases T₂ - simp_all only [IndexValue, mk.injEq] - apply And.intro h - simp only at h - subst h - simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h' - rfl - -/-! - -## Mapping isomorphisms. - --/ - -/-- An equivalence of Tensors given an equivalence of underlying sets. -/ -@[simps!] -def mapIso (d : ℕ) (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where - toFun T := { - color := T.color ∘ f.symm, - coord := T.coord ∘ (indexValueIso d f (by simp : T.color = T.color ∘ f.symm ∘ f)).symm} - invFun T := { - color := T.color ∘ f, - coord := T.coord ∘ (indexValueIso d f.symm (by simp : T.color = T.color ∘ f ∘ f.symm)).symm} - left_inv T := by - refine ext ?_ ?_ - · simp [Function.comp.assoc] - · funext i - simp only [IndexValue, Function.comp_apply, Function.comp_id] - apply congrArg - funext x - erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm, - indexValueIso_symm_apply'] - rw [← Equiv.apply_eq_iff_eq_symm_apply] - simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast, - Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply] - apply cast_eq_iff_heq.mpr - congr - exact Equiv.symm_apply_apply f x - right_inv T := by - refine ext ?_ ?_ - · simp [Function.comp.assoc] - · funext i - simp only [IndexValue, Function.comp_apply, Function.comp_id] - apply congrArg - funext x - erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm, - indexValueIso_symm_apply'] - rw [← Equiv.apply_eq_iff_eq_symm_apply] - simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast, - Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply] - apply cast_eq_iff_heq.mpr - congr - exact Equiv.apply_symm_apply f x - -@[simp] -lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) : - (mapIso d f).trans (mapIso d g) = mapIso d (f.trans g) := by - refine Equiv.coe_inj.mp ?_ - funext T - refine ext rfl ?_ - simp only [Equiv.trans_apply, IndexValue, mapIso_apply_color, Equiv.symm_trans_apply, - indexValueIso_refl, Equiv.refl_apply, mapIso_apply_coord] - funext i - rw [mapIso_apply_coord, mapIso_apply_coord] - apply congrArg - rw [← indexValueIso_trans] - rfl - exact (Equiv.comp_symm_eq f (T.color ∘ ⇑f.symm) T.color).mp rfl - -lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := rfl - -lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl - -/-! - -## Sums - --/ - -/-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/ -def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} : - IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where - toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x)) - invFun p := fun c => match c with - | Sum.inl x => (p.1 x) - | Sum.inr x => (p.2 x) - left_inv i := by - simp only [IndexValue] - ext1 x - cases x with - | inl val => rfl - | inr val_1 => rfl - right_inv p := rfl - -/-- An equivalence between index values formed by commuting sums. -/ -def indexValueSumComm {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) : - IndexValue d (Sum.elim Tc Sc) ≃ IndexValue d (Sum.elim Sc Tc) := - indexValueIso d (Equiv.sumComm X Y) (by aesop) - -/-! - -## Marked Lorentz tensors - -To define contraction and multiplication of Lorentz tensors we need to mark indices. - --/ - -/-- A `RealLorentzTensor` with `n` marked indices. -/ -def Marked (d : ℕ) (X : Type) (n : ℕ) : Type := - RealLorentzTensor d (X ⊕ Fin n) - -namespace Marked - -variable {n m : ℕ} - -/-- The marked point. -/ -def markedPoint (X : Type) (i : Fin n) : (X ⊕ Fin n) := - Sum.inr i - -/-- The colors of unmarked indices. -/ -def unmarkedColor (T : Marked d X n) : X → Colors := - T.color ∘ Sum.inl - -/-- The colors of marked indices. -/ -def markedColor (T : Marked d X n) : Fin n → Colors := - T.color ∘ Sum.inr - -/-- The index values restricted to unmarked indices. -/ -def UnmarkedIndexValue (T : Marked d X n) : Type := - IndexValue d T.unmarkedColor - -instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue := - Pi.fintype - -instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue := - Fintype.decidablePiFintype - -/-- The index values restricted to marked indices. -/ -def MarkedIndexValue (T : Marked d X n) : Type := - IndexValue d T.markedColor - -instance (T : Marked d X n) : Fintype T.MarkedIndexValue := - Pi.fintype - -instance (T : Marked d X n) : DecidableEq T.MarkedIndexValue := - Fintype.decidablePiFintype - -lemma color_eq_elim (T : Marked d X n) : - T.color = Sum.elim T.unmarkedColor T.markedColor := by - ext1 x - cases' x <;> rfl - -/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/ -def splitIndexValue {T : Marked d X n} : - IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue := - (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans - indexValueSumEquiv - -@[simp] -lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X] - (P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) : - ∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by - rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type] - -/-- Construction of marked index values for the case of 1 marked index. -/ -def oneMarkedIndexValue {T : Marked d X 1} : - ColorsIndex d (T.color (markedPoint X 0)) ≃ T.MarkedIndexValue where - toFun x := fun i => match i with - | 0 => x - invFun i := i 0 - left_inv x := rfl - right_inv i := by - funext x - fin_cases x - rfl - -/-- Construction of marked index values for the case of 2 marked index. -/ -def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0))) - (y : ColorsIndex d <| T.color <| markedPoint X 1) : - T.MarkedIndexValue := fun i => - match i with - | 0 => x - | 1 => y - -/-- An equivalence of types used to turn the first marked index into an unmarked index. -/ -def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) ⊕ Fin n := - trans (Equiv.sumCongr (Equiv.refl _) - (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm))) - (Equiv.sumAssoc _ _ _).symm - -/-- Unmark the first marked index of a marked tensor. -/ -def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n := - mapIso d (unmarkFirstSet X n) - -/-! - -## Marking elements. - --/ -section markingElements - -variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] - -/-- Splits a type based on an embedding from `Fin n` into elements not in the image of the - embedding, and elements in the image. -/ -def markEmbeddingSet {n : ℕ} (f : Fin n ↪ X) : - X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Fin n := - (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <| - (Equiv.sumComm _ _).trans <| - Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <| - (Function.Embedding.toEquivRange f).symm - -lemma markEmbeddingSet_on_mem {n : ℕ} (f : Fin n ↪ X) (x : X) - (hx : x ∈ Finset.image f Finset.univ) : markEmbeddingSet f x = - Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩) := by - rw [markEmbeddingSet] - simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply] - rw [Equiv.Set.sumCompl_symm_apply_of_mem] - rfl - -lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X) - (hx : ¬ x ∈ (Finset.image f Finset.univ)) : markEmbeddingSet f x = - Sum.inl ⟨x, by simpa using hx⟩ := by - rw [markEmbeddingSet] - simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply] - rw [Equiv.Set.sumCompl_symm_apply_of_not_mem] - rfl - simpa using hx - -/-- Marks the indices of tensor in the image of an embedding. -/ -@[simps!] -def markEmbedding {n : ℕ} (f : Fin n ↪ X) : - RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n := - mapIso d (markEmbeddingSet f) - -lemma markEmbeddingSet_on_mem_indexValue_apply {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) - (i : IndexValue d (markEmbedding f T).color) (x : X) (hx : x ∈ (Finset.image f Finset.univ)) : - i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color - (markEmbeddingSet_on_mem f x hx).symm) - (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by - simp [colorsIndexCast] - symm - apply cast_eq_iff_heq.mpr - rw [markEmbeddingSet_on_mem f x hx] - -lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ} - (f : Fin n ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) - (x : X) (hx : ¬ x ∈ (Finset.image f Finset.univ)) : - i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color - (markEmbeddingSet_on_not_mem f x hx).symm) (i (Sum.inl ⟨x, by simpa using hx⟩)) := by - simp [colorsIndexCast] - symm - apply cast_eq_iff_heq.mpr - rw [markEmbeddingSet_on_not_mem f x hx] - -/-- An equivalence between the IndexValues for a tensor `T` and the corresponding - tensor with indices maked by an embedding. -/ -@[simps!] -def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) : - IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color := - indexValueIso d (markEmbeddingSet f) ( - (Equiv.comp_symm_eq (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) - -lemma markEmbeddingIndexValue_apply_symm_on_mem {n : ℕ} - (f : Fin n.succ ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) - (x : X) (hx : x ∈ (Finset.image f Finset.univ)) : - (markEmbeddingIndexValue f T).symm i x = (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq - (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans - (congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_mem f x hx)))).symm - (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by - rw [markEmbeddingIndexValue, indexValueIso_symm_apply'] - rw [markEmbeddingSet_on_mem_indexValue_apply f T i x hx] - simp [colorsIndexCast] - -lemma markEmbeddingIndexValue_apply_symm_on_not_mem {n : ℕ} (f : Fin n.succ ↪ X) - (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) (x : X) - (hx : ¬ x ∈ (Finset.image f Finset.univ)) : (markEmbeddingIndexValue f T).symm i x = - (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq - (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans - ((congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_not_mem f x hx))))).symm - (i (Sum.inl ⟨x, by simpa using hx⟩)) := by - rw [markEmbeddingIndexValue, indexValueIso_symm_apply'] - rw [markEmbeddingSet_on_not_mem_indexValue_apply f T i x hx] - simp only [Nat.succ_eq_add_one, Function.comp_apply, markEmbedding_apply_color, colorsIndexCast, - Equiv.cast_symm, id_eq, eq_mp_eq_cast, eq_mpr_eq_cast, Equiv.cast_apply, cast_cast, cast_eq, - Equiv.cast_refl, Equiv.refl_symm] - rfl - -/-- Given an equivalence of types, an embedding `f` to an embedding `g`, the equivalence - taking the complement of the image of `f` to the complement of the image of `g`. -/ -@[simps!] -def equivEmbedCompl (e : X ≃ Y) {f : Fin n ↪ X} {g : Fin n ↪ Y} (he : f.trans e = g) : - {x // x ∈ (Finset.image f Finset.univ)ᶜ} ≃ {y // y ∈ (Finset.image g Finset.univ)ᶜ} := - (Equiv.subtypeEquivOfSubtype' e).trans <| - (Equiv.subtypeEquivRight (fun x => by simp [← he, Equiv.eq_symm_apply])) - -lemma markEmbedding_mapIso_right (e : X ≃ Y) (f : Fin n ↪ X) (g : Fin n ↪ Y) (he : f.trans e = g) - (T : RealLorentzTensor d X) : markEmbedding g (mapIso d e T) = - mapIso d (Equiv.sumCongr (equivEmbedCompl e he) (Equiv.refl (Fin n))) (markEmbedding f T) := by - rw [markEmbedding, markEmbedding] - erw [← Equiv.trans_apply, ← Equiv.trans_apply] - rw [mapIso_trans, mapIso_trans] - apply congrFun - repeat apply congrArg - refine Equiv.ext (fun x => ?_) - simp only [Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl] - by_cases hx : x ∈ Finset.image f Finset.univ - · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g (e x) (by simpa [← he] using hx)] - subst he - simp only [Sum.map_inr, id_eq, Sum.inr.injEq, Equiv.symm_apply_eq, - Function.Embedding.toEquivRange_apply, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, - Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] - change x = f.toEquivRange _ - rw [Equiv.apply_symm_apply] - · rw [markEmbeddingSet_on_not_mem f x hx, - markEmbeddingSet_on_not_mem g (e x) (by simpa [← he] using hx)] - subst he - rfl - -lemma markEmbedding_mapIso_left {n m : ℕ} (e : Fin n ≃ Fin m) (f : Fin n ↪ X) (g : Fin m ↪ X) - (he : e.symm.toEmbedding.trans f = g) (T : RealLorentzTensor d X) : - markEmbedding g T = mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by - simpa [← he] using Equiv.forall_congr_left e)) e) (markEmbedding f T) := by - rw [markEmbedding, markEmbedding] - erw [← Equiv.trans_apply] - rw [mapIso_trans] - apply congrFun - repeat apply congrArg - refine Equiv.ext (fun x => ?_) - simp only [Equiv.trans_apply, Equiv.sumCongr_apply] - by_cases hx : x ∈ Finset.image f Finset.univ - · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g x (by - simp [← he, hx] - obtain ⟨y, _, hy2⟩ := Finset.mem_image.mp hx - use e y - simpa using hy2)] - subst he - simp [Equiv.symm_apply_eq] - change x = f.toEquivRange _ - rw [Equiv.apply_symm_apply] - · rw [markEmbeddingSet_on_not_mem f x hx, markEmbeddingSet_on_not_mem g x (by - simpa [← he, hx] using fun x => not_exists.mp (Finset.mem_image.mpr.mt hx) (e.symm x))] - subst he - rfl - -/-! - -## Marking a single element - --/ - -/-- An embedding from `Fin 1` into `X` given an element `x ∈ X`. -/ -@[simps!] -def embedSingleton (x : X) : Fin 1 ↪ X := - ⟨![x], fun x y => by fin_cases x; fin_cases y; simp⟩ - -lemma embedSingleton_toEquivRange_symm (x : X) : - (embedSingleton x).toEquivRange.symm ⟨x, by simp⟩ = 0 := by - exact Fin.fin_one_eq_zero _ - -/-- Equivalence, taking a tensor to a tensor with a single marked index. -/ -@[simps!] -def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 := - (markEmbedding (embedSingleton x)).trans - (mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _))) - -/-- Equivalence between index values of a tensor and the corresponding tensor with a single - marked index. -/ -@[simps!] -def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) : - IndexValue d T.color ≃ IndexValue d (markSingle x T).color := - (markEmbeddingIndexValue (embedSingleton x) T).trans <| - indexValueIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)) - (by funext x_1; simp) - -/-- Given an equivalence of types, taking `x` to `y` the corresponding equivalence of - subtypes of elements not equal to `x` and not equal to `y` respectively. -/ -@[simps!] -def equivSingleCompl (e : X ≃ Y) {x : X} {y : Y} (he : e x = y) : - {x' // x' ≠ x} ≃ {y' // y' ≠ y} := - (Equiv.subtypeEquivOfSubtype' e).trans <| - Equiv.subtypeEquivRight (fun a => by simp [Equiv.symm_apply_eq, he]) - -lemma markSingle_mapIso (e : X ≃ Y) (x : X) (y : Y) (he : e x = y) - (T : RealLorentzTensor d X) : markSingle y (mapIso d e T) = - mapIso d (Equiv.sumCongr (equivSingleCompl e he) (Equiv.refl _)) (markSingle x T) := by - rw [markSingle, Equiv.trans_apply] - rw [markEmbedding_mapIso_right e (embedSingleton x) (embedSingleton y) - (Function.Embedding.ext_iff.mp (fun a => by simpa using he)), markSingle, markEmbedding] - erw [← Equiv.trans_apply, ← Equiv.trans_apply, ← Equiv.trans_apply] - rw [mapIso_trans, mapIso_trans, mapIso_trans, mapIso_trans] - apply congrFun - repeat apply congrArg - refine Equiv.ext fun x => ?_ - simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.sumCongr_trans, - Equiv.trans_refl, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.coe_refl, - Sum.map_map, CompTriple.comp_eq] - subst he - rfl - -/-! - -## Marking two elements - --/ - -/-- An embedding from `Fin 2` given two inequivalent elements. -/ -@[simps!] -def embedDoubleton (x y : X) (h : x ≠ y) : Fin 2 ↪ X := - ⟨![x, y], fun a b => by - fin_cases a <;> fin_cases b <;> simp [h] - exact h.symm⟩ - -end markingElements - -end Marked - -/-! - -## Contraction of indices - --/ - -open Marked - -/-- The contraction of the marked indices in a tensor with two marked indices. -/ -def contr {X : Type} (T : Marked d X 2) (h : T.markedColor 0 = τ (T.markedColor 1)) : - RealLorentzTensor d X where - color := T.unmarkedColor - coord := fun i => - ∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ colorsIndexDualCast h x)) - -/-! TODO: Following the ethos of modular operads, prove properties of contraction. -/ - -/-! TODO: Use `contr` to generalize to any pair of marked index. -/ - -/-! - -## Rising and lowering indices - -Rising or lowering an index corresponds to changing the color of that index. - --/ - -/-! TODO: Define the rising and lowering of indices using contraction with the metric. -/ - -/-! - -## Graphical species and Lorentz tensors - --/ - -/-! TODO: From Lorentz tensors graphical species. -/ -/-! TODO: Show that the action of the Lorentz group defines an action on the graphical species. -/ - -end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean deleted file mode 100644 index acd45d4..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean +++ /dev/null @@ -1,401 +0,0 @@ -/- -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.Basic -import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction -import HepLean.SpaceTime.LorentzTensor.Real.Multiplication -/-! - -# Constructors for real Lorentz tensors - -In this file we will constructors of real Lorentz tensors from real numbers, -vectors and matrices. - -We will derive properties of these constructors. - --/ - -namespace RealLorentzTensor -/-! - -# Tensors from and to the reals - -An important point that we shall see here is that there is a well defined map -to the real numbers, i.e. which is invariant under transformations of mapIso. - --/ - -/-- An equivalence from Real tensors on an empty set to `ℝ`. -/ -@[simps!] -def toReal (d : ℕ) {X : Type} (h : IsEmpty X) : RealLorentzTensor d X ≃ ℝ where - toFun := fun T => T.coord (IsEmpty.elim h) - invFun := fun r => { - color := fun x => IsEmpty.elim h x, - coord := fun _ => r} - left_inv T := by - refine ext ?_ ?_ - funext x - exact IsEmpty.elim h x - funext a - change T.coord (IsEmpty.elim h) = _ - apply congrArg - funext x - exact IsEmpty.elim h x - right_inv x := rfl - -/-- The real number obtained from a tensor is invariant under `mapIso`. -/ -lemma toReal_mapIso (d : ℕ) {X Y : Type} (h : IsEmpty X) (f : X ≃ Y) : - (mapIso d f).trans (toReal d (Equiv.isEmpty f.symm)) = toReal d h := by - apply Equiv.ext - intro x - simp only [Equiv.trans_apply, toReal_apply, mapIso_apply_color, mapIso_apply_coord] - apply congrArg - funext x - exact IsEmpty.elim h x - -/-! - -# Tensors from reals, vectors and matrices - -Note that that these definitions are not equivariant with respect to an -action of the Lorentz group. They are provided for constructive purposes. - --/ - -/-- A marked 1-tensor with a single up index constructed from a vector. - - Note: This is not the same as rising indices on `ofVecDown`. -/ -def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) : - Marked d Empty 1 where - color := fun _ => Colors.up - coord := fun i => v <| i <| Sum.inr <| 0 - -/-- A marked 1-tensor with a single down index constructed from a vector. - - Note: This is not the same as lowering indices on `ofVecUp`. -/ -def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) : - Marked d Empty 1 where - color := fun _ => Colors.down - coord := fun i => v <| i <| Sum.inr <| 0 - -/-- A tensor with two up indices constructed from a matrix. - -Note: This is not the same as rising or lowering indices on other `ofMat...`. -/ -def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Marked d Empty 2 where - color := fun _ => Colors.up - coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1)) - -/-- A tensor with two down indices constructed from a matrix. - -Note: This is not the same as rising or lowering indices on other `ofMat...`. -/ -def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Marked d Empty 2 where - color := fun _ => Colors.down - coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1)) - -/-- A marked 2-tensor with the first index up and the second index down. - -Note: This is not the same as rising or lowering indices on other `ofMat...`. -/ -@[simps!] -def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Marked d Empty 2 where - color := fun i => match i with - | Sum.inr 0 => Colors.up - | Sum.inr 1 => Colors.down - coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1)) - -/-- A marked 2-tensor with the first index down and the second index up. - -Note: This is not the same as rising or lowering indices on other `ofMat...`. -/ -def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Marked d Empty 2 where - color := fun i => match i with - | Sum.inr 0 => Colors.down - | Sum.inr 1 => Colors.up - coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1)) - -/-! - -## Equivalence of `IndexValue` for constructors - --/ - -/-- Index values for `ofVecUp v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/ -def ofVecUpIndexValue (v : Fin 1 ⊕ Fin d → ℝ) : - IndexValue d (ofVecUp v).color ≃ (Fin 1 ⊕ Fin d) where - toFun i := i (Sum.inr 0) - invFun x := fun i => match i with - | Sum.inr 0 => x - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - right_inv x := rfl - -/-- Index values for `ofVecDown v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/ -def ofVecDownIndexValue (v : Fin 1 ⊕ Fin d → ℝ) : - IndexValue d (ofVecDown v).color ≃ (Fin 1 ⊕ Fin d) where - toFun i := i (Sum.inr 0) - invFun x := fun i => match i with - | Sum.inr 0 => x - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - right_inv x := rfl - -/-- Index values for `ofMatUpUp v` are equivalent to elements of - `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/ -def ofMatUpUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - IndexValue d (ofMatUpUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where - toFun i := (i (Sum.inr 0), i (Sum.inr 1)) - invFun x := fun i => match i with - | Sum.inr 0 => x.1 - | Sum.inr 1 => x.2 - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - | Sum.inr 1 => rfl - right_inv x := rfl - -/-- Index values for `ofMatDownDown v` are equivalent to elements of - `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/ -def ofMatDownDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - IndexValue d (ofMatDownDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where - toFun i := (i (Sum.inr 0), i (Sum.inr 1)) - invFun x := fun i => match i with - | Sum.inr 0 => x.1 - | Sum.inr 1 => x.2 - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - | Sum.inr 1 => rfl - right_inv x := rfl - -/-- Index values for `ofMatUpDown v` are equivalent to elements of - `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/ -def ofMatUpDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - IndexValue d (ofMatUpDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where - toFun i := (i (Sum.inr 0), i (Sum.inr 1)) - invFun x := fun i => match i with - | Sum.inr 0 => x.1 - | Sum.inr 1 => x.2 - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - | Sum.inr 1 => rfl - right_inv x := rfl - -/-- Index values for `ofMatDownUp v` are equivalent to elements of - `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/ -def ofMatDownUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - IndexValue d (ofMatDownUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where - toFun i := (i (Sum.inr 0), i (Sum.inr 1)) - invFun x := fun i => match i with - | Sum.inr 0 => x.1 - | Sum.inr 1 => x.2 - left_inv i := by - funext y - match y with - | Sum.inr 0 => rfl - | Sum.inr 1 => rfl - right_inv x := rfl - -/-! - -## Contraction of indices of tensors from matrices - --/ -open Matrix -open Marked - -/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/ -lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - contr (ofMatUpDown M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by - refine ext ?_ rfl - · funext i - exact Empty.elim i - -/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/ -lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - contr (ofMatDownUp M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by - refine ext ?_ rfl - · funext i - exact Empty.elim i - -/-! - -## Multiplication of tensors from vectors and matrices - --/ - -/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/ -@[simp] -lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) : - mul (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by - refine ext ?_ rfl - · funext i - exact IsEmpty.elim instIsEmptySum i - -/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/ -@[simp] -lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) : - mul (ofVecDown v₁) (ofVecUp v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by - refine ext ?_ rfl - · funext i - exact IsEmpty.elim instIsEmptySum i - -lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) - (v : Fin 1 ⊕ Fin d → ℝ) : - mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)) - (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by - refine ext ?_ rfl - · funext i - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm] - fin_cases i - rfl - -lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) - (v : Fin 1 ⊕ Fin d → ℝ) : - mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty) - (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by - refine ext ?_ rfl - · funext i - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm] - fin_cases i - rfl - -/-! - -## The Lorentz action on constructors - --/ -section lorentzAction -variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors) -variable (Λ Λ' : LorentzGroup d) - -open Matrix - -/-- The action of the Lorentz group on `ofReal v` is trivial. -/ -@[simp] -lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) : - Λ • (toReal d h).symm r = (toReal d h).symm r := - lorentzAction_on_isEmpty Λ ((toReal d h).symm r) - -/-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/ -@[simp] -lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) : - Λ • ofVecUp v = ofVecUp (Λ *ᵥ v) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - simp only [ofVecUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul] - rw [mulVec] - simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero, - Finset.sum_singleton] - erw [Finset.sum_equiv (ofVecUpIndexValue v)] - intro i - simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk] - intro j _ - simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl] - rfl - -/-- The action of the Lorentz group on `ofVecDown v` is - by vector multiplication of the transpose-inverse. -/ -@[simp] -lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) : - Λ • ofVecDown v = ofVecDown ((LorentzGroup.transpose Λ⁻¹) *ᵥ v) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - simp only [ofVecDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul, lorentzGroupIsGroup_inv] - rw [mulVec] - simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero, - Finset.sum_singleton] - erw [Finset.sum_equiv (ofVecUpIndexValue v)] - intro i - simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk] - intro j _ - simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl] - rfl - -@[simp] -lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Λ • ofMatUpUp M = ofMatUpUp (Λ.1 * M * (LorentzGroup.transpose Λ).1) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - erw [← Equiv.sum_comp (ofMatUpUpIndexValue M).symm] - simp only [ofMatUpUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul, mul_apply] - erw [Finset.sum_product] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul] - refine Finset.sum_congr rfl (fun y _ => ?_) - simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] - exact mul_right_comm _ _ _ - -@[simp] -lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Λ • ofMatDownDown M = ofMatDownDown ((LorentzGroup.transpose Λ⁻¹).1 * M * (Λ⁻¹).1) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - erw [← Equiv.sum_comp (ofMatDownDownIndexValue M).symm] - simp only [ofMatDownDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul, mul_apply] - erw [Finset.sum_product] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul] - refine Finset.sum_congr rfl (fun y _ => ?_) - simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] - exact mul_right_comm _ _ _ - -@[simp] -lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Λ • ofMatUpDown M = ofMatUpDown (Λ.1 * M * (Λ⁻¹).1) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - erw [← Equiv.sum_comp (ofMatUpDownIndexValue M).symm] - simp only [ofMatUpDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul, mul_apply] - erw [Finset.sum_product] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul] - refine Finset.sum_congr rfl (fun y _ => ?_) - simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] - exact mul_right_comm _ _ _ - -@[simp] -lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : - Λ • ofMatDownUp M = - ofMatDownUp ((LorentzGroup.transpose Λ⁻¹).1 * M * (LorentzGroup.transpose Λ).1) := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - erw [← Equiv.sum_comp (ofMatDownUpIndexValue M).symm] - simp only [ofMatDownUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty, - Finset.prod_empty, one_mul, mul_apply] - erw [Finset.sum_product] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul] - refine Finset.sum_congr rfl (fun y _ => ?_) - simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue] - exact mul_right_comm _ _ _ - -end lorentzAction - -end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean deleted file mode 100644 index eee0dff..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean +++ /dev/null @@ -1,444 +0,0 @@ -/- -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.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. - -The Lorentz action is currently only defined for finite and decidable types `X`. - --/ - -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 LorentzGroup BigOperators Marked - -/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a - color `μ`. - - This can be 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 - -lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) : - colorMatrix μ Λ = - Matrix.reindex (colorsIndexCast h).symm (colorsIndexCast h).symm (colorMatrix ν Λ) := by - subst h - rfl - -lemma colorMatrix_dual_cast {μ : Colors} (Λ : LorentzGroup d) : - colorMatrix (τ μ) Λ = Matrix.reindex (colorsIndexDualCastSelf) (colorsIndexDualCastSelf) - (colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by - match μ with - | .up => rfl - | .down => - ext i j - simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose, - lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose, - minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply] -lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) : - colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by - match μ with - | .up => rfl - | .down => - ext i j - simp only [colorMatrix, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply, - MonoidHom.coe_mk, OneHom.coe_mk, minkowskiMetric.dual_transpose] - -/-! - -## Lorentz group to tensor representation matrices. - --/ - -/-- The matrix representation of the Lorentz group given a color of index. -/ -@[simps!] -def toTensorRepMat {c : X → Colors} : - LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where - toFun Λ := fun i j => ∏ x, colorMatrix (c x) Λ (i x) (j x) - map_one' := by - ext i j - by_cases hij : i = j - · subst hij - simp only [map_one, Matrix.one_apply_eq, Finset.prod_const_one] - · obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij - simp only [map_one] - rw [@Finset.prod_eq_zero _ _ _ _ _ x] - exact Eq.symm (Matrix.one_apply_ne' fun a => hij (id (Eq.symm a))) - exact Finset.mem_univ x - exact Matrix.one_apply_ne' (id (Ne.symm hijx)) - map_mul' Λ Λ' := by - ext i j - rw [Matrix.mul_apply] - trans ∑ (k : IndexValue d c), ∏ x, - (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) - 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] - rfl - rw [h1] - simp only [map_mul] - rfl - refine Finset.sum_congr rfl (fun k _ => ?_) - rw [Finset.prod_mul_distrib] - -lemma toTensorRepMat_mul' (i j : IndexValue d c) : - toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c), - ∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by - simp [Matrix.mul_apply, IndexValue] - refine Finset.sum_congr rfl (fun k _ => ?_) - rw [Finset.prod_mul_distrib] - rfl - -lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors} - (i j : IndexValue d (Sum.elim cX cY)) : - toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 * - toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 := - Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ (i x) (j x) - -lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors} - (i j : IndexValue d cX) (k l : IndexValue d cY) : - toTensorRepMat Λ i j * toTensorRepMat Λ k l = - toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) := - (Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ - (indexValueSumEquiv.symm (i, k) x) (indexValueSumEquiv.symm (j, l) x)).symm - -/-! - -## Tensor representation matrices and marked tensors. - --/ - -lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n) - (i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) : - toTensorRepMat Λ i j * toTensorRepMat Λ k l = - toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) := - (Fintype.prod_sum_type fun x => - (colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm - -lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0)) - (k : S.MarkedIndexValue) : - toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k = - toTensorRepMat Λ⁻¹ (oneMarkedIndexValue - $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) - (oneMarkedIndexValue x) := by - rw [toTensorRepMat_apply, toTensorRepMat_apply] - erw [Finset.prod_singleton, Finset.prod_singleton] - simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv] - rw [colorMatrix_cast h, colorMatrix_dual_cast] - rw [Matrix.reindex_apply, Matrix.reindex_apply] - simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta, - Equiv.symm_symm, Matrix.submatrix_apply] - rw [colorMatrix_transpose] - simp only [Fin.isValue, Matrix.transpose_apply] - apply congrArg - simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk, - Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply, - Equiv.symm_apply_apply] - -lemma toTensorRepMap_sum_dual (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) (j : T.MarkedIndexValue) (k : S.MarkedIndexValue) : - ∑ x, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k - * toTensorRepMat Λ (oneMarkedIndexValue x) j = - toTensorRepMat 1 - (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j := by - trans ∑ x, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue$ (colorsIndexDualCast h).symm $ - oneMarkedIndexValue.symm k) (oneMarkedIndexValue x) * toTensorRepMat Λ (oneMarkedIndexValue x) j - apply Finset.sum_congr rfl (fun x _ => ?_) - rw [toTensorRepMat_oneMarkedIndexValue_dual] - rw [← Equiv.sum_comp oneMarkedIndexValue.symm] - change ∑ i, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ - oneMarkedIndexValue.symm k) i * toTensorRepMat Λ i j = _ - rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ] - -lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue) - (k : T.MarkedIndexValue) : T.coord (splitIndexValue.symm (i, k)) = ∑ j, toTensorRepMat 1 k j * - T.coord (splitIndexValue.symm (i, j)) := by - erw [Finset.sum_eq_single_of_mem k] - simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul] - exact Finset.mem_univ k - intro j _ hjk - simp [hjk, IndexValue] - exact Or.inl (Matrix.one_apply_ne' hjk) - -/-! - -## Definition of the Lorentz group action on Real Lorentz Tensors. - --/ - -/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/ -@[simps!] -instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where - smul Λ T := {color := T.color, - coord := fun i => ∑ j, toTensorRepMat Λ 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] - simp only [Matrix.one_apply_eq, one_mul, IndexValue] - rfl - exact Finset.mem_univ i - exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij)) - mul_smul Λ Λ' T := by - refine ext rfl ?_ - simp only [HSMul.hSMul] - funext i - have h1 : ∑ j : IndexValue d T.color, toTensorRepMat (Λ * Λ') 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 [toTensorRepMat_mul', 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 [toTensorRepMat, IndexValue] - rw [← mul_assoc] - congr - rw [Finset.prod_mul_distrib] - rfl - -lemma lorentzAction_smul_coord' {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (Λ : ↑(𝓛 d)) - (T : RealLorentzTensor d X) (i : IndexValue d T.color) : - (Λ • T).coord i = ∑ j : IndexValue d T.color, toTensorRepMat Λ i j * T.coord j := by - rfl - -/-! - -## Properties of the Lorentz action. - --/ - -/-- The action on an empty Lorentz tensor is trivial. -/ -lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) : - Λ • T = T := by - refine ext rfl ?_ - funext i - erw [lorentzAction_smul_coord] - simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul, - Finset.sum_singleton, toTensorRepMat_apply] - simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const, - Finset.card_singleton, one_smul] - -/-- The Lorentz action commutes with `mapIso`. -/ -lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) : - mapIso d f (Λ • T) = Λ • (mapIso d f T) := by - refine ext rfl ?_ - funext i - rw [mapIso_apply_coord] - rw [lorentzAction_smul_coord', lorentzAction_smul_coord'] - let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color := - indexValueIso d f ((Equiv.comp_symm_eq f ((mapIso d f) T).color T.color).mp rfl) - rw [← Equiv.sum_comp is] - refine Finset.sum_congr rfl (fun j _ => ?_) - rw [mapIso_apply_coord] - refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl - · simp only [IndexValue, toTensorRepMat, MonoidHom.coe_mk, OneHom.coe_mk, mapIso_apply_color, - indexValueIso_refl] - rw [← Equiv.prod_comp f] - apply Finset.prod_congr rfl (fun x _ => ?_) - have h1 : (T.color (f.symm (f x))) = T.color x := by - simp only [Equiv.symm_apply_apply] - rw [colorMatrix_cast h1] - apply congrArg - simp only [is] - erw [indexValueIso_eq_symm, indexValueIso_symm_apply'] - simp only [colorsIndexCast, Function.comp_apply, mapIso_apply_color, Equiv.cast_refl, - Equiv.refl_symm, Equiv.refl_apply, Equiv.cast_apply] - symm - refine cast_eq_iff_heq.mpr ?_ - congr - exact Equiv.symm_apply_apply f x - · apply congrArg - exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueIso d f (mapIso.proof_1 d f T))).mp rfl - -/-! - -## The Lorentz action on marked tensors. - --/ - -@[simps!] -instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction - -/-- Action of the Lorentz group on just marked indices. -/ -@[simps!] -def markedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where - smul Λ T := { - color := T.color, - coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j * - T.coord (splitIndexValue.symm ((splitIndexValue i).1, j))} - one_smul T := by - refine ext rfl ?_ - funext i - simp only [HSMul.hSMul, map_one] - erw [Finset.sum_eq_single_of_mem (splitIndexValue i).2] - erw [Matrix.one_apply_eq (splitIndexValue i).2] - simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply] - apply congrArg - exact Equiv.symm_apply_apply splitIndexValue i - exact Finset.mem_univ (splitIndexValue i).2 - exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij)) - mul_smul Λ Λ' T := by - refine ext rfl ?_ - simp only [HSMul.hSMul] - funext i - have h1 : ∑ (j : T.MarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).2 j - * T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) = - ∑ (j : T.MarkedIndexValue), ∑ (k : T.MarkedIndexValue), - (∏ x, ((colorMatrix (T.markedColor x) Λ ((splitIndexValue i).2 x) (k x)) * - (colorMatrix (T.markedColor x) Λ' (k x) (j x)))) * - T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) := by - refine Finset.sum_congr rfl (fun j _ => ?_) - rw [toTensorRepMat_mul', Finset.sum_mul] - rfl - erw [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 [toTensorRepMat, IndexValue] - rw [← mul_assoc] - congr - rw [Finset.prod_mul_distrib] - rfl - -/-- Action of the Lorentz group on just unmarked indices. -/ -@[simps!] -def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where - smul Λ T := { - color := T.color, - coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j * - T.coord (splitIndexValue.symm (j, (splitIndexValue i).2))} - one_smul T := by - refine ext rfl ?_ - funext i - simp only [HSMul.hSMul, map_one] - erw [Finset.sum_eq_single_of_mem (splitIndexValue i).1] - erw [Matrix.one_apply_eq (splitIndexValue i).1] - simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply] - apply congrArg - exact Equiv.symm_apply_apply splitIndexValue i - exact Finset.mem_univ (splitIndexValue i).1 - exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij)) - mul_smul Λ Λ' T := by - refine ext rfl ?_ - simp only [HSMul.hSMul] - funext i - have h1 : ∑ (j : T.UnmarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).1 j - * T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) = - ∑ (j : T.UnmarkedIndexValue), ∑ (k : T.UnmarkedIndexValue), - (∏ x, ((colorMatrix (T.unmarkedColor x) Λ ((splitIndexValue i).1 x) (k x)) * - (colorMatrix (T.unmarkedColor x) Λ' (k x) (j x)))) * - T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) := by - refine Finset.sum_congr rfl (fun j _ => ?_) - rw [toTensorRepMat_mul', Finset.sum_mul] - rfl - erw [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 [toTensorRepMat, IndexValue] - rw [← mul_assoc] - congr - rw [Finset.prod_mul_distrib] - rfl - -/-- Notation for `markedLorentzAction.smul`. -/ -scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul - -/-- Notation for `unmarkedLorentzAction.smul`. -/ -scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul - -/-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/ -lemma marked_unmarked_action_eq_action (T : Marked d X n) : Λ •ₘ (Λ •ᵤₘ T) = Λ • T := by - refine ext rfl ?_ - funext i - change ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j * - (∑ k, toTensorRepMat Λ (splitIndexValue i).1 k * T.coord (splitIndexValue.symm (k, j))) = _ - trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).2 j * - toTensorRepMat Λ (splitIndexValue i).1 k) * T.coord (splitIndexValue.symm (k, j)) - apply Finset.sum_congr rfl (fun j _ => ?_) - rw [Finset.mul_sum] - apply Finset.sum_congr rfl (fun k _ => ?_) - exact Eq.symm (mul_assoc _ _ _) - trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (k, j)) - * T.coord (splitIndexValue.symm (k, j))) - apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_))) - rw [mul_comm (toTensorRepMat _ _ _), toTensorRepMat_of_splitIndexValue'] - simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply] - trans ∑ p, (toTensorRepMat Λ i p * T.coord p) - rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type, Finset.sum_comm] - rfl - rfl - -/-- Acting on marked and then unmarked indices is equivalent to acting on all indices. -/ -lemma unmarked_marked_action_eq_action (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ • T := by - refine ext rfl ?_ - funext i - change ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j * - (∑ k, toTensorRepMat Λ (splitIndexValue i).2 k * T.coord (splitIndexValue.symm (j, k))) = _ - trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).1 j * - toTensorRepMat Λ (splitIndexValue i).2 k) * T.coord (splitIndexValue.symm (j, k)) - apply Finset.sum_congr rfl (fun j _ => ?_) - rw [Finset.mul_sum] - apply Finset.sum_congr rfl (fun k _ => ?_) - exact Eq.symm (mul_assoc _ _ _) - trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (j, k)) - * T.coord (splitIndexValue.symm (j, k))) - apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_))) - rw [toTensorRepMat_of_splitIndexValue'] - simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply] - trans ∑ p, (toTensorRepMat Λ i p * T.coord p) - rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type] - rfl - rfl - -/-- The marked and unmarked actions commute. -/ -lemma marked_unmarked_action_comm (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ •ₘ (Λ •ᵤₘ T) := by - rw [unmarked_marked_action_eq_action, marked_unmarked_action_eq_action] - -/-! TODO: Show that the Lorentz action commutes with contraction. -/ -/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/ -end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean deleted file mode 100644 index 7208059..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean +++ /dev/null @@ -1,485 +0,0 @@ -/- -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.Basic -import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction -/-! - -# Multiplication of Real Lorentz Tensors along an index - -We define the multiplication of two singularly marked Lorentz tensors along the -marked index. This is equivalent to contracting two Lorentz tensors. - -We prove various results about this multiplication. - --/ -/-! TODO: Set up a good notation for the multiplication. -/ - -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 - -/-- The contraction of the marked indices of two tensors each with one marked index, which -is dual to the others. The contraction is done via -`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/ -@[simps!] -def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) : - RealLorentzTensor d (X ⊕ Y) where - color := Sum.elim T.unmarkedColor S.unmarkedColor - coord := fun i => ∑ x, - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)) * - S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, - oneMarkedIndexValue $ colorsIndexDualCast h x)) - -/-- The index value appearing in the multiplication of Marked tensors on the left. -/ -def mulFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1} - (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor)) - (x : ColorsIndex d (T.color (markedPoint X 0))) : IndexValue d T.color := - splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x) - -lemma mulFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1} - (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor)) - (x : ColorsIndex d (T.color (markedPoint X 0))) : - mulFstArg i x (Sum.inr 0) = x := by - rfl - -lemma mulFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1} - (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor)) - (x : ColorsIndex d (T.color (markedPoint X 0))) (c : X): - mulFstArg i x (Sum.inl c) = i (Sum.inl c) := by - rfl - -/-- The index value appearing in the multiplication of Marked tensors on the right. -/ -def mulSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1} - (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor)) - (x : ColorsIndex d (T.color (markedPoint X 0))) (h : T.markedColor 0 = τ (S.markedColor 0)) : - IndexValue d S.color := - 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)) : - mapIso d (Equiv.sumComm X Y) (mul T S h) = mul S T (color_eq_dual_symm h) := by - refine ext ?_ ?_ - · funext a - cases a with - | inl _ => rfl - | inr _ => rfl - · funext i - rw [mul_colorsIndex_right] - refine Fintype.sum_congr _ _ (fun x => ?_) - rw [mul_comm] - 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) - (mapIso d (Equiv.sumCongr g (Equiv.refl _)) S) h := by - refine ext ?_ ?_ - · funext a - cases a with - | inl _ => rfl - | inr _ => rfl - · funext i - rw [mapIso_apply_coord, mul_coord, mul_coord] - refine Fintype.sum_congr _ _ (fun x => ?_) - rw [mapIso_apply_coord, mapIso_apply_coord] - refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl - · apply congrArg - exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl - · apply congrArg - exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl - -/-! - -## Lorentz action and multiplication. - --/ - -/-- The marked Lorentz Action leaves multiplication invariant. -/ -lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mul (Λ •ₘ T) (Λ •ₘ S) h = mul T S h := by - refine ext rfl ?_ - funext i - change ∑ x, (∑ j, toTensorRepMat Λ (oneMarkedIndexValue x) j * - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))) * - (∑ k, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k * - S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))) = _ - trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k - * toTensorRepMat Λ (oneMarkedIndexValue x) j) * - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) - * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k)) - apply Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul_sum] - apply Finset.sum_congr rfl (fun j _ => ?_) - apply Finset.sum_congr rfl (fun k _ => ?_) - ring - rw [Finset.sum_comm] - trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k - * toTensorRepMat Λ (oneMarkedIndexValue x) j) * - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) - * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k)) - apply Finset.sum_congr rfl (fun j _ => ?_) - rw [Finset.sum_comm] - trans ∑ j, ∑ k, (toTensorRepMat 1 - (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j) * - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) - * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k)) - apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_)) - rw [← Finset.sum_mul, ← Finset.sum_mul] - erw [toTensorRepMap_sum_dual] - rfl - rw [Finset.sum_comm] - trans ∑ k, - T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, - (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)))* - S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k)) - apply Finset.sum_congr rfl (fun k _ => ?_) - rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum T] - rw [← Equiv.sum_comp (oneMarkedIndexValue)] - erw [← Equiv.sum_comp (colorsIndexDualCast h)] - simp - rfl - -/-- The unmarked Lorentz Action commutes with multiplication. -/ -lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mul (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mul T S h := by - refine ext rfl ?_ - funext i - change ∑ x, (∑ j, toTensorRepMat Λ (indexValueSumEquiv i).1 j * - T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))* - ∑ k, toTensorRepMat Λ (indexValueSumEquiv i).2 k * - S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) = _ - trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueSumEquiv i).1 j * - T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))* - toTensorRepMat Λ (indexValueSumEquiv i).2 k * - S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) - · apply Finset.sum_congr rfl (fun x _ => ?_) - rw [Finset.sum_mul_sum ] - apply Finset.sum_congr rfl (fun j _ => ?_) - apply Finset.sum_congr rfl (fun k _ => ?_) - ring - rw [Finset.sum_comm] - trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j * - T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))* - toTensorRepMat Λ (indexValueSumEquiv i).2 k * - S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) - · exact Finset.sum_congr rfl (fun j _ => Finset.sum_comm) - trans ∑ j, ∑ k, - ((toTensorRepMat Λ (indexValueSumEquiv i).1 j) * toTensorRepMat Λ (indexValueSumEquiv i).2 k) - * ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x))) - * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) - · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_)) - rw [Finset.mul_sum] - apply Finset.sum_congr rfl (fun x _ => ?_) - ring - trans ∑ j, ∑ k, toTensorRepMat Λ i (indexValueSumEquiv.symm (j, k)) * - ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x))) - * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) - apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_)) - · rw [toTensorRepMat_of_indexValueSumEquiv'] - congr - simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color] - trans ∑ p, toTensorRepMat Λ i p * - ∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x))) - * S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2, - oneMarkedIndexValue $ colorsIndexDualCast h x)) - · erw [← Equiv.sum_comp indexValueSumEquiv.symm] - exact Eq.symm Fintype.sum_prod_type - rfl - -/-- The Lorentz action commutes with multiplication. -/ -lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mul (Λ • T) (Λ • S) h = Λ • mul T S h := by - simp only [← marked_unmarked_action_eq_action] - rw [mul_markedLorentzAction, mul_unmarkedLorentzAction] - -/-! - -## Multiplication on selected indices - --/ - -variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] - {X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y'] - [Fintype Z] [DecidableEq Z] - -/-- The multiplication of two real Lorentz Tensors along specified indices. -/ -@[simps!] -def mulS (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y) - (h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) := - mul (markSingle x T) (markSingle y S) h - -/-- The first index value appearing in the multiplication of two Lorentz tensors. -/ -def mulSFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) : - IndexValue d T.color := (markSingleIndexValue T x).symm (mulFstArg i a) - -lemma mulSFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)} - {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))} - (hij : i = j) (hab : a = b) : mulSFstArg i a = mulSFstArg j b := by - subst hij; subst hab - rfl - -lemma mulSFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) : - mulSFstArg i a x = a := by - rw [mulSFstArg, markSingleIndexValue] - simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply, - Sum.map_inr, id_eq] - erw [markEmbeddingIndexValue_apply_symm_on_mem] - swap - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero, - Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton] - rw [indexValueIso_symm_apply'] - erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq] - simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast] - symm - apply cast_eq_iff_heq.mpr - rw [embedSingleton_toEquivRange_symm] - rfl - -lemma mulSFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) - (c : X) (hc : c ≠ x) : mulSFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by - rw [mulSFstArg, markSingleIndexValue] - simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply, - Sum.map_inr, id_eq] - erw [markEmbeddingIndexValue_apply_symm_on_not_mem] - swap - simpa using hc - rfl - -/-- The second index value appearing in the multiplication of two Lorentz tensors. -/ -def mulSSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) - (h : T.color x = τ (S.color y)) : IndexValue d S.color := - (markSingleIndexValue S y).symm (mulSndArg i a h) - -lemma mulSSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) - (h : T.color x = τ (S.color y)) : mulSSndArg i a h y = colorsIndexDualCast h a := by - rw [mulSSndArg, markSingleIndexValue] - simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply, - Sum.map_inr, id_eq] - erw [markEmbeddingIndexValue_apply_symm_on_mem] - swap - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero, - Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton] - rw [indexValueIso_symm_apply'] - erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq] - simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast] - symm - apply cast_eq_iff_heq.mpr - rw [embedSingleton_toEquivRange_symm] - rfl - -lemma mulSSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) - (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) - (h : T.color x = τ (S.color y)) (c : Y) (hc : c ≠ y) : - mulSSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by - rw [mulSSndArg, markSingleIndexValue] - simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply, - Sum.map_inr, id_eq] - erw [markEmbeddingIndexValue_apply_symm_on_not_mem] - swap - simpa using hc - rfl - -lemma mulSSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y} - {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)} - {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))} - (h : T.color x = τ (S.color y)) (hij : i = j) (hab : a = b) : - mulSSndArg i a h = mulSSndArg j b h := by - subst hij - subst hab - rfl - -lemma mulS_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y) - (h : T.color x = τ (S.color y)) - (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) : - (mulS T S x y h).coord i = ∑ a, T.coord (mulSFstArg i a) * S.coord (mulSSndArg i a h) := by - rfl - -lemma mulS_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) - (eX : X ≃ X') (eY : Y ≃ Y') (x : X) (y : Y) (x' : X') (y' : Y') (hx : eX x = x') - (hy : eY y = y') (h : T.color x = τ (S.color y)) : - mulS (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) = - mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy)) - (mulS T S x y h) := by - rw [mulS, mulS, mul_mapIso] - congr 1 <;> rw [markSingle_mapIso] - -lemma mulS_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) - (x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) : - mulS (Λ • T) (Λ • S) x y h = Λ • mulS T S x y h := by - rw [mulS, mulS, ← mul_lorentzAction] - congr 1 - all_goals - rw [markSingle, markEmbedding, Equiv.trans_apply] - erw [lorentzAction_mapIso, lorentzAction_mapIso] - rfl - -lemma mulS_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) - (x : X) (y : Y) (h : T.color x = τ (S.color y)) : - mapIso d (Equiv.sumComm _ _) (mulS T S x y h) = mulS S T y x (color_eq_dual_symm h) := by - rw [mulS, mulS, mul_symm] - -/-- An equivalence of types associated with multiplying two consecutive indices, -with the second index appearing on the left. -/ -def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) : - {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃ - {y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} := - Equiv.subtypeSum.trans <| - Equiv.sumCongr ( - (Equiv.subtypeEquivRight (fun a => by - obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans - (Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <| - Equiv.subtypeUnivEquiv (fun a => Sum.inr_ne_inl) - -/-- An equivalence of types associated with multiplying two consecutive indices with the -second index appearing on the right. -/ -def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) : - {yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃ - {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} := - Equiv.subtypeSum.trans <| - Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => Sum.inl_ne_inr)) <| - (Equiv.subtypeEquivRight (fun a => by - obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <| - ((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans - (Equiv.subtypeEquivRight (fun y'' => And.comm))) - -/-- An equivalence of types associated with the associativity property of multiplication. -/ -def mulSAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) : - {x' // x' ≠ x} ⊕ {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} - ≃ {xy // xy ≠ (Sum.inr ⟨y', hy.symm⟩ : {x' // x' ≠ x} ⊕ {y'' // y'' ≠ y})} ⊕ {z' // z' ≠ z} := - (Equiv.sumCongr (Equiv.refl _) (mulSSplitLeft hy z)).trans <| - (Equiv.sumAssoc _ _ _).symm.trans <| - (Equiv.sumCongr (mulSSplitRight hy x).symm (Equiv.refl _)) - -lemma mulS_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} - {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z} - (h : T.color x = τ (S.color y)) - (h' : S.color y' = τ (U.color z)) : (mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color - = (mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by - funext a - match a with - | .inl ⟨.inl _, _⟩ => rfl - | .inl ⟨.inr _, _⟩ => rfl - | .inr _ => rfl - -/-- An equivalence of index values associated with the associativity property of multiplication. -/ -def mulSAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} - {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z} - (h : T.color x = τ (S.color y)) (h' : S.color y' = τ (U.color z)) : - IndexValue d ((T.mulS S x y h).mulS U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃ - IndexValue d (T.mulS (S.mulS U y' z h') x (Sum.inl ⟨y, hy⟩) h).color := - indexValueIso d (mulSAssocIso x hy z).symm (mulS_assoc_color hy h h') - -/-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/ -lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z) - (x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y)) - (h' : S.color y' = τ (U.color z)) : mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' = - mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by - apply ext (mulS_assoc_color _ _ _) ?_ - funext i - trans ∑ a, (∑ b, T.coord (mulSFstArg (mulSFstArg i a) b) * - S.coord (mulSSndArg (mulSFstArg i a) b h)) * U.coord (mulSSndArg i a h') - rfl - trans ∑ a, T.coord (mulSFstArg (mulSAssocIndexValue hy h h' i) a) * - (∑ b, S.coord (mulSFstArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b) * - U.coord (mulSSndArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b h')) - swap - rw [mapIso_apply_coord, mulS_coord_arg, indexValueIso_symm] - rfl - rw [Finset.sum_congr rfl (fun x _ => Finset.sum_mul _ _ _)] - rw [Finset.sum_congr rfl (fun x _ => Finset.mul_sum _ _ _)] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl (fun a _ => Finset.sum_congr rfl (fun b _ => ?_)) - rw [mul_assoc] - refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl - apply congrArg - funext c - by_cases hcy : c = y - · subst hcy - rw [mulSSndArg_on_mem, mulSFstArg_on_not_mem, mulSSndArg_on_mem] - rfl - · by_cases hcy' : c = y' - · subst hcy' - rw [mulSFstArg_on_mem, mulSSndArg_on_not_mem, mulSFstArg_on_mem] - · rw [mulSFstArg_on_not_mem, mulSSndArg_on_not_mem, mulSSndArg_on_not_mem, - mulSFstArg_on_not_mem] - rw [mulSAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply'] - simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mulS_color, Sum.elim_inr, - colorsIndexCast, Equiv.cast_refl, Equiv.refl_symm] - erw [Equiv.refl_apply] - rfl - exact hcy' - simpa using hcy - -end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean b/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean deleted file mode 100644 index 9791a6d..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean +++ /dev/null @@ -1,195 +0,0 @@ -/- -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/docs/references.bib b/docs/references.bib index 44c329a..0a3db38 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -20,6 +20,23 @@ year = "2022" } +@Article{ Dreiner:2008tw, + author = "Dreiner, Herbi K. and Haber, Howard E. and Martin, Stephen + P.", + title = "{Two-component spinor techniques and Feynman rules for + quantum field theory and supersymmetry}", + eprint = "0812.1594", + archiveprefix = "arXiv", + primaryclass = "hep-ph", + reportnumber = "BN-TH-2008-12, SCIPP-08-08, FERMILAB-PUB-09-855-T, + BN-TH-2008-12 and SCIPP-08/08", + doi = "10.1016/j.physrep.2010.05.002", + journal = "Phys. Rept.", + volume = "494", + pages = "1--196", + year = "2010" +} + @Article{ Lohitsiri:2019fuu, author = "Lohitsiri, Nakarin and Tong, David", title = "{Hypercharge Quantisation and Fermat's Last Theorem}", diff --git a/scripts/hepLean_style_lint.lean b/scripts/hepLean_style_lint.lean index 7d0b2fd..3dc6587 100644 --- a/scripts/hepLean_style_lint.lean +++ b/scripts/hepLean_style_lint.lean @@ -98,7 +98,7 @@ def hepLeanLintFile (path : FilePath) : IO (Array HepLeanErrorContext) := do substringLinter "( ", substringLinter "=by", substringLinter " def ", substringLinter "/-- We ", substringLinter "[ ", substringLinter " ]", substringLinter " ," , substringLinter "by exact ", - substringLinter "⟨ ", substringLinter " ⟩", substringLinter "):"] + substringLinter "⟨ ", substringLinter " ⟩", substringLinter "):", substringLinter "(_)"] let errors := allOutput.flatten return errors