From 0f4092e0ec301f31eb8f792963a891977f5c0691 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 25 Jul 2024 16:57:57 -0400 Subject: [PATCH] feat: Doing tensors generally --- HepLean/Mathematics/PiTensorProduct.lean | 367 +++++++++ HepLean/SpaceTime/LorentzTensor/Basic.lean | 430 ++++++++++ .../LorentzTensor/Complex/Basic.lean | 166 ++++ .../SpaceTime/LorentzTensor/Real/Basic.lean | 743 +++++------------- .../LorentzTensor/Real/Constructors.lean | 2 +- .../LorentzTensor/Real/Contraction.lean | 119 +++ .../LorentzTensor/Real/LorentzAction.lean | 296 ++----- .../LorentzTensor/Real/Multiplication.lean | 534 ------------- .../Real/MultiplicationUnit.lean | 36 +- .../LorentzTensor/Real/TensorProducts.lean | 177 +---- docs/references.bib | 17 + 11 files changed, 1408 insertions(+), 1479 deletions(-) create mode 100644 HepLean/Mathematics/PiTensorProduct.lean create mode 100644 HepLean/SpaceTime/LorentzTensor/Basic.lean create mode 100644 HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean diff --git a/HepLean/Mathematics/PiTensorProduct.lean b/HepLean/Mathematics/PiTensorProduct.lean new file mode 100644 index 0000000..186f2e6 --- /dev/null +++ b/HepLean/Mathematics/PiTensorProduct.lean @@ -0,0 +1,367 @@ +/- +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.DirectSum.Finsupp +import Mathlib.RingTheory.PiTensorProduct +import Mathlib.Algebra.DirectSum.Module +import Mathlib.LinearAlgebra.Multilinear.Basic +import Mathlib.LinearAlgebra.FinsuppVectorSpace +/-! +# Pi Tensor Products + +This file contains some proofs regarding Pi tensor products authored by Sophie Morel +in this Mathlib pull-request: + +https://github.com/leanprover-community/mathlib4/pull/11156 + +Once this pull request has being merged, this file will be deleted. + +-/ + +noncomputable section + +namespace MultilinearMap + +open DirectSum LinearMap BigOperators Function + +variable (R : Type*) [CommSemiring R] + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)] + +variable {M : (i : ι) → κ i → Type*} {M' : Type*} + +variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M'] + +variable [Π i (j : κ i), Module R (M i j)] [Module R M'] + +variable [Π i (j : κ i) (x : M i j), Decidable (x ≠ 0)] + +theorem fromDirectSum_aux1 (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') + (x : Π i, ⨁ (j : κ i), M i j) {p : Π i, κ i} + (hp : p ∉ Fintype.piFinset (fun i ↦ (x i).support)) : + (f p) (fun j ↦ (x j) (p j)) = 0 := by + simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hp + obtain ⟨i, hi⟩ := hp + exact (f p).map_coord_zero i hi + +theorem fromDirectSum_aux2 (x : Π i, ⨁ (j : κ i), M i j) (i : ι) (p : Π i, κ i) + (a : ⨁ (j : κ i), M i j) : + (fun j ↦ (update x i a j) (p j)) = update (fun j ↦ x j (p j)) i (a (p i)) := by + ext j + by_cases h : j =i + · rw [h]; simp only [update_same] + · simp only [ne_eq, h, not_false_eq_true, update_noteq] + +/-- Given a family indexed by `p : Π i : ι, κ i` of multilinear maps on the +`fun i ↦ M i (p i)`, construct a multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/ +def fromDirectSum (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') : + MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where + toFun x := ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) + map_add' x i a b := by + simp only + rename_i myinst _ _ _ _ _ _ _ + conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _ + (fun j ↦ (update x i a j).support) + ∪ @Fintype.piFinset _ myinst _ _ (fun j ↦ (update x i b j).support)) + (fun p _ hp ↦ by + letI := myinst + exact fromDirectSum_aux1 _ _ f _ hp)] + rw [Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p (a + b)])] + erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_add _ i (a (p i)) (b (p i)))] + rw [Finset.sum_add_distrib] + congr 1 + · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p a]), + Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)] + rw [Finset.sum_union_eq_left (fun p _ hp ↦ by + letI := myinst + exact fromDirectSum_aux1 _ _ f _ hp)] + · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p b]), + Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl), + Finset.sum_congr (Finset.union_comm _ _) (fun _ _ ↦ rfl), + Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)] + rw [Finset.sum_union_eq_left (fun p _ hp ↦ by + letI := myinst + exact fromDirectSum_aux1 _ _ f _ hp)] + map_smul' x i c a := by + simp only + rename_i myinst _ _ _ _ _ _ _ + conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _ + (fun j ↦ (update x i a j).support)) + (fun p _ hp ↦ by + letI := myinst + exact fromDirectSum_aux1 _ _ f _ hp), + Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p _])] + erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_smul _ i c (a (p i)))] + rw [← Finset.smul_sum] + conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p _]), + Finset.sum_union_eq_left (fun p _ hp ↦ by + letI := myinst + exact fromDirectSum_aux1 _ _ f _ hp)] + +@[simp] +theorem fromDirectSum_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') + (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSum R κ f x = + ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl + +/-- The construction `MultilinearMap.fromDirectSum`, as an `R`-linear map.-/ +def fromDirectSumₗ : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') →ₗ[R] + MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where + toFun := fromDirectSum R κ + map_add' f g := by + ext x + simp only [fromDirectSum_apply, Pi.add_apply, MultilinearMap.add_apply] + rw [Finset.sum_add_distrib] + map_smul' c f := by + ext x + simp only [fromDirectSum_apply, Pi.smul_apply, MultilinearMap.smul_apply, RingHom.id_apply] + rw [Finset.smul_sum] + +@[simp] +theorem fromDirectSumₗ_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') + (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumₗ R κ f x = + ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl + +theorem _root_.piFinset_support_lof_sub (p : Π i, κ i) (a : Π i, M i (p i)) : + Fintype.piFinset (fun i ↦ DFinsupp.support (lof R (κ i) (M i) (p i) (a i))) ⊆ {p} := by + intro q + simp only [Fintype.mem_piFinset, ne_eq, Finset.mem_singleton] + simp_rw [DirectSum.lof_eq_of] + exact fun hq ↦ funext fun i ↦ Finset.mem_singleton.mp (DirectSum.support_of_subset _ (hq i)) + +/-- The linear equivalence between families indexed by `p : Π i : ι, κ i` of multilinear maps +on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/ +def fromDirectSumEquiv : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') ≃ₗ[R] + MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' := by + refine LinearEquiv.ofLinear (fromDirectSumₗ R κ) (LinearMap.pi + (fun p ↦ MultilinearMap.compLinearMapₗ (fun i ↦ DirectSum.lof R (κ i) _ (p i)))) ?_ ?_ + · ext f x + simp only [coe_comp, Function.comp_apply, fromDirectSumₗ_apply, pi_apply, + MultilinearMap.compLinearMapₗ_apply, MultilinearMap.compLinearMap_apply, id_coe, id_eq] + change _ = f (fun i ↦ x i) + rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))] + rw [MultilinearMap.map_sum_finset] + sorry + · ext f p a + simp only [coe_comp, Function.comp_apply, LinearMap.pi_apply, compLinearMapₗ_apply, + compLinearMap_apply, fromDirectSumₗ_apply, id_coe, id_eq] + rw [Finset.sum_subset (piFinset_support_lof_sub R κ p a)] + · rw [Finset.sum_singleton] + simp only [lof_apply] + · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, + not_forall, not_not, forall_exists_index, forall_eq, lof_apply] + intro i hi + exact (f p).map_coord_zero i hi + +@[simp] +theorem fromDirectSumEquiv_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') + (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumEquiv R κ f x = + ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl + +@[simp] +theorem fromDirectSumEquiv_symm_apply (f : MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M') + (p : Π i, κ i) : (fromDirectSumEquiv R κ).symm f p = + f.compLinearMap (fun i ↦ DirectSum.lof R (κ i) _ (p i)) := rfl + +end MultilinearMap + +namespace PiTensorProduct + +open PiTensorProduct DirectSum LinearMap + +open scoped TensorProduct + +variable (R : Type*) [CommSemiring R] + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +variable {κ : ι → Type*} [(i : ι) → DecidableEq (κ i)] + +variable (M : (i : ι) → κ i → Type*) (M' : Type*) + +variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M'] + +variable [Π i (j : κ i), Module R (M i j)] [Module R M'] + +variable [Π i (j : κ i) (x : M i j), Decidable (x ≠ 0)] + +/-- The linear equivalence `⨂[R] i, (⨁ j : κ i, M i j) ≃ ⨁ p : (i : ι) → κ i, ⨂[R] i, M i (p i)`, + i.e. "tensor product distributes over direct sum". -/ +protected def directSum : + (⨂[R] i, (⨁ j : κ i, M i j)) ≃ₗ[R] ⨁ p : Π i, κ i, ⨂[R] i, M i (p i) := by + refine LinearEquiv.ofLinear (R := R) (R₂ := R) ?toFun ?invFun ?left ?right + · exact lift (MultilinearMap.fromDirectSumEquiv R (M := M) + (fun p ↦ (DirectSum.lof R _ _ p).compMultilinearMap (PiTensorProduct.tprod R))) + · exact DirectSum.toModule R _ _ (fun p ↦ lift (LinearMap.compMultilinearMap + (PiTensorProduct.map (fun i ↦ DirectSum.lof R _ _ (p i))) (tprod R))) + · ext p x + simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, toModule_lof, lift.tprod, + map_tprod, MultilinearMap.fromDirectSumEquiv_apply, id_comp] + rw [Finset.sum_subset (piFinset_support_lof_sub R κ p x)] + · rw [Finset.sum_singleton] + simp only [lof_apply] + · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, + not_forall, not_not, forall_exists_index, forall_eq, lof_apply] + intro i hi + rw [(tprod R).map_coord_zero i hi, LinearMap.map_zero] + · ext x + simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, lift.tprod, + MultilinearMap.fromDirectSumEquiv_apply, map_sum, toModule_lof, map_tprod, id_coe, id_eq] + change _ = tprod R (fun i ↦ x i) + rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))] + rw [MultilinearMap.map_sum_finset] + sorry + +end PiTensorProduct + +/-! +The case of `PiTensorProduct`. +-/ + +open DirectSum Set LinearMap Submodule TensorProduct + + +section PiTensorProduct + +open PiTensorProduct BigOperators + +attribute [local ext] TensorProduct.ext + +variable (R : Type*) [CommSemiring R] + +variable {ι : Type*} + +variable [Fintype ι] + +variable [DecidableEq ι] + +variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)] + +variable (M : ι → Type*) + +variable [∀ i, AddCommMonoid (M i)] + +variable [∀ i, Module R (M i)] + +variable [(i : ι) → (x : M i) → Decidable (x ≠ 0)] + +/-- If `ι` is a `Fintype`, `κ i` is a family of types indexed by `ι` and `M i` is a family +of modules indexed by `ι`, then the tensor product of the family `κ i →₀ M i` is linearly +equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`. +-/ +def finsuppPiTensorProduct : (⨂[R] i, κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ ⨂[R] i, M i := + PiTensorProduct.congr (fun i ↦ finsuppLEquivDirectSum R (M i) (κ i)) ≪≫ₗ + (PiTensorProduct.directSum R (fun (i : ι) ↦ fun (_ : κ i) ↦ M i)) ≪≫ₗ + (finsuppLEquivDirectSum R (⨂[R] i, M i) ((i : ι) → κ i)).symm + +@[simp] +theorem finsuppPiTensorProduct_single (p : (i : ι) → κ i) (m : (i : ι) → M i) : + finsuppPiTensorProduct R κ M (⨂ₜ[R] i, Finsupp.single (p i) (m i)) = + Finsupp.single p (⨂ₜ[R] i, m i) := by + classical + simp only [finsuppPiTensorProduct, PiTensorProduct.directSum, LinearEquiv.trans_apply, + congr_tprod, finsuppLEquivDirectSum_single, LinearEquiv.ofLinear_apply, lift.tprod, + MultilinearMap.fromDirectSumEquiv_apply, compMultilinearMap_apply, map_sum, + finsuppLEquivDirectSum_symm_lof] + rw [Finset.sum_subset (piFinset_support_lof_sub R κ p _)] + · rw [Finset.sum_singleton] + simp only [lof_apply] + · intro q _ hq + simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hq + obtain ⟨i, hi⟩ := hq + simp only [Finsupp.single_eq_zero] + exact (tprod R).map_coord_zero i hi + +@[simp] +theorem finsuppPiTensorProduct_apply (f : (i : ι) → (κ i →₀ M i)) (p : (i : ι) → κ i) : + finsuppPiTensorProduct R κ M (⨂ₜ[R] i, f i) p = ⨂ₜ[R] i, f i (p i) := by + rw [congrArg (tprod R) (funext (fun i ↦ (Eq.symm (Finsupp.sum_single (f i)))))] + erw [MultilinearMap.map_sum_finset (tprod R)] + simp only [map_sum, finsuppPiTensorProduct_single] + rw [Finset.sum_apply'] + rw [← Finset.sum_union_eq_right (s₁ := {p}) (fun _ _ h ↦ by + simp only [Fintype.mem_piFinset, Finsupp.mem_support_iff, ne_eq, not_forall, not_not] at h + obtain ⟨i, hi⟩ := h + rw [(tprod R).map_coord_zero i hi, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]), + Finset.sum_union_eq_left (fun _ _ h ↦ Finsupp.single_eq_of_ne (Finset.not_mem_singleton.mp h)), + Finset.sum_singleton, Finsupp.single_eq_same] + +@[simp] +theorem finsuppPiTensorProduct_symm_single (p : (i : ι) → κ i) (m : (i : ι) → M i) : + (finsuppPiTensorProduct R κ M).symm (Finsupp.single p (⨂ₜ[R] i, m i)) = + ⨂ₜ[R] i, Finsupp.single (p i) (m i) := + (LinearEquiv.symm_apply_eq _).2 (finsuppPiTensorProduct_single _ _ _ _ _).symm + +variable [(x : R) → Decidable (x ≠ 0)] + +/-- A variant of `finsuppPiTensorProduct` where all modules `M i` are the ground ring. +-/ +def finsuppPiTensorProduct' : (⨂[R] i, (κ i →₀ R)) ≃ₗ[R] ((i : ι) → κ i) →₀ R := + finsuppPiTensorProduct R κ (fun _ ↦ R) ≪≫ₗ + Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) (constantBaseRingEquiv ι R).toLinearEquiv + +@[simp] +theorem finsuppPiTensorProduct'_apply_apply (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i) : + finsuppPiTensorProduct' R κ (⨂ₜ[R] i, f i) p = ∏ i, f i (p i) := by + simp only [finsuppPiTensorProduct', LinearEquiv.trans_apply, Finsupp.lcongr_apply_apply, + Equiv.refl_symm, Equiv.refl_apply, finsuppPiTensorProduct_apply, AlgEquiv.toLinearEquiv_apply, + constantBaseRingEquiv_tprod] + +@[simp] +theorem finsuppPiTensorProduct'_tprod_single (p : (i : ι) → κ i) (r : ι → R) : + finsuppPiTensorProduct' R κ (⨂ₜ[R] i, Finsupp.single (p i) (r i)) = + Finsupp.single p (∏ i, r i) := by + ext q + simp only [finsuppPiTensorProduct'_apply_apply] + by_cases h : q = p + · rw [h]; simp only [Finsupp.single_eq_same] + · obtain ⟨i, hi⟩ := Function.ne_iff.mp h + rw [Finsupp.single_eq_of_ne (Ne.symm h), Finset.prod_eq_zero (Finset.mem_univ i) + (by rw [(Finsupp.single_eq_of_ne (Ne.symm hi))])] + +end PiTensorProduct + +section PiTensorProduct + +open PiTensorProduct BigOperators + +attribute [local ext] PiTensorProduct.ext + +open LinearMap + +open scoped TensorProduct + +variable {ι R : Type*} [CommSemiring R] + +variable {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] + +variable {κ : ι → Type*} + +variable [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(x : R) → Decidable (x ≠ 0)] + +/-- Let `ι` be a `Fintype` and `M` be a family of modules indexed by `ι`. If `b i : κ i → M i` +is a basis for every `i` in `ι`, then `fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i)` is a basis +of `⨂[R] i, M i`. +-/ +def Basis.piTensorProduct (b : Π i, Basis (κ i) R (M i)) : + Basis (Π i, κ i) R (⨂[R] i, M i) := + Finsupp.basisSingleOne.map + ((PiTensorProduct.congr (fun i ↦ (b i).repr)).trans <| + (finsuppPiTensorProduct R _ _).trans <| + Finsupp.lcongr (Equiv.refl _) (constantBaseRingEquiv _ R).toLinearEquiv).symm + +theorem Basis.piTensorProduct_apply (b : Π i, Basis (κ i) R (M i)) (p : Π i, κ i) : + Basis.piTensorProduct b p = ⨂ₜ[R] i, (b i) (p i) := by + simp only [piTensorProduct, LinearEquiv.trans_symm, Finsupp.lcongr_symm, Equiv.refl_symm, + AlgEquiv.toLinearEquiv_symm, map_apply, Finsupp.coe_basisSingleOne, LinearEquiv.trans_apply, + Finsupp.lcongr_single, Equiv.refl_apply, AlgEquiv.toLinearEquiv_apply, _root_.map_one] + apply LinearEquiv.injective (PiTensorProduct.congr (fun i ↦ (b i).repr)) + simp only [LinearEquiv.apply_symm_apply, congr_tprod, repr_self] + apply LinearEquiv.injective (finsuppPiTensorProduct R κ fun _ ↦ R) + simp only [LinearEquiv.apply_symm_apply, finsuppPiTensorProduct_single] + rfl + +end PiTensorProduct diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean new file mode 100644 index 0000000..61fe00d --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -0,0 +1,430 @@ +/- +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 +import Mathlib.Algebra.Module.Pi +import Mathlib.Algebra.Module.Equiv +import Mathlib.Algebra.Module.LinearMap.Basic +import Mathlib.LinearAlgebra.TensorProduct.Basic +import Mathlib.LinearAlgebra.TensorProduct.Basis +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] + +structure PreTensorStructure (R : Type) [CommSemiring R] where + Color : Type + ColorModule : Color → Type + τ : Color → Color + τ_involutive : Function.Involutive τ + colorModule_addCommMonoid : ∀ μ, AddCommMonoid (ColorModule μ) + colorModule_module : ∀ μ, Module R (ColorModule μ) + contrDual : ∀ μ, ColorModule μ ⊗[R] ColorModule (τ μ) →ₗ[R] R + +namespace PreTensorStructure + + +variable (𝓣 : PreTensorStructure 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} + +instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ + +instance : Module R (𝓣.ColorModule μ) := 𝓣.colorModule_module μ + +def Tensor (c : X → 𝓣.Color): Type := ⨂[R] x, 𝓣.ColorModule (c x) + +instance : AddCommMonoid (𝓣.Tensor c) := + PiTensorProduct.instAddCommMonoid fun i => 𝓣.ColorModule (c i) + +instance : Module R (𝓣.Tensor c) := PiTensorProduct.instModule + +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 := by + subst h + rfl + right_inv x := by + subst h + rfl + +/-! + +## Mapping isomorphisms + +-/ + +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 : c = d ∘ e) (h' : d = b ∘ e') : + c = b ∘ (e.trans e') := by + funext a + subst h h' + simp + +@[simp] +lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : c = d ∘ e) (h' : d = b ∘ 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 (d x)) e') + ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast (_)) _)) = + (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (c 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 : c = d ∘ e) (h' : d = b ∘ e') + (T : 𝓣.Tensor c) : + (𝓣.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 : c = d ∘ e) : + (𝓣.mapIso e h).symm = 𝓣.mapIso e.symm ((Equiv.eq_comp_symm e d c).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 (c x)) e).symm + ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _).symm ((PiTensorProduct.tprod R) x)) = + (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) + ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (d 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 : c = c) = 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 (fun x => 𝓣.ColorModule (c x)) e) ((PiTensorProduct.tprod R) f)) = _ + rw [PiTensorProduct.reindex_tprod] + simp only [PiTensorProduct.congr_tprod] + +/-! + +## Contraction + +-/ + +def pairProd : 𝓣.Tensor c ⊗[R] 𝓣.Tensor c₂ →ₗ[R] + ⨂[R] x, 𝓣.ColorModule (c x) ⊗[R] 𝓣.ColorModule (c₂ x) := + TensorProduct.lift ( + PiTensorProduct.map₂ (fun x => + TensorProduct.mk R (𝓣.ColorModule (c x)) (𝓣.ColorModule (c₂ 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] + + +def contrAll' : 𝓣.Tensor c ⊗[R] 𝓣.Tensor (𝓣.τ ∘ c) →ₗ[R] R := + (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) ∘ₗ + (PiTensorProduct.map (fun x => 𝓣.contrDual (c x))) ∘ₗ + (𝓣.pairProd) + +lemma contrAll'_mapIso_cond {e : X ≃ Y} (h : c = d ∘ e) : + 𝓣.τ ∘ d = (𝓣.τ ∘ c) ∘ ⇑e.symm := by + subst h + ext1 x + simp + +@[simp] +lemma contrAll'_mapIso (e : X ≃ Y) (h : c = d ∘ 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 + apply congrArg + rw [← LinearEquiv.symm_apply_eq] + rw [PiTensorProduct.reindex_symm] + rw [← PiTensorProduct.map_reindex] + subst h + simp + apply congrArg + rw [pairProd, pairProd] + simp + apply congrArg + change _ = ((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (d (e x))) (𝓣.ColorModule (𝓣.τ (d (e x))))) + ((PiTensorProduct.tprod R) fx)) + ((𝓣.mapIso e.symm _) ((PiTensorProduct.tprod R) fy)) + rw [mapIso_tprod] + simp + rw [PiTensorProduct.map₂_tprod_tprod] + change (PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (d x) ⊗[R] 𝓣.ColorModule (𝓣.τ (d x))) e.symm) + (((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (d x)) (𝓣.ColorModule (𝓣.τ (d x)))) + ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (fx (e.symm i)))) + ((PiTensorProduct.tprod R) fy)) = _ + rw [PiTensorProduct.map₂_tprod_tprod] + simp + erw [PiTensorProduct.reindex_tprod] + apply congrArg + funext i + simp + congr + simp [colorModuleCast] + apply cast_eq_iff_heq.mpr + rw [Equiv.symm_apply_apply] + +@[simp] +lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : c = d ∘ e) (x : 𝓣.Tensor c) (y : 𝓣.Tensor (𝓣.τ ∘ d)) : + 𝓣.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 + +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 = 𝓣.τ ∘ d ∘ e) : + d = 𝓣.τ ∘ c ∘ ⇑e.symm := by + subst h + ext1 x + simp + rw [𝓣.τ_involutive] + +lemma contrAll_mapIso_right_cond {e : X ≃ Y} {e' : Z ≃ Y} + (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ e') : c = 𝓣.τ ∘ b ∘ ⇑(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 = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ e') (x : 𝓣.Tensor c) (z : 𝓣.Tensor b) : + 𝓣.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 = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ 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 = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') : b = 𝓣.τ ∘ d ∘ ⇑(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 = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') (x : 𝓣.Tensor b) (y : 𝓣.Tensor d) : + 𝓣.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 = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') : + 𝓣.contrAll e h ∘ₗ + (TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor d))).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 + +structure TensorStructure (R : Type) [CommSemiring R] extends PreTensorStructure R where + 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 + +structure GroupTensorStructure (R : Type) [CommSemiring R] + (G : Type) [Group G] extends TensorStructure R where + repColorModule : (μ : Color) → Representation R G (ColorModule μ) + 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] + {c c₂ : X → 𝓣.Color} {d : Y → 𝓣.Color} {b : Z → 𝓣.Color} {d' : Y' → 𝓣.Color} {μ ν: 𝓣.Color} + + +def rep : Representation R G (𝓣.Tensor c) where + toFun g := PiTensorProduct.map (fun x => 𝓣.repColorModule (c 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 + +@[simp] +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 + + +@[simp] +lemma rep_mapIso (e : X ≃ Y) (h : c = d ∘ 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 + erw [mapIso_tprod] + simp [rep] + change (PiTensorProduct.map fun x => (𝓣.repColorModule (d x)) g) + ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (x (e.symm i))) = + (𝓣.mapIso e h) ((PiTensorProduct.map fun x => (𝓣.repColorModule (c x)) g) ((PiTensorProduct.tprod R) x)) + rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod] + rw [mapIso_tprod] + apply congrArg + funext i + subst h + simp + +@[simp] +lemma rep_mapIso_apply (e : X ≃ Y) (h : c = d ∘ e) (g : G) (x : 𝓣.Tensor c) : + (𝓣.rep g) ((𝓣.mapIso e h) x) = (𝓣.mapIso e h) ((𝓣.rep g) x) := by + trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x + rfl + simp + + + + + + + +end GroupTensorStructure + + +end diff --git a/HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean new file mode 100644 index 0000000..920f06b --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean @@ -0,0 +1,166 @@ +/- +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 +import Mathlib.Algebra.Module.Pi +import Mathlib.Algebra.Module.Equiv +import Mathlib.Algebra.Module.LinearMap.Basic +import Mathlib.LinearAlgebra.TensorProduct.Basic +import Mathlib.LinearAlgebra.TensorProduct.Basis +import Mathlib.Data.Complex.Basic +/-! + +# Complex Lorentz Tensors + +In this file we define complex 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] +-- For Van der Waerden notation see: [Dreiner et al.][Dreiner:2008tw] + +-/ + +/-- The possible `color` of an index for a complex Lorentz tensor. + There are four possiblities, specifying how the index transforms under `SL(2, C)`. + This follows Van der Waerden notation. -/ +inductive ComplexLorentzTensor.Color where + | up : ComplexLorentzTensor.Color + | down : ComplexLorentzTensor.Color + | weylUp : ComplexLorentzTensor.Color + | weylDown : ComplexLorentzTensor.Color + | weylUpDot : ComplexLorentzTensor.Color + | weylDownDot : ComplexLorentzTensor.Color + +/-- To set of allowed index values associated to a color of index. -/ +def ComplexLorentzTensor.ColorIndex (μ : ComplexLorentzTensor.Color) : Type := + match μ with + | ComplexLorentzTensor.Color.up => Fin 1 ⊕ Fin 3 + | ComplexLorentzTensor.Color.down => Fin 1 ⊕ Fin 3 + | ComplexLorentzTensor.Color.weylUp => Fin 2 + | ComplexLorentzTensor.Color.weylDown => Fin 2 + | ComplexLorentzTensor.Color.weylUpDot => Fin 2 + | ComplexLorentzTensor.Color.weylDownDot => Fin 2 + +/-- The instance of a finite type on the set of allowed index values for a given color. -/ +instance (μ : ComplexLorentzTensor.Color) : Fintype (ComplexLorentzTensor.ColorIndex μ) := + match μ with + | ComplexLorentzTensor.Color.up => instFintypeSum (Fin 1) (Fin 3) + | ComplexLorentzTensor.Color.down => instFintypeSum (Fin 1) (Fin 3) + | ComplexLorentzTensor.Color.weylUp => Fin.fintype 2 + | ComplexLorentzTensor.Color.weylDown => Fin.fintype 2 + | ComplexLorentzTensor.Color.weylUpDot => Fin.fintype 2 + | ComplexLorentzTensor.Color.weylDownDot => Fin.fintype 2 + +/-- The color index set for each color has a decidable equality. -/ +instance (μ : ComplexLorentzTensor.Color) : DecidableEq (ComplexLorentzTensor.ColorIndex μ) := + match μ with + | ComplexLorentzTensor.Color.up => instDecidableEqSum + | ComplexLorentzTensor.Color.down => instDecidableEqSum + | ComplexLorentzTensor.Color.weylUp => instDecidableEqFin 2 + | ComplexLorentzTensor.Color.weylDown => instDecidableEqFin 2 + | ComplexLorentzTensor.Color.weylUpDot => instDecidableEqFin 2 + | ComplexLorentzTensor.Color.weylDownDot => instDecidableEqFin 2 + +/-- The set of all index values associated with a map from `X` to `ComplexLorentzTensor.Color`. -/ +def ComplexLorentzTensor.IndexValue {X : Type} (c : X → ComplexLorentzTensor.Color) : Type := + (x : X) → ComplexLorentzTensor.ColorIndex (c x) + +/-- Complex lorentz tensors. -/ +def ComplexLorentzTensor {X : Type} (c : X → ComplexLorentzTensor.Color) : Type := + ComplexLorentzTensor.IndexValue c → ℂ + +/-- Complex Lorentz tensors form an additive commutative monoid. -/ +instance {X : Type} (c : X → ComplexLorentzTensor.Color) : + AddCommMonoid (ComplexLorentzTensor c) := Pi.addCommMonoid + +/-- Complex Lorentz tensors form a module over the complex numbers. -/ +instance {X : Type} (c : X → ComplexLorentzTensor.Color) : + Module ℂ (ComplexLorentzTensor c) := Pi.module _ _ _ + +/-- Complex Lorentz tensors form an additive commutative group. -/ +instance {X : Type} (c : X → ComplexLorentzTensor.Color) : + AddCommGroup (ComplexLorentzTensor c) := Pi.addCommGroup + +namespace ComplexLorentzTensor + +/-- A map taking every color to its dual color. -/ +def τ : Color → Color + | Color.up => Color.down + | Color.down => Color.up + | Color.weylUp => Color.weylDown + | Color.weylDown => Color.weylUp + | Color.weylUpDot => Color.weylDownDot + | Color.weylDownDot => Color.weylUpDot + +/-- The map τ is an involution. -/ +@[simp] +lemma τ_involutive : Function.Involutive τ := by + intro x + cases x <;> rfl + +/-! + +## Color index value + +-/ + +/-- An equivalence of `ColorIndex` types given an equality of color. -/ +def colorIndexCast {μ₁ μ₂ : Color} (h : μ₁ = μ₂) : + ColorIndex μ₁ ≃ ColorIndex μ₂ := Equiv.cast (congrArg ColorIndex h) + +@[simp] +lemma colorIndexCast_symm {μ₁ μ₂ : Color} (h : μ₁ = μ₂) : + (colorIndexCast h).symm = colorIndexCast h.symm := by + rfl + +/-- The allowed index values of a color are equal to that of the dual color. -/ +lemma colorIndex_eq_on_dual {μ ν : Color} (h : μ = τ ν) : + ColorIndex μ = ColorIndex ν := by + match μ, ν, h with + | .up, .down, _ => rfl + | .down, .up, _ => rfl + | .weylUp, .weylDown, _ => rfl + | .weylDown, .weylUp, _ => rfl + | .weylUpDot, .weylDownDot, _ => rfl + | .weylDownDot, .weylUpDot, _ => rfl + +/-- An equivalence between the allowed index values of a color and a color dual to it. -/ +def colorIndexDualCast {μ ν : Color} (h : μ = τ ν) : ColorIndex μ ≃ ColorIndex ν := + Equiv.cast (colorIndex_eq_on_dual h) + +@[simp] +lemma colorIndexDualCast_symm {μ ν : Color} (h : μ = τ ν) : (colorIndexDualCast h).symm = + colorIndexDualCast ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by + rfl + +@[simp] +lemma colorIndexDualCast_trans {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = τ ξ) : + (colorIndexDualCast h).trans (colorIndexDualCast h') = + colorIndexCast (by rw [h, h', τ_involutive]) := by + simp [colorIndexDualCast, colorIndexCast] + + +@[simp] +lemma colorIndexDualCast_trans_colorsIndexCast {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = ξ) : + (colorIndexDualCast h).trans (colorIndexCast h') = + colorIndexDualCast (by rw [h, h']) := by + simp [colorIndexDualCast, colorIndexCast] + +@[simp] +lemma colorIndexCast_trans_colorsIndexDualCast {μ ν ξ : Color} (h : μ = ν) (h' : ν = τ ξ) : + (colorIndexCast h).trans (colorIndexDualCast h') = + colorIndexDualCast (by rw [h, h']) := by + simp [colorIndexDualCast, colorIndexCast] + +end ComplexLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index ff30e69..dd05a6e 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -14,6 +14,8 @@ import Mathlib.Algebra.Module.Equiv import Mathlib.Algebra.Module.LinearMap.Basic import Mathlib.LinearAlgebra.TensorProduct.Basic import Mathlib.LinearAlgebra.TensorProduct.Basis +import Mathlib.LinearAlgebra.PiTensorProduct +import HepLean.Mathematics.PiTensorProduct /-! # Real Lorentz Tensors @@ -28,59 +30,106 @@ This will relation should be made explicit in the future. -- For modular operads see: [Raynor][raynor2021graphical] -/ -/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/ +/-! TODO: Relate the constructions here to `PiTensorProduct`. -/ /-! TODO: Generalize to maps into Lorentz tensors. -/ -/-- The possible `colors` of an index for a RealLorentzTensor. + + +section PiTensorProductResults +variable {ι ι₂ ι₃ : Type*} +variable {R : Type*} [CommSemiring R] +variable {R₁ R₂ : Type*} +variable {s : ι → Type*} [∀ i, AddCommMonoid (s i)] [∀ i, Module R (s i)] +variable {M : Type*} [AddCommMonoid M] [Module R M] +variable {E : Type*} [AddCommMonoid E] [Module R E] +variable {F : Type*} [AddCommMonoid F] + + +end PiTensorProductResults + +open TensorProduct +noncomputable section +/-- The possible `color` of an index for a RealLorentzTensor. There are two possiblities, `up` and `down`. -/ -inductive RealLorentzTensor.Colors where - | up : RealLorentzTensor.Colors - | down : RealLorentzTensor.Colors +inductive RealLorentzTensor.Color where + | up : RealLorentzTensor.Color + | down : RealLorentzTensor.Color -/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/ -def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type := +/-- To set of allowed index values associated to a color of index. -/ +def RealLorentzTensor.ColorIndex (d : ℕ) (μ : RealLorentzTensor.Color) : Type := match μ with - | RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d - | RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d + | RealLorentzTensor.Color.up => Fin 1 ⊕ Fin d + | RealLorentzTensor.Color.down => Fin 1 ⊕ Fin d -instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) := +/-- The instance of a finite type on the set of allowed index values for a given color. -/ +instance (d : ℕ) (μ : RealLorentzTensor.Color) : Fintype (RealLorentzTensor.ColorIndex d μ) := match μ with - | RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d) - | RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d) + | RealLorentzTensor.Color.up => instFintypeSum (Fin 1) (Fin d) + | RealLorentzTensor.Color.down => instFintypeSum (Fin 1) (Fin d) -instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) := +/-- The color index set for each color has a decidable equality. -/ +instance (d : ℕ) (μ : RealLorentzTensor.Color) : DecidableEq (RealLorentzTensor.ColorIndex d μ) := match μ with - | RealLorentzTensor.Colors.up => instDecidableEqSum - | RealLorentzTensor.Colors.down => instDecidableEqSum + | RealLorentzTensor.Color.up => instDecidableEqSum + | RealLorentzTensor.Color.down => instDecidableEqSum + +def RealLorentzTensor.ColorModule (d : ℕ) (μ : RealLorentzTensor.Color) : Type := + RealLorentzTensor.ColorIndex d μ → ℝ + +instance (d : ℕ) (μ : RealLorentzTensor.Color) : + AddCommMonoid (RealLorentzTensor.ColorModule d μ) := + Pi.addCommMonoid + +instance (d : ℕ) (μ : RealLorentzTensor.Color) : Module ℝ (RealLorentzTensor.ColorModule d μ) := + Pi.module _ _ _ + +instance (d : ℕ) (μ : RealLorentzTensor.Color) : AddCommGroup (RealLorentzTensor.ColorModule d μ) := + Pi.addCommGroup + +/-- Real Lorentz tensors. -/ +def RealLorentzTensor {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : Type := + ⨂[ℝ] i : X, RealLorentzTensor.ColorModule d (c i) + +instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : + AddCommMonoid (RealLorentzTensor d c) := + PiTensorProduct.instAddCommMonoid fun i => RealLorentzTensor.ColorModule d (c i) + +instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : + Module ℝ (RealLorentzTensor d c) := PiTensorProduct.instModule + + +instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : + AddCommGroup (RealLorentzTensor d c) := PiTensorProduct.instAddCommGroup + +namespace RealLorentzTensor + +variable {d : ℕ} {X Y Z : Type} (c : X → Color) + [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] /-- 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) +def IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : + Type 0 := (x : X) → ColorIndex d (c x) -def RealLorentzTensor.ColorFiber {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : Type := - RealLorentzTensor.IndexValue d c → ℝ +instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype -instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : - AddCommMonoid (RealLorentzTensor.ColorFiber d c) := Pi.addCommMonoid +instance [Fintype X] : DecidableEq (IndexValue d c) := + Fintype.decidablePiFintype -instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : - Module ℝ (RealLorentzTensor.ColorFiber d c) := Pi.module _ _ _ +def basisColorModule {d : ℕ} (μ : Color) : + Basis (ColorIndex d μ) ℝ (ColorModule d μ) := Pi.basisFun _ _ -instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : - AddCommGroup (RealLorentzTensor.ColorFiber d c) := Pi.addCommGroup +def basis (d : ℕ) (c : X → RealLorentzTensor.Color) : + Basis (IndexValue d c) ℝ (RealLorentzTensor d c) := + Basis.piTensorProduct (fun x => basisColorModule (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.ColorFiber d color +abbrev PiModule (d : ℕ) (c : X → Color) := IndexValue d c → ℝ + +def asPi {d : ℕ} {c : X → Color} : + RealLorentzTensor d c ≃ₗ[ℝ] PiModule d c := + (basis d c).repr ≪≫ₗ + Finsupp.linearEquivFunOnFinite ℝ ℝ (IndexValue d c) -namespace RealLorentzTensor -open Matrix -universe u1 -variable {d : ℕ} {X Y Z : Type} (c : X → Colors) /-! @@ -89,9 +138,9 @@ variable {d : ℕ} {X Y Z : Type} (c : X → Colors) -/ /-- The involution acting on colors. -/ -def τ : Colors → Colors - | Colors.up => Colors.down - | Colors.down => Colors.up +def τ : Color → Color + | Color.up => Color.down + | Color.down => Color.up /-- The map τ is an involution. -/ @[simp] @@ -99,75 +148,71 @@ lemma τ_involutive : Function.Involutive τ := by intro x cases x <;> rfl -lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ := +lemma color_eq_dual_symm {μ ν : Color} (h : μ = τ ν) : ν = τ μ := (Function.Involutive.eq_iff τ_involutive).mp h.symm -lemma color_comp_τ_symm {c1 c2 : X → Colors} (h : c1 = τ ∘ c2) : c2 = τ ∘ c1 := +lemma color_comp_τ_symm {c1 c2 : X → Color} (h : c1 = τ ∘ c2) : c2 = τ ∘ c1 := funext (fun x => color_eq_dual_symm (congrFun h x)) -/-- 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 `ColorIndex` types given an equality of colors. -/ +def colorIndexCast {d : ℕ} {μ₁ μ₂ : Color} (h : μ₁ = μ₂) : + ColorIndex d μ₁ ≃ ColorIndex d μ₂ := + Equiv.cast (congrArg (ColorIndex d) h) @[simp] -lemma colorsIndexCast_symm {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) : - (@colorsIndexCast d _ _ h).symm = colorsIndexCast h.symm := by +lemma colorIndexCast_symm {d : ℕ} {μ₁ μ₂ : Color} (h : μ₁ = μ₂) : + (@colorIndexCast d _ _ h).symm = colorIndexCast h.symm := by rfl -/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/ -def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}: - ColorsIndex d μ ≃ ColorsIndex d (τ μ) where +/-- An equivalence of `ColorIndex` between that of a color and that of its dual. + I.e. the allowed index values for a color and its dual are equivalent. -/ +def colorIndexDualCastSelf {d : ℕ} {μ : Color}: + ColorIndex d μ ≃ ColorIndex d (τ μ) where toFun x := match μ with - | RealLorentzTensor.Colors.up => x - | RealLorentzTensor.Colors.down => x + | Color.up => x + | Color.down => x invFun x := match μ with - | RealLorentzTensor.Colors.up => x - | RealLorentzTensor.Colors.down => x + | Color.up => x + | Color.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 +/-- An equivalence between the allowed index values of a color and a color dual to it. -/ +def colorIndexDualCast {μ ν : Color} (h : μ = τ ν) : ColorIndex d μ ≃ ColorIndex d ν := + (colorIndexCast h).trans colorIndexDualCastSelf.symm @[simp] -lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) : - (colorsIndexDualCast h).symm = - @colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by +lemma colorIndexDualCast_symm {μ ν : Color} (h : μ = τ ν) : (colorIndexDualCast h).symm = + @colorIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by match μ, ν with - | Colors.up, Colors.down => rfl - | Colors.down, Colors.up => rfl + | Color.up, Color.down => rfl + | Color.down, Color.up => rfl @[simp] -lemma colorsIndexDualCast_trans {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = τ ξ) : - (@colorsIndexDualCast d _ _ h).trans (colorsIndexDualCast h') = - colorsIndexCast (by rw [h, h', τ_involutive]) := by +lemma colorIndexDualCast_trans {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = τ ξ) : + (@colorIndexDualCast d _ _ h).trans (colorIndexDualCast h') = + colorIndexCast (by rw [h, h', τ_involutive]) := by match μ, ν, ξ with - | Colors.up, Colors.down, Colors.up => rfl - | Colors.down, Colors.up, Colors.down => rfl + | Color.up, Color.down, Color.up => rfl + | Color.down, Color.up, Color.down => rfl @[simp] -lemma colorsIndexDualCast_trans_colorsIndexCast {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = ξ) : - (@colorsIndexDualCast d _ _ h).trans (colorsIndexCast h') = - colorsIndexDualCast (by rw [h, h']) := by +lemma colorIndexDualCast_trans_colorsIndexCast {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = ξ) : + (@colorIndexDualCast d _ _ h).trans (colorIndexCast h') = + colorIndexDualCast (by rw [h, h']) := by match μ, ν, ξ with - | Colors.down, Colors.up, Colors.up => rfl - | Colors.up, Colors.down, Colors.down => rfl + | Color.down, Color.up, Color.up => rfl + | Color.up, Color.down, Color.down => rfl @[simp] -lemma colorsIndexCast_trans_colorsIndexDualCast {μ ν ξ : Colors} (h : μ = ν) (h' : ν = τ ξ) : - (colorsIndexCast h).trans (@colorsIndexDualCast d _ _ h') = - colorsIndexDualCast (by rw [h, h']) := by +lemma colorIndexCast_trans_colorsIndexDualCast {μ ν ξ : Color} (h : μ = ν) (h' : ν = τ ξ) : + (colorIndexCast h).trans (@colorIndexDualCast d _ _ h') = + colorIndexDualCast (by rw [h, h']) := by match μ, ν, ξ with - | Colors.up, Colors.up, Colors.down => rfl - | Colors.down, Colors.down, Colors.up => rfl + | Color.up, Color.up, Color.down => rfl + | Color.down, Color.down, Color.up => rfl /-! @@ -176,10 +221,7 @@ lemma colorsIndexCast_trans_colorsIndexDualCast {μ ν ξ : Colors} (h : μ = ν -/ -instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype -instance [Fintype X] : DecidableEq (IndexValue d c) := - Fintype.decidablePiFintype /-! @@ -188,20 +230,20 @@ instance [Fintype X] : DecidableEq (IndexValue d c) := -/ /-- An isomorphism of the type of index values given an isomorphism of sets. -/ -def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) : +def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Color} {j : Y → Color} (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 + (Equiv.piCongrRight (fun μ => colorIndexCast (congrFun h μ))).trans $ + Equiv.piCongrLeft (fun y => ColorIndex d (j y)) f @[simp] -lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} +lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Color} {j : Y → Color} (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 + (indexValueIso d f h).symm y x = (colorIndexCast (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) : +lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color} + {j : Y → Color} {k : Z → Color} (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 = @@ -218,7 +260,7 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : 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] + simp only [Function.comp_apply, colorIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast] apply cast_eq_iff_heq.mpr rw [Equiv.apply_symm_apply] @@ -229,7 +271,7 @@ lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : rfl @[simp] -lemma indexValueIso_refl (d : ℕ) (i : X → Colors) : +lemma indexValueIso_refl (d : ℕ) (i : X → Color) : indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by rfl @@ -242,17 +284,17 @@ lemma indexValueIso_refl (d : ℕ) (i : X → Colors) : -/ /-- The isomorphism between the index values of a color map and its dual. -/ -def indexValueDualIso (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y) +def indexValueDualIso (d : ℕ) {i : X → Color} {j : Y → Color} (e : X ≃ Y) (h : i = τ ∘ j ∘ e) : IndexValue d i ≃ IndexValue d j := - (Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ))).trans $ - Equiv.piCongrLeft (fun y => ColorsIndex d (j y)) e + (Equiv.piCongrRight (fun μ => colorIndexDualCast (congrFun h μ))).trans $ + Equiv.piCongrLeft (fun y => ColorIndex d (j y)) e -lemma indexValueDualIso_symm_apply' (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y) +lemma indexValueDualIso_symm_apply' (d : ℕ) {i : X → Color} {j : Y → Color} (e : X ≃ Y) (h : i = τ ∘ j ∘ e) (y : IndexValue d j) (x : X) : - (indexValueDualIso d e h).symm y x = (colorsIndexDualCast (congrFun h x)).symm (y (e x)) := by + (indexValueDualIso d e h).symm y x = (colorIndexDualCast (congrFun h x)).symm (y (e x)) := by rfl -lemma indexValueDualIso_cond_symm {i : X → Colors} {j : Y → Colors} {e : X ≃ Y} +lemma indexValueDualIso_cond_symm {i : X → Color} {j : Y → Color} {e : X ≃ Y} (h : i = τ ∘ j ∘ e) : j = τ ∘ i ∘ e.symm := by subst h simp only [Function.comp.assoc, Equiv.self_comp_symm, CompTriple.comp_eq] @@ -261,26 +303,26 @@ lemma indexValueDualIso_cond_symm {i : X → Colors} {j : Y → Colors} {e : X simp only [τ_involutive, Function.Involutive.comp_self, Function.comp_apply, id_eq] @[simp] -lemma indexValueDualIso_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y) +lemma indexValueDualIso_symm {d : ℕ} {i : X → Color} {j : Y → Color} (e : X ≃ Y) (h : i = τ ∘ j ∘ e) : (indexValueDualIso d e h).symm = indexValueDualIso d e.symm (indexValueDualIso_cond_symm h) := by ext i : 1 rw [← Equiv.symm_apply_eq] funext a rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply'] - erw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_symm, - colorsIndexDualCast_trans] - simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_apply] + erw [← Equiv.trans_apply, colorIndexDualCast_symm, colorIndexDualCast_symm, + colorIndexDualCast_trans] + simp only [Function.comp_apply, colorIndexCast, Equiv.cast_apply] apply cast_eq_iff_heq.mpr rw [Equiv.apply_symm_apply] -lemma indexValueDualIso_eq_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y) +lemma indexValueDualIso_eq_symm {d : ℕ} {i : X → Color} {j : Y → Color} (e : X ≃ Y) (h : i = τ ∘ j ∘ e) : indexValueDualIso d e h = (indexValueDualIso d e.symm (indexValueDualIso_cond_symm h)).symm := by rw [indexValueDualIso_symm] simp -lemma indexValueDualIso_cond_trans {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueDualIso_cond_trans {i : X → Color} {j : Y → Color} {k : Z → Color} {e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) : i = k ∘ (e.trans f) := by rw [h, h'] @@ -289,7 +331,7 @@ lemma indexValueDualIso_cond_trans {i : X → Colors} {j : Y → Colors} {k : Z rw [τ_involutive] @[simp] -lemma indexValueDualIso_trans {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueDualIso_trans {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color} (e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) : (indexValueDualIso d e h).trans (indexValueDualIso d f h') = indexValueIso d (e.trans f) (indexValueDualIso_cond_trans h h') := by @@ -300,14 +342,14 @@ lemma indexValueDualIso_trans {d : ℕ} {i : X → Colors} {j : Y → Colors} {k rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply', indexValueIso_symm_apply'] erw [← Equiv.trans_apply] - rw [colorsIndexDualCast_symm, colorsIndexDualCast_symm, colorsIndexDualCast_trans] - simp only [Function.comp_apply, colorsIndexCast, Equiv.symm_trans_apply, Equiv.cast_symm, + rw [colorIndexDualCast_symm, colorIndexDualCast_symm, colorIndexDualCast_trans] + simp only [Function.comp_apply, colorIndexCast, Equiv.symm_trans_apply, Equiv.cast_symm, Equiv.cast_apply, cast_cast] symm apply cast_eq_iff_heq.mpr rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply] -lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Color} {j : Y → Color} {k : Z → Color} {e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f) : i = τ ∘ k ∘ (e.trans f) := by rw [h, h'] @@ -315,7 +357,7 @@ lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Colors} {j : Y → C simp only [Function.comp_apply, Equiv.coe_trans] @[simp] -lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color} (e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f) : (indexValueDualIso d e h).trans (indexValueIso d f h') = indexValueDualIso d (e.trans f) (indexValueDualIso_cond_trans_indexValueIso h h') := by @@ -326,14 +368,14 @@ lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Colors} {j : Y indexValueIso_symm_apply',indexValueDualIso_eq_symm, indexValueDualIso_symm_apply'] rw [Equiv.symm_apply_eq] erw [← Equiv.trans_apply, ← Equiv.trans_apply] - simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm, - colorsIndexCast_symm, colorsIndexCast_trans_colorsIndexDualCast, colorsIndexDualCast_trans] - simp only [colorsIndexCast, Equiv.cast_apply] + simp only [Function.comp_apply, Equiv.symm_trans_apply, colorIndexDualCast_symm, + colorIndexCast_symm, colorIndexCast_trans_colorsIndexDualCast, colorIndexDualCast_trans] + simp only [colorIndexCast, Equiv.cast_apply] symm apply cast_eq_iff_heq.mpr rw [Equiv.symm_apply_apply] -lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Color} {j : Y → Color} {k : Z → Color} {e : X ≃ Y} {f : Y ≃ Z} (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f) : i = τ ∘ k ∘ (e.trans f) := by rw [h, h'] @@ -341,7 +383,7 @@ lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Colors} {j : Y → C simp only [Function.comp_apply, Equiv.coe_trans] @[simp] -lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors} +lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color} (e : X ≃ Y) (f : Y ≃ Z) (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f) : (indexValueIso d e h).trans (indexValueDualIso d f h') = indexValueDualIso d (e.trans f) (indexValueIso_trans_indexValueDualIso_cond h h') := by @@ -351,9 +393,9 @@ lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y rw [indexValueIso_symm_apply', indexValueDualIso_symm_apply', indexValueDualIso_eq_symm, indexValueDualIso_symm_apply'] erw [← Equiv.trans_apply, ← Equiv.trans_apply] - simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm, - colorsIndexCast_symm, colorsIndexDualCast_trans_colorsIndexCast, colorsIndexDualCast_trans] - simp only [colorsIndexCast, Equiv.cast_apply] + simp only [Function.comp_apply, Equiv.symm_trans_apply, colorIndexDualCast_symm, + colorIndexCast_symm, colorIndexDualCast_trans_colorsIndexCast, colorIndexDualCast_trans] + simp only [colorIndexCast, Equiv.cast_apply] symm apply cast_eq_iff_heq.mpr rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply] @@ -367,8 +409,8 @@ lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y -/ @[simps!] -def mapIsoFiber (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) : - ColorFiber d i ≃ₗ[ℝ] ColorFiber d j where +def mapIso {d : ℕ} (f : X ≃ Y) {i : X → Color} {j : Y → Color} (h : i = j ∘ f) : + RealLorentzTensor d i ≃ₗ[ℝ] RealLorentzTensor d j where toFun F := F ∘ (indexValueIso d f h).symm invFun F := F ∘ indexValueIso d f h map_add' F G := by rfl @@ -383,82 +425,21 @@ def mapIsoFiber (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h exact congrArg _ $ Equiv.apply_symm_apply (indexValueIso d f h) x @[simp] -lemma mapIsoFiber_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) : - (mapIsoFiber d f h).trans (mapIsoFiber d g h') = - mapIsoFiber d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by +lemma mapIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color} + {j : Y → Color} {k : Z → Color} (h : i = j ∘ f) (h' : j = k ∘ g) : + (@mapIso _ _ d f _ _ h).trans (mapIso g h') = + mapIso (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_)))) - simp only [LinearEquiv.coe_toEquiv, LinearEquiv.trans_apply, mapIsoFiber_apply, + simp only [LinearEquiv.coe_toEquiv, LinearEquiv.trans_apply, mapIso_apply, indexValueIso_symm, ← Equiv.trans_apply, indexValueIso_trans] rfl -lemma mapIsoFiber_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : - (mapIsoFiber d f h).symm = mapIsoFiber d f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by +lemma mapIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) : + (@mapIso _ _ d f _ _ h).symm = mapIso f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_)))) - simp only [LinearEquiv.coe_toEquiv, mapIsoFiber_symm_apply, mapIsoFiber_apply, indexValueIso_symm, + simp only [LinearEquiv.coe_toEquiv, mapIso_symm_apply, mapIso_apply, indexValueIso_symm, Equiv.symm_symm] -/-! - -## Extensionality - --/ - -lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color) - (h' : T₁.coord = mapIsoFiber d (Equiv.refl X) h.symm T₂.coord) : T₁ = T₂ := by - cases T₁ - cases T₂ - simp_all only [IndexValue, mk.injEq] - apply And.intro h - simp only at h - subst 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 := ⟨T.color ∘ f.symm, mapIsoFiber d f (by funext x; simp) T.coord⟩ - invFun T := ⟨T.color ∘ f, (mapIsoFiber d f (by funext x; simp)).symm T.coord⟩ - left_inv T := by - refine ext ?_ ?_ - · simp [Function.comp.assoc] - · simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm, - mapIsoFiber_trans] - congr - exact Equiv.self_trans_symm f - right_inv T := by - refine ext ?_ ?_ - · simp [Function.comp.assoc] - · simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm, - mapIsoFiber_trans] - congr - exact Equiv.symm_trans_self f - -@[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 - erw [← LinearEquiv.trans_apply, ← LinearEquiv.trans_apply, mapIsoFiber_trans, mapIsoFiber_trans] - rfl - -lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by - refine Equiv.coe_inj.mp ?_ - funext T - refine ext rfl ?_ - erw [← LinearEquiv.trans_apply] - rw [mapIso_symm_apply_coord, mapIsoFiber_trans, mapIsoFiber_symm] - rfl - -lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl /-! @@ -467,7 +448,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl -/ /-- 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} : +def indexValueTensorator {X Y : Type} {TX : X → Color} {TY : Y → Color} : 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 @@ -481,338 +462,37 @@ def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} : | 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) - -def indexValueFinOne {c : Fin 1 → Colors} : - ColorsIndex d (c 0) ≃ IndexValue d c 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 -/-! - -## 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 +/-! TODO : Move -/ +lemma tensorator_mapIso_cond {cX : X → Color} {cY : Y → Color} {cX' : X' → Color} + {cY' : Y' → Color} {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) : + Sum.elim cX cY = Sum.elim cX' cY' ∘ ⇑(eX.sumCongr eY) := by + subst hX hY ext1 x - cases' x <;> rfl + simp_all only [Function.comp_apply, Equiv.sumCongr_apply] + cases x with + | inl val => simp_all only [Sum.elim_inl, Function.comp_apply, Sum.map_inl] + | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply, Sum.map_inr] -/-- 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 +lemma indexValueTensorator_indexValueMapIso {cX : X → Color} {cY : Y → Color} {cX' : X' → Color} + {cY' : Y' → Color} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) : + (indexValueIso d (Equiv.sumCongr eX eY) (tensorator_mapIso_cond hX hY)).trans indexValueTensorator = + indexValueTensorator.trans (Equiv.prodCongr (indexValueIso d eX hX) (indexValueIso d eY hY)) := by + apply Equiv.ext + intro i + simp + simp [ indexValueTensorator] + apply And.intro + all_goals 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) + rw [indexValueIso_eq_symm, indexValueIso_symm_apply'] + rw [indexValueIso_eq_symm, indexValueIso_symm_apply'] + simp /-! -## Marking elements. +## A basis for Lorentz tensors -/ -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 noncomputable section basis @@ -821,28 +501,28 @@ open Set LinearMap Submodule variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X'] - (cX : X → Colors) (cY : Y → Colors) + (cX : X → Color) (cY : Y → Color) -def basisColorFiber : Basis (IndexValue d cX) ℝ (ColorFiber d cX) := Pi.basisFun _ _ +def basis : Basis (IndexValue d cX) ℝ (RealLorentzTensor d cX) := Pi.basisFun _ _ @[simp] def basisProd : - Basis (IndexValue d cX × IndexValue d cY) ℝ (ColorFiber d cX ⊗[ℝ] ColorFiber d cY) := - (Basis.tensorProduct (basisColorFiber cX) (basisColorFiber cY)) + Basis (IndexValue d cX × IndexValue d cY) ℝ (RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY) := + (Basis.tensorProduct (basis cX) (basis cY)) -lemma mapIsoFiber_basis {cX : X → Colors} {cY : Y → Colors} (e : X ≃ Y) (h : cX = cY ∘ e) - (i : IndexValue d cX) : (mapIsoFiber d e h) (basisColorFiber cX i) - = basisColorFiber cY (indexValueIso d e h i) := by +lemma mapIsoFiber_basis {cX : X → Color} {cY : Y → Color} (e : X ≃ Y) (h : cX = cY ∘ e) + (i : IndexValue d cX) : (mapIso e h) (basis cX i) + = basis cY (indexValueIso d e h i) := by funext a - rw [mapIsoFiber_apply] + rw [mapIso_apply] by_cases ha : a = ((indexValueIso d e h) i) · subst ha nth_rewrite 2 [indexValueIso_eq_symm] rw [Equiv.apply_symm_apply] - simp only [basisColorFiber] + simp only [basis] erw [Pi.basisFun_apply, Pi.basisFun_apply] simp only [stdBasis_same] - · simp only [basisColorFiber] + · simp only [basis] erw [Pi.basisFun_apply, Pi.basisFun_apply] simp rw [if_neg, if_neg] @@ -851,24 +531,7 @@ lemma mapIsoFiber_basis {cX : X → Colors} {cY : Y → Colors} (e : X ≃ Y) (h exact fun a_1 => ha (_root_.id (Eq.symm a_1)) - - - end basis -/-! - -## 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. -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean index 3630925..22089b8 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean @@ -29,7 +29,7 @@ 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 +def toReal (d : ℕ) {X : Type} (h : IsEmpty X) (f : X → Color) : RealLorentzTensor d f ≃ ℝ where toFun := fun T => T.coord (IsEmpty.elim h) invFun := fun r => { color := fun x => IsEmpty.elim h x, diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean new file mode 100644 index 0000000..f0b15e0 --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean @@ -0,0 +1,119 @@ +/- +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.TensorProducts +/-! + +# 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 +open TensorProduct +open Set LinearMap Submodule + +variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] + [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X'] + (cX : X → Color) (cY : Y → Color) + + + +/-- The contraction of all indices of two tensors with dual index-colors. + This is a bilinear map to ℝ. -/ +@[simps!] +def contrAll {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) : + RealLorentzTensor d f1 →ₗ[ℝ] RealLorentzTensor d f2 →ₗ[ℝ] ℝ where + toFun T := { + toFun := fun S => ∑ i, T i * S (indexValueDualIso d e hc i), + map_add' := fun S F => by + trans ∑ i, (T i * S (indexValueDualIso d e hc i) + T i * F (indexValueDualIso d e hc i)) + exact Finset.sum_congr rfl (fun i _ => mul_add _ _ _ ) + exact Finset.sum_add_distrib, + map_smul' := fun r S => by + trans ∑ i , r * (T i * S (indexValueDualIso d e hc i)) + refine Finset.sum_congr rfl (fun x _ => ?_) + ring_nf + rw [mul_assoc] + rfl + rw [← Finset.mul_sum] + rfl} + map_add' := fun T S => by + ext F + trans ∑ i , (T i * F (indexValueDualIso d e hc i) + S i * F (indexValueDualIso d e hc i)) + exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _) + exact Finset.sum_add_distrib + map_smul' := fun r T => by + ext S + trans ∑ i , r * (T i * S (indexValueDualIso d e hc i)) + refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _) + rw [← Finset.mul_sum] + rfl + +lemma contrAll_symm {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) + (h : f1 = τ ∘ f2 ∘ e) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) : + contrAll e h T S = contrAll e.symm (indexValueDualIso_cond_symm h) S T := by + rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d e h)] + refine Finset.sum_congr rfl (fun i _ => ?_) + rw [mul_comm, ← Equiv.trans_apply] + simp + +lemma contrAll_mapIsoFiber_right {f1 : X → Color} {f2 : Y → Color} + {g2 : Y' → Color} (e : X ≃ Y) (eY : Y ≃ Y') + (h : f1 = τ ∘ f2 ∘ e) (hY : f2 = g2 ∘ eY) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) : + contrAll e h T S = contrAll (e.trans eY) (indexValueDualIso_cond_trans_indexValueIso h hY) + T (mapIso eY hY S) := by + rw [contrAll_apply_apply, contrAll_apply_apply] + refine Finset.sum_congr rfl (fun i _ => Mathlib.Tactic.Ring.mul_congr rfl ?_ rfl) + rw [mapIso_apply, ← Equiv.trans_apply] + simp only [indexValueDualIso_trans_indexValueIso] + congr + ext1 x + simp only [Equiv.trans_apply, Equiv.symm_apply_apply] + +lemma contrAll_mapIsoFiber_left {f1 : X → Color} {f2 : Y → Color} + {g1 : X' → Color} (e : X ≃ Y) (eX : X ≃ X') + (h : f1 = τ ∘ f2 ∘ e) (hX : f1 = g1 ∘ eX) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) : + contrAll e h T S = contrAll (eX.symm.trans e) + (indexValueIso_trans_indexValueDualIso_cond ((Equiv.eq_comp_symm eX g1 f1).mpr hX.symm) h) + (mapIso eX hX T) S := by + rw [contrAll_symm, contrAll_mapIsoFiber_right _ eX _ hX, contrAll_symm] + rfl + +lemma contrAll_lorentzAction {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) + (hc : f1 = τ ∘ f2 ∘ e) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) (Λ : LorentzGroup d) : + contrAll e hc (Λ • T) (Λ • S) = contrAll e hc T S := by + change ∑ i, (∑ j, toTensorRepMat Λ i j * T j) * + (∑ k, toTensorRepMat Λ (indexValueDualIso d e hc i) k * S k) = _ + trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d e hc i) k * toTensorRepMat Λ i j) + * T j * S 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, ∑ i, (toTensorRepMat Λ (indexValueDualIso d e hc i) k + * toTensorRepMat Λ i j) * T j * S k + · apply Finset.sum_congr rfl (fun j _ => ?_) + rw [Finset.sum_comm] + trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j) * T j * S k + · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_)) + rw [← Finset.sum_mul, ← Finset.sum_mul] + erw [toTensorRepMat_indexValueDualIso_sum] + rw [Finset.sum_comm] + trans ∑ k, T (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) * S k + · apply Finset.sum_congr rfl (fun k _ => ?_) + rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum' T] + rw [← Equiv.sum_comp (indexValueDualIso d e hc), ← indexValueDualIso_symm e hc] + simp only [Equiv.symm_apply_apply, contrAll_apply_apply] + +end RealLorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean index 9edbc98..0d13fd9 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean @@ -19,15 +19,15 @@ 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} + (c : X → Color) (Λ Λ' : LorentzGroup d) {μ : Color} -open LorentzGroup BigOperators Marked +open LorentzGroup BigOperators /-- 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 +def colorMatrix (μ : Color) : LorentzGroup d →* Matrix (ColorIndex d μ) (ColorIndex d μ) ℝ where toFun Λ := match μ with | .up => fun i j => Λ.1 i j | .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j @@ -35,11 +35,11 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C ext i j match μ with | .up => - simp only [lorentzGroupIsGroup_one_coe, OfNat.ofNat, One.one, ColorsIndex] + simp only [lorentzGroupIsGroup_one_coe, OfNat.ofNat, One.one, ColorIndex] congr | .down => simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one] - simp only [OfNat.ofNat, One.one, ColorsIndex] + simp only [OfNat.ofNat, One.one, ColorIndex] congr map_mul' Λ Λ' := by ext i j @@ -51,18 +51,18 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C Matrix.transpose_mul, Matrix.transpose_apply] rfl -lemma colorMatrix_ext {μ : Colors} {a b c d : ColorsIndex d μ} (hab : a = b) (hcd : c = d) : +lemma colorMatrix_ext {μ : Color} {a b c d : ColorIndex d μ} (hab : a = b) (hcd : c = d) : (colorMatrix μ) Λ a c = (colorMatrix μ) Λ b d := by rw [hab, hcd] -lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) : +lemma colorMatrix_cast {μ ν : Color} (h : μ = ν) (Λ : LorentzGroup d) : colorMatrix ν Λ = - Matrix.reindex (colorsIndexCast h) (colorsIndexCast h) (colorMatrix μ Λ) := by + Matrix.reindex (colorIndexCast h) (colorIndexCast h) (colorMatrix μ Λ) := by subst h rfl -lemma colorMatrix_dual_cast {μ ν : Colors} (Λ : LorentzGroup d) (h : μ = τ ν) : - colorMatrix ν Λ = Matrix.reindex (colorsIndexDualCast h) (colorsIndexDualCast h) +lemma colorMatrix_dual_cast {μ ν : Color} (Λ : LorentzGroup d) (h : μ = τ ν) : + colorMatrix ν Λ = Matrix.reindex (colorIndexDualCast h) (colorIndexDualCast h) (colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by subst h match ν with @@ -70,16 +70,16 @@ lemma colorMatrix_dual_cast {μ ν : Colors} (Λ : LorentzGroup d) (h : μ = τ ext i j simp only [colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, τ, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose, minkowskiMetric.dual_dual, - Matrix.reindex_apply, colorsIndexDualCast_symm, Matrix.submatrix_apply] + Matrix.reindex_apply, colorIndexDualCast_symm, Matrix.submatrix_apply] rfl | .down => ext i j - simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose, + simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorIndexDualCastSelf, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose, minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply] rfl -lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) : +lemma colorMatrix_transpose {μ : Color} (Λ : LorentzGroup d) : colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by match μ with | .up => rfl @@ -96,7 +96,7 @@ lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) : /-- The matrix representation of the Lorentz group given a color of index. -/ @[simps!] -def toTensorRepMat {c : X → Colors} : +def toTensorRepMat {c : X → Color} : 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 @@ -135,18 +135,18 @@ lemma toTensorRepMat_mul' (i j : IndexValue d c) : rw [Finset.prod_mul_distrib] rfl -lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors} +lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Color} {cY : Y → Color} (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 := + toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueTensorator i).1 (indexValueTensorator j).1 * + toTensorRepMat Λ (indexValueTensorator i).2 (indexValueTensorator 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} +lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Color} {cY : Y → Color} (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)) := + toTensorRepMat Λ (indexValueTensorator.symm (i, k)) (indexValueTensorator.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 + (indexValueTensorator.symm (i, k) x) (indexValueTensorator.symm (j, l) x)).symm /-! @@ -154,7 +154,7 @@ lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colo -/ -lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Colors} {f2 : Y → Colors} +lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (i : IndexValue d f1) (j : IndexValue d f2) : toTensorRepMat Λ (indexValueDualIso d e hc i) j = toTensorRepMat Λ⁻¹ (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) j) i := by @@ -162,18 +162,18 @@ lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Colors} {f2 : Y → Colo apply Finset.prod_congr rfl (fun x _ => ?_) erw [colorMatrix_dual_cast Λ (congrFun hc x)] rw [Matrix.reindex_apply, colorMatrix_transpose] - simp only [Function.comp_apply, colorsIndexDualCast_symm, + simp only [Function.comp_apply, colorIndexDualCast_symm, Matrix.submatrix_apply, Matrix.transpose_apply] rw [indexValueDualIso_eq_symm, indexValueDualIso_symm_apply', indexValueDualIso_eq_symm, indexValueDualIso_symm_apply'] - rw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_trans] + rw [← Equiv.trans_apply, colorIndexDualCast_symm, colorsIndexDualCast_trans] apply colorMatrix_ext simp - simp [colorsIndexCast] + simp [colorIndexCast] apply cast_eq_iff_heq.mpr rw [Equiv.symm_apply_apply] -lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Colors} {f2 : Y → Colors} +lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (j : IndexValue d f1) (k : IndexValue d f2) : (∑ i : IndexValue d f1, toTensorRepMat Λ ((indexValueDualIso d e hc) i) k * toTensorRepMat Λ i j) = toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j := by @@ -183,8 +183,8 @@ lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Colors} {f2 : Y → Color rw [toTensorRepMat_indexValueDualIso_left] rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ] -lemma toTensorRepMat_one_coord_sum' {f1 : X → Colors} - (T : ColorFiber d f1) (k : IndexValue d f1) : +lemma toTensorRepMat_one_coord_sum' {f1 : X → Color} + (T : RealLorentzTensor d f1) (k : IndexValue d f1) : ∑ j, (toTensorRepMat 1 k j) * T j = T k := by erw [Finset.sum_eq_single_of_mem k] simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul] @@ -193,23 +193,6 @@ lemma toTensorRepMat_one_coord_sum' {f1 : X → Colors} simp only [IndexValue, map_one, mul_eq_zero] exact Or.inl (Matrix.one_apply_ne' hjk) -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_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) /-! @@ -217,8 +200,8 @@ lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue) -/ @[simps!] -def lorentzActionFiber {c : X → Colors} : - Representation ℝ (LorentzGroup d) (ColorFiber d c) where +def lorentzAction {c : X → Color} : + Representation ℝ (LorentzGroup d) (RealLorentzTensor d c) where toFun Λ := { toFun := fun T i => ∑ j, toTensorRepMat Λ i j * T j, map_add' := fun T S => by @@ -260,13 +243,14 @@ def lorentzActionFiber {c : X → Colors} : rw [← mul_assoc, Finset.prod_mul_distrib] rfl +scoped[RealLorentzTensor] infixl:78 " • " => lorentzAction + /-- The Lorentz action commutes with `mapIso`. -/ -lemma lorentzActionFiber_mapIsoFiber (e : X ≃ Y) {f1 : X → Colors} - {f2 : Y → Colors} (h : f1 = f2 ∘ e) (Λ : LorentzGroup d) - (T : ColorFiber d f1) : mapIsoFiber d e h (lorentzActionFiber Λ T) = - lorentzActionFiber Λ (mapIsoFiber d e h T) := by +lemma lorentzAction_mapIso (e : X ≃ Y) {f1 : X → Color} + {f2 : Y → Color} (h : f1 = f2 ∘ e) (Λ : LorentzGroup d) + (T : RealLorentzTensor d f1) : mapIso e h (Λ • T) = Λ • (mapIso e h T) := by funext i - rw [mapIsoFiber_apply, lorentzActionFiber_apply_apply, lorentzActionFiber_apply_apply] + rw [mapIso_apply, lorentzAction_apply_apply, lorentzAction_apply_apply] rw [← Equiv.sum_comp (indexValueIso d e h)] refine Finset.sum_congr rfl (fun j _ => Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl) · rw [← Equiv.prod_comp e] @@ -277,236 +261,48 @@ lemma lorentzActionFiber_mapIsoFiber (e : X ≃ Y) {f1 : X → Colors} apply colorMatrix_ext rw [indexValueIso_eq_symm, indexValueIso_symm_apply'] erw [← Equiv.eq_symm_apply] - simp only [Function.comp_apply, Equiv.symm_symm_apply, colorsIndexCast, Equiv.cast_symm, + simp only [Function.comp_apply, Equiv.symm_symm_apply, colorIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast, cast_eq] rw [indexValueIso_eq_symm, indexValueIso_symm_apply'] - simp [colorsIndexCast] + simp [colorIndexCast] symm refine cast_eq_iff_heq.mpr ?_ rw [Equiv.symm_apply_apply] - · rw [mapIsoFiber_apply] + · rw [mapIso_apply] apply congrArg rw [← Equiv.trans_apply] simp -/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/ -@[simps!] -instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where - smul Λ T := ⟨T.color, lorentzActionFiber Λ T.coord⟩ - one_smul T := by - refine ext rfl ?_ - simp only [HSMul.hSMul, map_one, LinearMap.one_apply] - rfl - mul_smul Λ Λ' T := by - refine ext rfl ?_ - simp [HSMul.hSMul] - 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, mapIsoFiber_apply] - simp only [lorentzActionFiber_apply_apply, Finset.univ_eq_empty, Finset.prod_empty, one_mul, - indexValueIso_refl, Equiv.refl_symm] - 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) := - ext rfl (lorentzActionFiber_mapIsoFiber f _ Λ T.coord) section variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X'] - (cX : X → Colors) (cY : Y → Colors) + (cX : X → Color) (cY : Y → Color) -lemma lorentzActionFiber_basis (Λ : LorentzGroup d) (i : IndexValue d cX) : - lorentzActionFiber Λ (basisColorFiber cX i) = - ∑ j, toTensorRepMat Λ j i • basisColorFiber cX j := by +lemma lorentzAction_basis (Λ : LorentzGroup d) (i : IndexValue d cX) : + Λ • (basis cX i) = ∑ j, toTensorRepMat Λ j i • basis cX j := by funext k - simp only [lorentzActionFiber, MonoidHom.coe_mk, OneHom.coe_mk, + simp only [lorentzAction, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.coe_mk, AddHom.coe_mk] rw [Finset.sum_apply] rw [Finset.sum_eq_single_of_mem i, Finset.sum_eq_single_of_mem k] change _ = toTensorRepMat Λ k i * (Pi.basisFun ℝ (IndexValue d cX)) k k - rw [basisColorFiber] + rw [basis] erw [Pi.basisFun_apply, Pi.basisFun_apply] simp exact Finset.mem_univ k intro b _ hbk - change toTensorRepMat Λ b i • (basisColorFiber cX) b k = 0 - erw [basisColorFiber, Pi.basisFun_apply] + change toTensorRepMat Λ b i • (basis cX) b k = 0 + erw [basis, Pi.basisFun_apply] simp [hbk] exact Finset.mem_univ i intro b hb hbk - erw [basisColorFiber, Pi.basisFun_apply] + erw [basis, Pi.basisFun_apply] simp [hbk] intro a subst a simp_all only [Finset.mem_univ, ne_eq, not_true_eq_false] end -/-! - -## 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 f1964d1..0000000 --- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean +++ /dev/null @@ -1,534 +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 - -section mulMarkedFiber - -variable {cX : X → Colors} {cY : Y → Colors} {fX : Fin 1 → Colors} {fY : Fin 1 → Colors} - -/-- The index value appearing in the multiplication of Marked tensors on the left. -/ -def mulMarkedFiberFstArg (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0)) : - IndexValue d (Sum.elim cX fX) := - indexValueSumEquiv.symm ((indexValueSumEquiv i).1, indexValueFinOne x) - -/-- The index value appearing in the multiplication of Marked tensors on the right. -/ -def mulMarkedFiberSndArg (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0)) - (h : fX 0 = τ (fY 0)) : IndexValue d (Sum.elim cY fY) := - indexValueSumEquiv.symm ((indexValueSumEquiv i).2, indexValueFinOne $ colorsIndexDualCast h x) - -def mulMarkedFiber (h : fX 0 = τ (fY 0)) : ColorFiber d (Sum.elim cX fX) →ₗ[ℝ] - ColorFiber d (Sum.elim cY fY) →ₗ[ℝ] ColorFiber d (Sum.elim cX cY) where - toFun T := { - toFun := fun S i => ∑ x, T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h), - map_add' := fun F S => by - funext i - trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) + - T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h)) - exact Finset.sum_congr rfl (fun x _ => mul_add _ _ _ ) - exact Finset.sum_add_distrib, - map_smul' := fun r S => by - funext i - trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h)) - refine Finset.sum_congr rfl (fun x _ => ?_) - ring_nf - rw [mul_assoc] - rfl - rw [← Finset.mul_sum] - rfl} - map_add' := fun T S => by - ext F - funext i - trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) + - S (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h)) - exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _) - exact Finset.sum_add_distrib - map_smul' := fun r T => by - ext S - funext i - trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h)) - refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _) - rw [← Finset.mul_sum] - rfl - -end mulMarkedFiber - -/-- 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 mulMarked {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 mulMarkedFstArg {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 mulMarkedFstArg_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))) : - mulMarkedFstArg i x (Sum.inr 0) = x := by - rfl - -lemma mulMarkedFstArg_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): - mulMarkedFstArg 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 mulMarkedSndArg {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 mulMarked_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) : - (mulMarked 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 mulMarked_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) : - (mulMarked 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 mulMarked_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 0)) : - (mulMarked 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 [mulMarked_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 mulMarked_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) (mulMarked T S h) = mulMarked S T (color_eq_dual_symm h) := by - refine ext ?_ ?_ - · funext a - cases a with - | inl _ => rfl - | inr _ => rfl - · funext i - rw [mulMarked_colorsIndex_right] - refine Fintype.sum_congr _ _ (fun x => ?_) - rw [mul_comm] - rfl - -/-- Multiplication commutes with `mapIso`. -/ -lemma mulMarked_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) (mulMarked T S h) = mulMarked (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, mapIsoFiber_apply, mapIsoFiber_apply, mulMarked_coord, mulMarked_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 mulMarked_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mulMarked (Λ •ₘ T) (Λ •ₘ S) h = mulMarked 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 mulMarked_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mulMarked (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mulMarked 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, mulMarked_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 mulMarked_lorentzAction (T : Marked d X 1) (S : Marked d Y 1) - (h : T.markedColor 0 = τ (S.markedColor 1)) : - mulMarked (Λ • T) (Λ • S) h = Λ • mulMarked T S h := by - simp only [← marked_unmarked_action_eq_action] - rw [mulMarked_markedLorentzAction, mulMarked_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 mult (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}) := - mulMarked (markSingle x T) (markSingle y S) h - -/-- The first index value appearing in the multiplication of two Lorentz tensors. -/ -def multFstArg {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 (mulMarkedFstArg i a) - -lemma multFstArg_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) : multFstArg i a = multFstArg j b := by - subst hij; subst hab - rfl - -lemma multFstArg_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))) : - multFstArg i a x = a := by - rw [multFstArg, 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 multFstArg_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) : multFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by - rw [multFstArg, 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 multSndArg {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 (mulMarkedSndArg i a h) - -lemma multSndArg_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)) : multSndArg i a h y = colorsIndexDualCast h a := by - rw [multSndArg, 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 multSndArg_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) : - multSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by - rw [multSndArg, 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 multSndArg_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) : - multSndArg i a h = multSndArg j b h := by - subst hij - subst hab - rfl - -lemma mult_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)) : - (mult T S x y h).coord i = ∑ a, T.coord (multFstArg i a) * S.coord (multSndArg i a h) := by - rfl - -lemma mult_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)) : - mult (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)) - (mult T S x y h) := by - rw [mult, mult, mulMarked_mapIso] - congr 1 <;> rw [markSingle_mapIso] - -lemma mult_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) - (x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) : - mult (Λ • T) (Λ • S) x y h = Λ • mult T S x y h := by - rw [mult, mult, ← mulMarked_lorentzAction] - congr 1 - all_goals - rw [markSingle, markEmbedding, Equiv.trans_apply] - erw [lorentzAction_mapIso, lorentzAction_mapIso] - rfl - -lemma mult_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) - (x : X) (y : Y) (h : T.color x = τ (S.color y)) : - mapIso d (Equiv.sumComm _ _) (mult T S x y h) = mult S T y x (color_eq_dual_symm h) := by - rw [mult, mult, mulMarked_symm] - -/-- An equivalence of types associated with multiplying two consecutive indices, -with the second index appearing on the left. -/ -def multSplitLeft {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 multSplitRight {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 multAssocIso (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 _) (multSplitLeft hy z)).trans <| - (Equiv.sumAssoc _ _ _).symm.trans <| - (Equiv.sumCongr (multSplitRight hy x).symm (Equiv.refl _)) - -lemma mult_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)) : (mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color - = (mapIso d (multAssocIso x hy z) (mult T (mult 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 multAssocIndexValue {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.mult S x y h).mult U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃ - IndexValue d (T.mult (S.mult U y' z h') x (Sum.inl ⟨y, hy⟩) h).color := - indexValueIso d (multAssocIso x hy z).symm (mult_assoc_color hy h h') - -/-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/ -lemma mult_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)) : mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' = - mapIso d (multAssocIso x hy z) (mult T (mult S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by - apply ext (mult_assoc_color _ _ _) ?_ - funext i - trans ∑ a, (∑ b, T.coord (multFstArg (multFstArg i a) b) * - S.coord (multSndArg (multFstArg i a) b h)) * U.coord (multSndArg i a h') - rfl - trans ∑ a, T.coord (multFstArg (multAssocIndexValue hy h h' i) a) * - (∑ b, S.coord (multFstArg (multSndArg (multAssocIndexValue hy h h' i) a h) b) * - U.coord (multSndArg (multSndArg (multAssocIndexValue hy h h' i) a h) b h')) - swap - rw [mapIso_apply_coord, mapIsoFiber_apply, mapIsoFiber_apply, mult_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 [multSndArg_on_mem, multFstArg_on_not_mem, multSndArg_on_mem] - rfl - · by_cases hcy' : c = y' - · subst hcy' - rw [multFstArg_on_mem, multSndArg_on_not_mem, multFstArg_on_mem] - · rw [multFstArg_on_not_mem, multSndArg_on_not_mem, multSndArg_on_not_mem, - multFstArg_on_not_mem] - rw [multAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply'] - simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mult_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 index 1a118a0..cfd125b 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean @@ -27,7 +27,7 @@ The main results of this file are: 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} + (T : RealLorentzTensor d X) (c : X → Color) (Λ Λ' : LorentzGroup d) {μ : Color} open Marked @@ -38,7 +38,7 @@ open Marked -/ /-- The unit for the multiplication of Lorentz tensors. -/ -def mulUnit (d : ℕ) (μ : Colors) : Marked d (Fin 1) 1 := +def mulUnit (d : ℕ) (μ : Color) : Marked d (Fin 1) 1 := match μ with | .up => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm) (ofMatUpDown 1) @@ -54,23 +54,23 @@ lemma mulUnit_down_coord : (mulUnit d Colors.down).coord = fun i => rfl @[simp] -lemma mulUnit_markedColor (μ : Colors) : (mulUnit d μ).markedColor 0 = τ μ := by +lemma mulUnit_markedColor (μ : Color) : (mulUnit d μ).markedColor 0 = τ μ := by cases μ case up => rfl case down => rfl -lemma mulUnit_dual_markedColor (μ : Colors) : τ ((mulUnit d μ).markedColor 0) = μ := by +lemma mulUnit_dual_markedColor (μ : Color) : τ ((mulUnit d μ).markedColor 0) = μ := by cases μ case up => rfl case down => rfl @[simp] -lemma mulUnit_unmarkedColor (μ : Colors) : (mulUnit d μ).unmarkedColor 0 = μ := by +lemma mulUnit_unmarkedColor (μ : Color) : (mulUnit d μ).unmarkedColor 0 = μ := by cases μ case up => rfl case down => rfl -lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) : +lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Color) : (mulUnit d μ).unmarkedColor = τ ∘ (mulUnit d μ).markedColor := by funext x fin_cases x @@ -78,7 +78,7 @@ lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) : mulUnit_markedColor] exact color_eq_dual_symm rfl -lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) : +lemma mulUnit_coord_diag (μ : Color) (i : (mulUnit d μ).UnmarkedIndexValue) : (mulUnit d μ).coord (splitIndexValue.symm (i, indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i)) = 1 := by cases μ @@ -92,7 +92,7 @@ lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) : rfl next h => exact False.elim (h rfl) -lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue) +lemma mulUnit_coord_off_diag (μ : Color) (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 @@ -118,7 +118,7 @@ lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue exact h exact hb (id (Eq.symm h1)) -lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) : +lemma mulUnit_right (μ : Color) (T : Marked d X 1) (h : T.markedColor 0 = μ) : multMarked T (mulUnit d μ) (h.trans (mulUnit_dual_markedColor μ).symm) = T := by refine ext ?_ ?_ · funext a @@ -130,9 +130,9 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) funext i rw [mulMarked_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 + T.coord (splitIndexValue.symm ((indexValueTensorator i).1, _)) * + (mulUnit d μ).coord (splitIndexValue.symm ((indexValueTensorator i).2, j)) = _ + let y := indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) (indexValueTensorator i).2 erw [Finset.sum_eq_single_of_mem y] rw [mulUnit_coord_diag] simp only [Fin.isValue, mul_one] @@ -140,14 +140,14 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) funext a match a with | .inl a => - change (indexValueSumEquiv i).1 a = _ + change (indexValueTensorator i).1 a = _ rfl | .inr 0 => change oneMarkedIndexValue - ((colorsIndexDualCast (Eq.trans h (Eq.symm (mulUnit_dual_markedColor μ)))).symm + ((colorIndexDualCast (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, + simp only [Fin.isValue, oneMarkedIndexValue, colorIndexDualCast, colorIndexCast, 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, @@ -157,15 +157,15 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) intro b _ hab rw [mul_eq_zero] apply Or.inr - exact mulUnit_coord_off_diag μ (indexValueSumEquiv i).2 b hab + exact mulUnit_coord_off_diag μ (indexValueTensorator i).2 b hab -lemma mulUnit_left (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) : +lemma mulUnit_left (μ : Color) (T : Marked d X 1) (h : T.markedColor 0 = μ) : multMarked (mulUnit d μ) T ((mulUnit_markedColor μ).trans (congrArg τ h.symm)) = mapIso d (Equiv.sumComm X (Fin 1)) T := by rw [← mult_symmd_symm, mulUnit_right] exact h -lemma mulUnit_lorentzAction (μ : Colors) (Λ : LorentzGroup d) : +lemma mulUnit_lorentzAction (μ : Color) (Λ : LorentzGroup d) : Λ • mulUnit d μ = mulUnit d μ := by match μ with | Colors.up => diff --git a/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean b/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean index 8c51152..6aef014 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean @@ -19,7 +19,7 @@ open Set LinearMap Submodule variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X'] - (cX : X → Colors) (cY : Y → Colors) + (cX : X → Color) (cY : Y → Color) /-! @@ -31,65 +31,60 @@ variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [ /-- An equivalence between `ColorFiber d (Sum.elim cX cY)` and `ColorFiber d cX ⊗[ℝ] ColorFiber d cY`. This is related to the `tensorator` of the monoidal functor defined by `ColorFiber`, hence the terminology. -/ -def tensorator {cX : X → Colors} {cY : Y → Colors} : - ColorFiber d (Sum.elim cX cY) ≃ₗ[ℝ] ColorFiber d cX ⊗[ℝ] ColorFiber d cY := - (basisColorFiber (Sum.elim cX cY)).equiv (basisProd cX cY) indexValueSumEquiv +def tensorator {cX : X → Color} {cY : Y → Color} : + RealLorentzTensor d (Sum.elim cX cY) ≃ₗ[ℝ] RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY := + (basis (Sum.elim cX cY)).equiv (basisProd cX cY) indexValueTensorator -lemma tensorator_symm_apply {cX : X → Colors} {cY : Y → Colors} - (X : ColorFiber d cX ⊗[ℝ] ColorFiber d cY) (i : IndexValue d (Sum.elim cX cY)) : - (tensorator.symm X) i = (basisProd cX cY).repr X (indexValueSumEquiv i) := by +lemma tensorator_symm_apply {cX : X → Color} {cY : Y → Color} + (X : RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY) (i : IndexValue d (Sum.elim cX cY)) : + (tensorator.symm X) i = (basisProd cX cY).repr X (indexValueTensorator i) := by rfl -/-! TODO : Move -/ -lemma tensorator_mapIso_cond {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors} - {cY' : Y' → Colors} {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) : - Sum.elim cX cY = Sum.elim cX' cY' ∘ ⇑(eX.sumCongr eY) := by - subst hX hY - ext1 x - simp_all only [Function.comp_apply, Equiv.sumCongr_apply] - cases x with - | inl val => simp_all only [Sum.elim_inl, Function.comp_apply, Sum.map_inl] - | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply, Sum.map_inr] + /-- The naturality condition for the `tensorator`. -/ -lemma tensorator_mapIso {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors} - {cY' : Y' → Colors} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) : - (mapIsoFiber d (Equiv.sumCongr eX eY) (tensorator_mapIso_cond hX hY)).trans tensorator = - tensorator.trans (TensorProduct.congr (mapIsoFiber d eX hX) (mapIsoFiber d eY hY)) := by - apply (basisColorFiber (Sum.elim cX cY)).ext' +lemma tensorator_mapIso {cX : X → Color} {cY : Y → Color} {cX' : X' → Color} + {cY' : Y' → Color} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) : + (@mapIso _ _ d (Equiv.sumCongr eX eY) _ _ (tensorator_mapIso_cond hX hY)).trans tensorator = + tensorator.trans (TensorProduct.congr (mapIso eX hX) (mapIso eY hY)) := by + apply (basis (Sum.elim cX cY)).ext' intro i simp nth_rewrite 2 [tensorator] simp rw [Basis.tensorProduct_apply, TensorProduct.congr_tmul, mapIsoFiber_basis] rw [tensorator] - simp + simp only [basisProd, Basis.equiv_apply] rw [Basis.tensorProduct_apply, mapIsoFiber_basis, mapIsoFiber_basis] congr - sorry - sorry + rw [← Equiv.trans_apply, indexValueTensorator_indexValueMapIso] + rfl + exact hY + rw [← Equiv.trans_apply, indexValueTensorator_indexValueMapIso] + rfl + exact hX lemma tensorator_lorentzAction (Λ : LorentzGroup d) : - (tensorator).toLinearMap ∘ₗ lorentzActionFiber Λ - = (TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) ) ∘ₗ + (tensorator).toLinearMap ∘ₗ lorentzAction Λ + = (TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) ) ∘ₗ ((@tensorator d X Y _ _ _ _ cX cY).toLinearMap) := by - apply (basisColorFiber (Sum.elim cX cY)).ext + apply (basis (Sum.elim cX cY)).ext intro i nth_rewrite 2 [tensorator] simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, Basis.equiv_apply] - rw [basisProd, Basis.tensorProduct_apply, TensorProduct.map_tmul, lorentzActionFiber_basis, - lorentzActionFiber_basis, lorentzActionFiber_basis, map_sum, tmul_sum] + rw [basisProd, Basis.tensorProduct_apply, TensorProduct.map_tmul, lorentzAction_basis, + lorentzAction_basis, lorentzAction_basis, map_sum, tmul_sum] simp only [sum_tmul] - rw [← Equiv.sum_comp (indexValueSumEquiv).symm, Fintype.sum_prod_type, Finset.sum_comm] + rw [← Equiv.sum_comp (indexValueTensorator).symm, Fintype.sum_prod_type, Finset.sum_comm] refine Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_))) rw [tmul_smul, smul_tmul, tmul_smul, smul_smul, map_smul] congr 1 · rw [toTensorRepMat_of_indexValueSumEquiv, Equiv.apply_symm_apply, mul_comm] · simp [tensorator] -lemma tensorator_lorentzAction_apply (Λ : LorentzGroup d) (T : ColorFiber d (Sum.elim cX cY)) : - tensorator (lorentzActionFiber Λ T) = - TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (tensorator T) := by +lemma tensorator_lorentzAction_apply (Λ : LorentzGroup d) (T : RealLorentzTensor d (Sum.elim cX cY)) : + tensorator (Λ • T) = + TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) (tensorator T) := by erw [← LinearMap.comp_apply, tensorator_lorentzAction] rfl @@ -106,33 +101,33 @@ def decompEmbedSet (f : Y ↪ X) : Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <| (Function.Embedding.toEquivRange f).symm -def decompEmbedColorLeft (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Colors := +def decompEmbedColorLeft (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Color := (cX ∘ (decompEmbedSet f).symm) ∘ Sum.inl -def decompEmbedColorRight (f : Y ↪ X) : Y → Colors := +def decompEmbedColorRight (f : Y ↪ X) : Y → Color := (cX ∘ (decompEmbedSet f).symm) ∘ Sum.inr /-- Decomposes a tensor into a tensor product based on an embedding. -/ def decompEmbed (f : Y ↪ X) : - ColorFiber d cX ≃ₗ[ℝ] ColorFiber d (decompEmbedColorLeft cX f) ⊗[ℝ] ColorFiber d (cX ∘ f) := - (@mapIsoFiber _ _ d (decompEmbedSet f) cX (Sum.elim (decompEmbedColorLeft cX f) + RealLorentzTensor d cX ≃ₗ[ℝ] RealLorentzTensor d (decompEmbedColorLeft cX f) ⊗[ℝ] RealLorentzTensor d (cX ∘ f) := + (@mapIso _ _ d (decompEmbedSet f) cX (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorRight cX f)) (by simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl)).trans tensorator -lemma decompEmbed_lorentzAction_apply {f : Y ↪ X} (Λ : LorentzGroup d) (T : ColorFiber d cX) : - decompEmbed cX f (lorentzActionFiber Λ T) = - TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (decompEmbed cX f T) := by +lemma decompEmbed_lorentzAction_apply {f : Y ↪ X} (Λ : LorentzGroup d) (T : RealLorentzTensor d cX) : + decompEmbed cX f (Λ • T) = + TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) (decompEmbed cX f T) := by rw [decompEmbed] simp - rw [lorentzActionFiber_mapIsoFiber] + rw [lorentzAction_mapIso] exact tensorator_lorentzAction_apply (decompEmbedColorLeft cX f) (decompEmbedColorRight cX f) Λ - ((mapIsoFiber d (decompEmbedSet f) (decompEmbed.proof_2 cX f)) T) + ((mapIso (decompEmbedSet f) (decompEmbed.proof_2 cX f)) T) def decompEmbedProd (f : X' ↪ X) (g : Y' ↪ Y) : - ColorFiber d cX ⊗[ℝ] ColorFiber d cY ≃ₗ[ℝ] - ColorFiber d (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorLeft cY g)) - ⊗[ℝ] (ColorFiber d (cX ∘ f) ⊗[ℝ] ColorFiber d (cY ∘ g)) := + RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY ≃ₗ[ℝ] + RealLorentzTensor d (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorLeft cY g)) + ⊗[ℝ] (RealLorentzTensor d (cX ∘ f) ⊗[ℝ] RealLorentzTensor d (cY ∘ g)) := (TensorProduct.congr (decompEmbed cX f) (decompEmbed cY g)).trans <| (TensorProduct.assoc ℝ _ _ _).trans <| (TensorProduct.congr (LinearEquiv.refl ℝ _) @@ -144,95 +139,5 @@ def decompEmbedProd (f : X' ↪ X) (g : Y' ↪ Y) : -/-- The contraction of all indices of two tensors with dual index-colors. - This is a bilinear map to ℝ. -/ -@[simps!] -def contrAll {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) : - ColorFiber d f1 →ₗ[ℝ] ColorFiber d f2 →ₗ[ℝ] ℝ where - toFun T := { - toFun := fun S => ∑ i, T i * S (indexValueDualIso d e hc i), - map_add' := fun S F => by - trans ∑ i, (T i * S (indexValueDualIso d e hc i) + T i * F (indexValueDualIso d e hc i)) - exact Finset.sum_congr rfl (fun i _ => mul_add _ _ _ ) - exact Finset.sum_add_distrib, - map_smul' := fun r S => by - trans ∑ i , r * (T i * S (indexValueDualIso d e hc i)) - refine Finset.sum_congr rfl (fun x _ => ?_) - ring_nf - rw [mul_assoc] - rfl - rw [← Finset.mul_sum] - rfl} - map_add' := fun T S => by - ext F - trans ∑ i , (T i * F (indexValueDualIso d e hc i) + S i * F (indexValueDualIso d e hc i)) - exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _) - exact Finset.sum_add_distrib - map_smul' := fun r T => by - ext S - trans ∑ i , r * (T i * S (indexValueDualIso d e hc i)) - refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _) - rw [← Finset.mul_sum] - rfl - -lemma contrAll_symm {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y) - (h : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) : - contrAll e h T S = contrAll e.symm (indexValueDualIso_cond_symm h) S T := by - rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d e h)] - refine Finset.sum_congr rfl (fun i _ => ?_) - rw [mul_comm, ← Equiv.trans_apply] - simp - -lemma contrAll_mapIsoFiber_right {f1 : X → Colors} {f2 : Y → Colors} - {g2 : Y' → Colors} (e : X ≃ Y) (eY : Y ≃ Y') - (h : f1 = τ ∘ f2 ∘ e) (hY : f2 = g2 ∘ eY) (T : ColorFiber d f1) (S : ColorFiber d f2) : - contrAll e h T S = contrAll (e.trans eY) (indexValueDualIso_cond_trans_indexValueIso h hY) - T (mapIsoFiber d eY hY S) := by - rw [contrAll_apply_apply, contrAll_apply_apply] - refine Finset.sum_congr rfl (fun i _ => Mathlib.Tactic.Ring.mul_congr rfl ?_ rfl) - rw [mapIsoFiber_apply, ← Equiv.trans_apply] - simp only [indexValueDualIso_trans_indexValueIso] - congr - ext1 x - simp only [Equiv.trans_apply, Equiv.symm_apply_apply] - -lemma contrAll_mapIsoFiber_left {f1 : X → Colors} {f2 : Y → Colors} - {g1 : X' → Colors} (e : X ≃ Y) (eX : X ≃ X') - (h : f1 = τ ∘ f2 ∘ e) (hX : f1 = g1 ∘ eX) (T : ColorFiber d f1) (S : ColorFiber d f2) : - contrAll e h T S = contrAll (eX.symm.trans e) - (indexValueIso_trans_indexValueDualIso_cond ((Equiv.eq_comp_symm eX g1 f1).mpr hX.symm) h) - (mapIsoFiber d eX hX T) S := by - rw [contrAll_symm, contrAll_mapIsoFiber_right _ eX _ hX, contrAll_symm] - rfl - -lemma contrAll_lorentzAction {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y) - (hc : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) (Λ : LorentzGroup d) : - contrAll e hc (lorentzActionFiber Λ T) (lorentzActionFiber Λ S) = contrAll e hc T S := by - change ∑ i, (∑ j, toTensorRepMat Λ i j * T j) * - (∑ k, toTensorRepMat Λ (indexValueDualIso d e hc i) k * S k) = _ - trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d e hc i) k * toTensorRepMat Λ i j) - * T j * S 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, ∑ i, (toTensorRepMat Λ (indexValueDualIso d e hc i) k - * toTensorRepMat Λ i j) * T j * S k - · apply Finset.sum_congr rfl (fun j _ => ?_) - rw [Finset.sum_comm] - trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j) * T j * S k - · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_)) - rw [← Finset.sum_mul, ← Finset.sum_mul] - erw [toTensorRepMat_indexValueDualIso_sum] - rw [Finset.sum_comm] - trans ∑ k, T (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) * S k - · apply Finset.sum_congr rfl (fun k _ => ?_) - rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum' T] - rw [← Equiv.sum_comp (indexValueDualIso d e hc), ← indexValueDualIso_symm e hc] - simp only [Equiv.symm_apply_apply, contrAll_apply_apply] - - end RealLorentzTensor end 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}",