From c9c7b25ea848defb63a724018534f55a311856df Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 24 Oct 2024 12:08:35 +0000 Subject: [PATCH] refactor: Lint --- HepLean.lean | 3 + HepLean/Tensors/ComplexLorentz/Basis.lean | 72 +- .../Tensors/ComplexLorentz/BasisTrees.lean | 233 ++++++ HepLean/Tensors/ComplexLorentz/Lemmas.lean | 679 +----------------- .../Tensors/ComplexLorentz/PauliContr.lean | 373 ++++++++++ .../Tensors/ComplexLorentz/PauliLower.lean | 257 +++++++ HepLean/Tensors/OverColor/Lift.lean | 9 +- HepLean/Tensors/Tree/Elab.lean | 2 +- .../Tensors/Tree/NodeIdentities/Basic.lean | 14 +- 9 files changed, 946 insertions(+), 696 deletions(-) create mode 100644 HepLean/Tensors/ComplexLorentz/BasisTrees.lean create mode 100644 HepLean/Tensors/ComplexLorentz/PauliContr.lean create mode 100644 HepLean/Tensors/ComplexLorentz/PauliLower.lean diff --git a/HepLean.lean b/HepLean.lean index ac4bf5c..4006143 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -109,7 +109,10 @@ import HepLean.StandardModel.HiggsBoson.Potential import HepLean.StandardModel.Representations import HepLean.Tensors.ComplexLorentz.Basic import HepLean.Tensors.ComplexLorentz.Basis +import HepLean.Tensors.ComplexLorentz.BasisTrees import HepLean.Tensors.ComplexLorentz.Lemmas +import HepLean.Tensors.ComplexLorentz.PauliContr +import HepLean.Tensors.ComplexLorentz.PauliLower import HepLean.Tensors.OverColor.Basic import HepLean.Tensors.OverColor.Discrete import HepLean.Tensors.OverColor.Functors diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean index 54ab11f..a3ff81c 100644 --- a/HepLean/Tensors/ComplexLorentz/Basis.lean +++ b/HepLean/Tensors/ComplexLorentz/Basis.lean @@ -79,6 +79,15 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply] rw [basis_eq_FDiscrete] +lemma perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C} + {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1) + (b : Π j, Fin (complexLorentzTensor.repDim (c j))) : + (perm σ (tensorNode (basisVector c b))).tensor = + (tensorNode (basisVector c1 (fun i => Fin.cast (perm_basisVector_cast σ i) + (b ((OverColor.Hom.toEquiv σ).symm i))))).tensor := by + exact perm_basisVector _ _ + +/-- The scalar determining if contracting two basis vectors together gives zero or not. -/ def contrBasisVectorMul {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} (i : Fin n.succ.succ) (j : Fin n.succ) (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : ℂ := @@ -89,7 +98,7 @@ lemma contrBasisVectorMul_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzT (h : ¬ (b i).val = (b (i.succAbove j)).val := by decide) : contrBasisVectorMul i j b = 0 := by rw [contrBasisVectorMul] - simp + simp only [ite_eq_else, one_ne_zero, imp_false] exact h lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} @@ -97,7 +106,7 @@ lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzT (h : (b i).val = (b (i.succAbove j)).val := by decide) : contrBasisVectorMul i j b = 1 := by rw [contrBasisVectorMul] - simp + simp only [ite_eq_then, zero_ne_one, imp_false, Decidable.not_not] exact h lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} @@ -119,37 +128,41 @@ lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor. erw [basis_contr] rfl -lemma contr_basisVector_tree {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} +lemma contr_basisVector_tree {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : (contr i j h (tensorNode (basisVector c b))).tensor = - (smul (contrBasisVectorMul i j b) (tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) - (fun k => b (i.succAbove (j.succAbove k)))) )).tensor := by + (smul (contrBasisVectorMul i j b) (tensorNode + (basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) + (fun k => b (i.succAbove (j.succAbove k)))))).tensor := by exact contr_basisVector _ -lemma contr_basisVector_tree_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} +lemma contr_basisVector_tree_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} - (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : (b i).val = (b (i.succAbove j)).val := by decide) : + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) + (hn : (b i).val = (b (i.succAbove j)).val := by decide) : (contr i j h (tensorNode (basisVector c b))).tensor = - ((tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) + ((tensorNode (basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j) (fun k => b (i.succAbove (j.succAbove k)))))).tensor := by rw [contr_basisVector_tree, contrBasisVectorMul] rw [if_pos hn] simp [smul_tensor] -lemma contr_basisVector_tree_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} +lemma contr_basisVector_tree_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} - (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : ¬ (b i).val = (b (i.succAbove j)).val := by decide) : + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) + (hn : ¬ (b i).val = (b (i.succAbove j)).val := by decide) : (contr i j h (tensorNode (basisVector c b))).tensor = (tensorNode 0).tensor := by rw [contr_basisVector_tree, contrBasisVectorMul] rw [if_neg hn] - simp [smul_tensor] - + simp only [Nat.succ_eq_add_one, smul_tensor, tensorNode_tensor, zero_smul] +/-- Equivalence of Fin types appearing in the product of two basis vectors. -/ def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (i : Fin n ⊕ Fin m) : - Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i => Fin (complexLorentzTensor.repDim (c1 i))) + Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i => + Fin (complexLorentzTensor.repDim (c1 i))) i ≃ Fin (complexLorentzTensor.repDim ((Sum.elim c c1 i))) := match i with | Sum.inl _ => Equiv.refl _ @@ -184,17 +197,17 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} | Sum.inl k => rfl | Sum.inr k => rfl -lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C} +lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (b1 : Π k, Fin (complexLorentzTensor.repDim (c1 k))) : - (prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor = + (prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor = (tensorNode (basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i => prodBasisVecEquiv (finSumFinEquiv.symm i) ((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by exact prod_basisVector _ _ -lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C} +lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C} {i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i))) (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : (eval i j (tensorNode (basisVector c b))).tensor = (if j = b i then (1 : ℂ) else 0) • @@ -282,7 +295,7 @@ lemma contrMatrix_basis_expand_tree : {Lorentz.contrMetric | μ ν}ᵀ.tensor = contrMatrix_basis_expand lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor = - - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1) + - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1) + basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor, Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue] @@ -299,7 +312,8 @@ lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor = · rfl lemma leftMetric_expand_tree : {Fermion.leftMetric | α β}ᵀ.tensor = - (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)))) <| + (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL] + (fun | 0 => 0 | 1 => 1)))) <| (tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0)))).tensor := leftMetric_expand @@ -320,8 +334,10 @@ lemma altLeftMetric_expand : {Fermion.altLeftMetric | α β}ᵀ.tensor = · rfl lemma altLeftMetric_expand_tree : {Fermion.altLeftMetric | α β}ᵀ.tensor = - (TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1))) <| - (smul (-1) (tensorNode (basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0))))).tensor := + (TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL] + (fun | 0 => 0 | 1 => 1))) <| + (smul (-1) (tensorNode (basisVector ![Color.downL, Color.downL] + (fun | 0 => 1 | 1 => 0))))).tensor := altLeftMetric_expand lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor = @@ -342,7 +358,8 @@ lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor = · rfl lemma rightMetric_expand_tree : {Fermion.rightMetric | α β}ᵀ.tensor = - (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)))) <| + (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR] + (fun | 0 => 0 | 1 => 1)))) <| (tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0)))).tensor := rightMetric_expand @@ -363,8 +380,10 @@ lemma altRightMetric_expand : {Fermion.altRightMetric | α β}ᵀ.tensor = · rfl lemma altRightMetric_expand_tree : {Fermion.altRightMetric | α β}ᵀ.tensor = - (TensorTree.add (tensorNode (basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <| - (smul (-1) (tensorNode (basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0))))).tensor := + (TensorTree.add (tensorNode (basisVector + ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <| + (smul (-1) (tensorNode (basisVector ![Color.downR, Color.downR] + (fun | 0 => 1 | 1 => 0))))).tensor := altRightMetric_expand /-- The expansion of the Pauli matrices `σ^μ^a^{dot a}` in terms of basis vectors. -/ @@ -406,13 +425,13 @@ lemma pauliMatrix_basis_expand : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor | (2 : Fin 3) => rfl lemma pauliMatrix_basis_expand_tree : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor = - (TensorTree.add (tensorNode + (TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0))) <| TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 1 | 2 => 1))) <| TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 0 | 2 => 1))) <| - TensorTree.add (tensorNode + TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 1 | 2 => 0))) <| TensorTree.add (smul (-I) (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <| @@ -421,7 +440,8 @@ lemma pauliMatrix_basis_expand_tree : {PauliMatrix.asConsTensor | μ α β}ᵀ.t TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 0 | 2 => 0))) <| (smul (-1) (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by + (basisVector ![Color.up, Color.upL, Color.upR] + (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by rw [pauliMatrix_basis_expand] simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor, smul_tensor, neg_smul, one_smul] diff --git a/HepLean/Tensors/ComplexLorentz/BasisTrees.lean b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean new file mode 100644 index 0000000..23ed781 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/BasisTrees.lean @@ -0,0 +1,233 @@ +/- +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.Tensors.Tree.Elab +import HepLean.Tensors.ComplexLorentz.Basic +import Mathlib.LinearAlgebra.TensorProduct.Basis +import HepLean.Tensors.Tree.NodeIdentities.Basic +import HepLean.Tensors.Tree.NodeIdentities.PermProd +import HepLean.Tensors.Tree.NodeIdentities.PermContr +import HepLean.Tensors.Tree.NodeIdentities.ProdComm +import HepLean.Tensors.Tree.NodeIdentities.ContrSwap +import HepLean.Tensors.Tree.NodeIdentities.ContrContr +import HepLean.Tensors.ComplexLorentz.Basis +/-! + +## Basis trees + +When contracting e.g. Pauli matrices with other tensors, it is sometimes convienent +to rewrite the contraction in terms of a basis. + +The lemmas in this file allow us to do this. +-/ +open IndexNotation +open CategoryTheory +open MonoidalCategory +open Matrix +open MatrixGroups +open Complex +open TensorProduct +open IndexNotation +open CategoryTheory +open TensorTree +open OverColor.Discrete + +noncomputable section + +namespace Fermion +open complexLorentzTensor + +/-! + +## Tree expansions for Pauli matrices. + +-/ + +/-- The map to colors one gets when contracting with Pauli matrices on the right. -/ +abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) := + (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) + +lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (t : TensorTree complexLorentzTensor c) : + (TensorTree.prod t (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor)).tensor = (((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add + (((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add + (((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add + (((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add + ((TensorTree.smul (-I) ((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add + ((TensorTree.smul I ((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add + ((t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0))).add + (TensorTree.smul (-1) (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] + fun | 0 => 3 | 1 => 1 | 2 => 1))))))))))).tensor := by + rw [prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree] + rw [prod_add _ _ _] + rw [add_tensor_eq_snd <| prod_add _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + prod_add _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] + /- Moving smuls. -/ + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd<| add_tensor_eq_snd + <| add_tensor_eq_snd <| prod_smul _ _ _] + rfl + +lemma contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (t : TensorTree complexLorentzTensor c) (i : Fin (n + 3)) (j : Fin (n +2)) + (h : (pauliMatrixContrMap c) (i.succAbove j) = + complexLorentzTensor.τ ((pauliMatrixContrMap c) i)) : + (contr i j h (TensorTree.prod t + (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor))).tensor = + ((contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add + ((contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add + ((contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add + ((contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add + ((TensorTree.smul (-I) (contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add + ((TensorTree.smul I (contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add + ((contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0)))).add + (TensorTree.smul (-1) (contr i j h (t.prod (tensorNode + (basisVector ![Color.up, Color.upL, Color.upR] + fun | 0 => 3 | 1 => 1 | 2 => 1)))))))))))).tensor := by + rw [contr_tensor_eq <| prod_pauliMatrix_basis_tree_expand _] + /- Moving contr over add. -/ + rw [contr_add] + rw [add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + /- Moving contr over smul. -/ + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + contr_smul _ _] + +lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (i : Fin (n + 3)) (j : Fin (n +2)) + (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ + ((pauliMatrixContrMap c) i)) + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : + let c' := Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm + let b' (i1 i2 i3 : Fin 4) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i) + ((HepLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3)) + (finSumFinEquiv.symm i)) + (contr i j h (TensorTree.prod (tensorNode (basisVector c b)) + (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor))).tensor = ((contr i j h ((tensorNode + (basisVector c' (b' 0 0 0))))).add + ((contr i j h ((tensorNode (basisVector c' (b' 0 1 1))))).add + ((contr i j h ((tensorNode (basisVector c' (b' 1 0 1))))).add + ((contr i j h ((tensorNode (basisVector c' (b' 1 1 0))))).add + ((TensorTree.smul (-I) (contr i j h ((tensorNode (basisVector c' (b' 2 0 1)))))).add + ((TensorTree.smul I (contr i j h ((tensorNode (basisVector c' (b' 2 1 0)))))).add + ((contr i j h ((tensorNode (basisVector c' (b' 3 0 0))))).add + (TensorTree.smul (-1) (contr i j h ((tensorNode + (basisVector c' (b' 3 1 1))))))))))))).tensor := by + rw [contr_pauliMatrix_basis_tree_expand] + /- Product of basis vectors . -/ + rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq + <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst + <| contr_tensor_eq <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq + <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq + <| prod_basisVector_tree _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq + <| contr_tensor_eq <| prod_basisVector_tree _ _] + rfl + +lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (i : Fin (n + 3)) (j : Fin (n +2)) + (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ + ((pauliMatrixContrMap c) i)) + (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : + let c' := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm) + ∘ Fin.succAbove i ∘ Fin.succAbove j + let b'' (i1 i2 i3 : Fin 4) : (i : Fin (n + (Nat.succ 0).succ.succ)) → + Fin (complexLorentzTensor.repDim (Sum.elim c ![Color.up, Color.upL, Color.upR] + (finSumFinEquiv.symm i))) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i) + ((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3)) + (finSumFinEquiv.symm i)) + let b' (i1 i2 i3 : Fin 4) := fun k => (b'' i1 i2 i3) (i.succAbove (j.succAbove k)) + (contr i j h (TensorTree.prod (tensorNode (basisVector c b)) + (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor))).tensor = ((( + TensorTree.smul (contrBasisVectorMul i j (b'' 0 0 0)) + (tensorNode (basisVector c' (b' 0 0 0))))).add + (((TensorTree.smul (contrBasisVectorMul i j (b'' 0 1 1)) + (tensorNode (basisVector c' (b' 0 1 1))))).add + (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 0 1)) + (tensorNode (basisVector c' (b' 1 0 1))))).add + (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 1 0)) + (tensorNode (basisVector c' (b' 1 1 0))))).add + ((TensorTree.smul (-I) ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 0 1)) + (tensorNode (basisVector c' (b' 2 0 1)))))).add + ((TensorTree.smul I ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 1 0)) + (tensorNode (basisVector c' (b' 2 1 0)))))).add + (((TensorTree.smul (contrBasisVectorMul i j (b'' 3 0 0)) + (tensorNode (basisVector c' (b' 3 0 0))))).add + (TensorTree.smul (-1) ((TensorTree.smul (contrBasisVectorMul i j (b'' 3 1 1)) (tensorNode + (basisVector c' (b' 3 1 1))))))))))))).tensor := by + rw [basis_contr_pauliMatrix_basis_tree_expand'] + /- Contracting basis vectors. -/ + rw [add_tensor_eq_fst <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst + <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_fst <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq + <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + smul_tensor_eq <| contr_basisVector_tree _] + +end Fermion + +end diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean index 1567bba..0f432d5 100644 --- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean +++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean @@ -3,17 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.Tensors.Tree.Elab -import HepLean.Tensors.ComplexLorentz.Basic -import Mathlib.LinearAlgebra.TensorProduct.Basis -import HepLean.Tensors.Tree.NodeIdentities.Basic -import HepLean.Tensors.Tree.NodeIdentities.PermProd -import HepLean.Tensors.Tree.NodeIdentities.PermContr -import HepLean.Tensors.Tree.NodeIdentities.ProdComm -import HepLean.Tensors.Tree.NodeIdentities.ContrSwap -import HepLean.Tensors.Tree.NodeIdentities.ContrContr -import HepLean.Tensors.ComplexLorentz.Basis -import LLMLean +import HepLean.Tensors.ComplexLorentz.BasisTrees /-! ## Lemmas related to complex Lorentz tensors. @@ -33,7 +23,7 @@ open OverColor.Discrete noncomputable section namespace Fermion - +open complexLorentzTensor set_option maxRecDepth 20000 in lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V} {T2 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V} : @@ -117,8 +107,8 @@ lemma antiSymm_add_self {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V} And related results. -/ -open complexLorentzTensor +/-- The map to color one gets when multiplying left and right metrics. -/ def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘ finSumFinEquiv.symm @@ -154,659 +144,20 @@ lemma leftMetric_mul_rightMetric : {Fermion.leftMetric | α α' ⊗ Fermion.righ funext x fin_cases x <;> rfl -def pauliMatrixLowerMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ - ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 1) - -abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) := - (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) - -lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} - (t : TensorTree complexLorentzTensor c) : - (TensorTree.prod t (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor)).tensor = (((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add - (((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add - (((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add - (((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add - ((TensorTree.smul (-I) ((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add - ((TensorTree.smul I ((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add - ((t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0))).add - (TensorTree.smul (-1) (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] - fun | 0 => 3 | 1 => 1 | 2 => 1))))))))))).tensor := by - rw [prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree] - rw [prod_add _ _ _] - rw [add_tensor_eq_snd <| prod_add _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - prod_add _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _] - /- Moving smuls. -/ - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd<| add_tensor_eq_snd - <| add_tensor_eq_snd <| prod_smul _ _ _] - rfl - -lemma contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} - (t : TensorTree complexLorentzTensor c) (i : Fin (n + 3)) (j : Fin (n +2)) - (h : (pauliMatrixContrMap c) (i.succAbove j) = - complexLorentzTensor.τ ((pauliMatrixContrMap c) i)) : - (contr i j h (TensorTree.prod t - (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor))).tensor = - ((contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add - ((contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add - ((contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add - ((contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add - ((TensorTree.smul (-I) (contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add - ((TensorTree.smul I (contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add - ((contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0)))).add - (TensorTree.smul (-1) (contr i j h (t.prod (tensorNode - (basisVector ![Color.up, Color.upL, Color.upR] - fun | 0 => 3 | 1 => 1 | 2 => 1)))))))))))).tensor := by - rw [contr_tensor_eq <| prod_pauliMatrix_basis_tree_expand _] - /- Moving contr over add. -/ - rw [contr_add] - rw [add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - /- Moving contr over smul. -/ - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - contr_smul _ _] - -lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C} - (i : Fin (n + 3)) (j : Fin (n +2)) - (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ - ((pauliMatrixContrMap c) i)) - (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : - let c' := Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm - let b' (i1 i2 i3 : Fin 4) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i) - ((HepLean.PiTensorProduct.elimPureTensor b (fun | 0 => i1 | 1 => i2 | 2 => i3)) - (finSumFinEquiv.symm i)) - (contr i j h (TensorTree.prod (tensorNode (basisVector c b)) - (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor))).tensor = ((contr i j h ((tensorNode - (basisVector c' (b' 0 0 0))))).add - ((contr i j h ((tensorNode (basisVector c' (b' 0 1 1))))).add - ((contr i j h ((tensorNode (basisVector c' (b' 1 0 1))))).add - ((contr i j h ((tensorNode (basisVector c' (b' 1 1 0))))).add - ((TensorTree.smul (-I) (contr i j h ((tensorNode (basisVector c' (b' 2 0 1)))))).add - ((TensorTree.smul I (contr i j h ((tensorNode (basisVector c' (b' 2 1 0)))))).add - ((contr i j h ((tensorNode (basisVector c' (b' 3 0 0))))).add - (TensorTree.smul (-1) (contr i j h ((tensorNode - (basisVector c' (b' 3 1 1))))))))))))).tensor := by - rw [contr_pauliMatrix_basis_tree_expand] - /- Product of basis vectors . -/ - rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq - <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst - <| contr_tensor_eq <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq - <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq - <| prod_basisVector_tree _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq - <| contr_tensor_eq <| prod_basisVector_tree _ _] - rfl - -lemma basis_contr_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C} - (i : Fin (n + 3)) (j : Fin (n +2)) - (h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ - ((pauliMatrixContrMap c) i)) - (b : Π k, Fin (complexLorentzTensor.repDim (c k))) : - let c' := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ finSumFinEquiv.symm) - ∘ Fin.succAbove i ∘ Fin.succAbove j - let b'' (i1 i2 i3 : Fin 4) : (i : Fin (n + (Nat.succ 0).succ.succ)) → - Fin (complexLorentzTensor.repDim (Sum.elim c ![Color.up, Color.upL, Color.upR] - (finSumFinEquiv.symm i))) := fun i => prodBasisVecEquiv (finSumFinEquiv.symm i) - ((HepLean.PiTensorProduct.elimPureTensor b (fun | (0 : Fin 3) => i1 | 1 => i2 | 2 => i3)) - (finSumFinEquiv.symm i)) - let b' (i1 i2 i3 : Fin 4) := fun k => (b'' i1 i2 i3) (i.succAbove (j.succAbove k)) - (contr i j h (TensorTree.prod (tensorNode (basisVector c b)) - (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor))).tensor = ((( - TensorTree.smul (contrBasisVectorMul i j (b'' 0 0 0)) - (tensorNode (basisVector c' (b' 0 0 0))))).add - (((TensorTree.smul (contrBasisVectorMul i j (b'' 0 1 1)) - (tensorNode (basisVector c' (b' 0 1 1))))).add - (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 0 1)) - (tensorNode (basisVector c' (b' 1 0 1))))).add - (((TensorTree.smul (contrBasisVectorMul i j (b'' 1 1 0)) - (tensorNode (basisVector c' (b' 1 1 0))))).add - ((TensorTree.smul (-I) ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 0 1)) - (tensorNode (basisVector c' (b' 2 0 1)))))).add - ((TensorTree.smul I ((TensorTree.smul (contrBasisVectorMul i j (b'' 2 1 0)) - (tensorNode (basisVector c' (b' 2 1 0)))))).add - (((TensorTree.smul (contrBasisVectorMul i j (b'' 3 0 0)) - (tensorNode (basisVector c' (b' 3 0 0))))).add - (TensorTree.smul (-1) ((TensorTree.smul (contrBasisVectorMul i j (b'' 3 1 1)) (tensorNode - (basisVector c' (b' 3 1 1))))))))))))).tensor := by - rw [basis_contr_pauliMatrix_basis_tree_expand'] - /- Contracting basis vectors. -/ - rw [add_tensor_eq_fst <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst - <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_fst <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq - <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - smul_tensor_eq <| contr_basisVector_tree _] - -lemma pauliMatrix_contr_down_0 : - (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod - (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor)))).tensor - = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0) - + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [one_smul, zero_smul, smul_zero, add_zero] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_down_0_tree : - (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod - (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR - PauliMatrix.asConsTensor)))).tensor +lemma leftMetric_mul_rightMetric_tree : + {Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ.tensor = (TensorTree.add (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) - (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)))).tensor := by - exact pauliMatrix_contr_down_0 - -lemma pauliMatrix_contr_down_1 : - {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1) - + basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_down_1_tree : - {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = (TensorTree.add (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1))) - (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))).tensor := by - exact pauliMatrix_contr_down_1 - -lemma pauliMatrix_contr_down_2 : - {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = (- I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1) - + (I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_down_2_tree : - {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor = - (TensorTree.add - (smul (- I) (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) - (smul I (tensorNode (basisVector - pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))))).tensor := by - exact pauliMatrix_contr_down_2 - -lemma pauliMatrix_contr_down_3 : - {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0) - + (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_down_3_tree : {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗ - PauliMatrix.asConsTensor | μ α β}ᵀ.tensor = - (TensorTree.add - ((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) - (smul (-1) (tensorNode (basisVector pauliMatrixLowerMap - (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by - exact pauliMatrix_contr_down_3 - -def pauliMatrixContrPauliMatrixMap := ((Sum.elim - ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ - Fin.succAbove 0 ∘ Fin.succAbove 1) ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ - Fin.succAbove 0 ∘ Fin.succAbove 2) - -lemma pauliMatrix_contr_lower_0_0_0 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_0_1_1 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_1_0_1 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_1_1_0 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_2_0_1 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - + (I) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_2_1_0 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) - + (I) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos, - contrBasisVectorMul_neg, contrBasisVectorMul_neg] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_3_0_0 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) - + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap - (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_3_1_1 : - {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗ - PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - + (-1 : ℂ) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by - rw [basis_contr_pauliMatrix_basis_tree_expand] - rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_neg, contrBasisVectorMul_neg, - contrBasisVectorMul_pos, contrBasisVectorMul_pos] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] - congr 1 - · congr 2 - funext k - fin_cases k <;> rfl - · congr 2 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_lower : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0) - + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) - - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1) - - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) - + I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1) - - I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) - - basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0) - + basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by - rw [contr_tensor_eq <| prod_tensor_eq_fst <| coMetric_basis_expand_tree] - /- Moving the prod through additions. -/ - rw [contr_tensor_eq <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] - /- Moving the prod through smuls. -/ - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst - <| smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd - <| smul_prod _ _ _] - /- Moving contraction through addition. -/ - rw [contr_add] - rw [add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - /- Moving contraction through smul. -/ - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_smul _ _] - /- Replacing the contractions. -/ - rw [add_tensor_eq_fst <| pauliMatrix_contr_down_0_tree] - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| pauliMatrix_contr_down_1_tree] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - pauliMatrix_contr_down_2_tree] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq <| - pauliMatrix_contr_down_3_tree] - /- Simplifying -/ - simp only [add_tensor, smul_tensor, tensorNode_tensor, smul_add,_root_.smul_smul] - simp only [Nat.reduceAdd, Fin.isValue, neg_smul, one_smul, mul_neg, neg_mul, one_mul, - _root_.neg_neg, mul_one] - rfl - -lemma pauliMatrix_lower_tree : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor - = (TensorTree.add (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <| - TensorTree.add (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))) <| - TensorTree.add (TensorTree.smul (-1) (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))) <| - TensorTree.add (TensorTree.smul (-1) (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))) <| - TensorTree.add (TensorTree.smul I (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <| - TensorTree.add (TensorTree.smul (-I) (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <| - TensorTree.add (TensorTree.smul (-1) (tensorNode - (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) <| - (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)))).tensor := by - rw [pauliMatrix_lower] - simp only [Nat.reduceAdd, Fin.isValue, add_tensor, - tensorNode_tensor, smul_tensor, neg_smul, one_smul] - rfl - -lemma pauliMatrix_contract_pauliMatrix_aux : - {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ - PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor - = ((tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)).add - ((tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1)).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul I (tensorNode - ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + - I • - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-I) (tensorNode - ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + - I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + - (-1 : ℂ) • - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1))).add + (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1))) <| + TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode + (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)))) <| + TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode + (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)))) <| (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + - (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap - fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by - rw [contr_tensor_eq <| prod_tensor_eq_fst <| pauliMatrix_lower_tree] - /- Moving the prod through additions. -/ - rw [contr_tensor_eq <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] - /- Moving the prod through smuls. -/ - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_fst <| smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] - rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - smul_prod _ _ _] - /- Moving contraction through addition. -/ - rw [contr_add] - rw [add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - /- Moving contraction through smul. -/ - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - /- Replacing the contractions. -/ - rw [add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_0_0_0] - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_0_1_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_0_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_1_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_2_0_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor - <| pauliMatrix_contr_lower_2_1_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_3_0_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_3_1_1] - -lemma pauliMatrix_contract_pauliMatrix : - {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ - PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor = - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) - + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) - - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) := by - rw [pauliMatrix_contract_pauliMatrix_aux] - simp only [Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, neg_smul, - one_smul, add_tensor, tensorNode_tensor, smul_tensor, smul_add, smul_neg, _root_.smul_smul, - neg_mul, _root_.neg_neg] - ring_nf - rw [Complex.I_sq] - simp only [neg_smul, one_smul, _root_.neg_neg] - abel + (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)))).tensor := by + rw [leftMetric_mul_rightMetric] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor, + smul_tensor, neg_smul, one_smul] + rfl end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/PauliContr.lean b/HepLean/Tensors/ComplexLorentz/PauliContr.lean new file mode 100644 index 0000000..4424299 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/PauliContr.lean @@ -0,0 +1,373 @@ +/- +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.Tensors.ComplexLorentz.PauliLower +import HepLean.Tensors.ComplexLorentz.Lemmas +/-! + +## Contractiong of indices of Pauli matrix. + +The main result of this file is `pauliMatrix_contract_pauliMatrix` which states that +`η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. + +The current way this result is proved is by using tensor tree manipulations. +There is likely a more direct path to this result. + +-/ +open IndexNotation +open CategoryTheory +open MonoidalCategory +open Matrix +open MatrixGroups +open Complex +open TensorProduct +open IndexNotation +open CategoryTheory +open TensorTree +open OverColor.Discrete +noncomputable section + +namespace Fermion +open complexLorentzTensor + +/-- The map to colors one gets when contracting the 4-vector indices pauli matrices. -/ +def pauliMatrixContrPauliMatrixMap := ((Sum.elim + ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ + Fin.succAbove 0 ∘ Fin.succAbove 1) ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ + Fin.succAbove 0 ∘ Fin.succAbove 2) + +lemma pauliMatrix_contr_lower_0_0_0 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_0_1_1 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_1_0_1 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_1_1_0 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_2_0_1 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + + (I) • + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_2_1_0 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + + (I) • + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_3_0_0 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap + (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_lower_3_1_1 : + {(basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗ + PauliMatrix.asConsTensor | μ α' β'}ᵀ.tensor = + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + + (-1 : ℂ) • + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +/-! TODO: Work out why `pauliMatrix_lower_basis_expand_prod'` is needed. -/ +/-- This lemma is exactly the same as `pauliMatrix_lower_basis_expand_prod'`. + It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why + `pauliMatrix_lower_basis_expand_prod` does not work. -/ +private lemma pauliMatrix_lower_basis_expand_prod' {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (t : TensorTree complexLorentzTensor c) : + (prod {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ t).tensor = + ((((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add + (((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add + ((TensorTree.smul I ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add + ((TensorTree.smul (-I) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add + ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod + t))))))))).tensor := by + exact pauliMatrix_lower_basis_expand_prod _ + +lemma pauliMatrix_contract_pauliMatrix_aux : + {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ + PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor + = ((tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)).add + ((tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1)).add + ((TensorTree.smul (-1) (tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add + ((TensorTree.smul (-1) (tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add + ((TensorTree.smul I (tensorNode + ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + + I • + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add + ((TensorTree.smul (-I) (tensorNode + ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + + I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add + ((TensorTree.smul (-1) (tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + + (-1 : ℂ) • + basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1))).add + (tensorNode + ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap + fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by + rw [contr_tensor_eq <| pauliMatrix_lower_basis_expand_prod' _] + /- Moving contraction through addition. -/ + rw [contr_add] + rw [add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + /- Moving contraction through smul. -/ + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| + contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + /- Replacing the contractions. -/ + rw [add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_0_0_0] + rw [add_tensor_eq_snd <| add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| + pauliMatrix_contr_lower_0_1_1] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| + eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_0_1] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| + smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_1_0] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| + pauliMatrix_contr_lower_2_0_1] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor + <| pauliMatrix_contr_lower_2_1_0] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| + eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_3_0_0] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| eq_tensorNode_of_eq_tensor <| + pauliMatrix_contr_lower_3_1_1] + +lemma pauliMatrix_contract_pauliMatrix_expand : + {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ + PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor = + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) + + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) + - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) := by + rw [pauliMatrix_contract_pauliMatrix_aux] + simp only [Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, neg_smul, + one_smul, add_tensor, tensorNode_tensor, smul_tensor, smul_add, smul_neg, _root_.smul_smul, + neg_mul, _root_.neg_neg] + ring_nf + rw [Complex.I_sq] + simp only [neg_smul, one_smul, _root_.neg_neg] + abel + +/-- The statement that `η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. -/ +theorem pauliMatrix_contract_pauliMatrix : + {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ + PauliMatrix.asConsTensor | ν α' β' = + 2 •ₜ Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ := by + rw [pauliMatrix_contract_pauliMatrix_expand] + rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_mul_rightMetric_tree] + rw [perm_smul] + /- Moving perm through adds. -/ + rw [smul_tensor_eq <| perm_add _ _ _] + rw [smul_tensor_eq <| add_tensor_eq_snd <| perm_add _ _ _] + rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| perm_add _ _ _] + /- Moving perm through smul. -/ + rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| perm_smul _ _ _] + rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd + <| add_tensor_eq_fst <| perm_smul _ _ _] + /- Perm acting on basis. -/ + erw [smul_tensor_eq <| add_tensor_eq_fst <| perm_basisVector_tree _ _] + erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| + perm_basisVector_tree _ _] + erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| + smul_tensor_eq <| perm_basisVector_tree _ _] + erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + perm_basisVector_tree _ _] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + have h1 (b0011 b1100 b0110 b1001 : CoeSort.coe (complexLorentzTensor.F.obj + (OverColor.mk pauliMatrixContrPauliMatrixMap))) : + ((2 • b0011 + 2 • b1100) - 2 • b0110 - 2 • b1001) = (2 : ℂ) • ((b0011) + + (((-1 : ℂ)• b0110) + (((-1 : ℂ) •b1001) + b1100))) := by + trans (2 : ℂ) • b0011 + (2 : ℂ) • b1100 - ((2 : ℂ) • b0110) - ((2 : ℂ) • b1001) + · repeat rw [two_smul] + · simp only [neg_smul, one_smul, smul_add, smul_neg] + abel + rw [h1] + congr + · funext i + fin_cases i <;> rfl + · funext i + fin_cases i <;> rfl + · funext i + fin_cases i <;> rfl + · funext i + fin_cases i <;> rfl + +end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/PauliLower.lean b/HepLean/Tensors/ComplexLorentz/PauliLower.lean new file mode 100644 index 0000000..f801f10 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/PauliLower.lean @@ -0,0 +1,257 @@ +/- +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.Tensors.ComplexLorentz.BasisTrees +/-! + +## Lowering indices of Pauli matrices. + +-/ +open IndexNotation +open CategoryTheory +open MonoidalCategory +open Matrix +open MatrixGroups +open Complex +open TensorProduct +open IndexNotation +open CategoryTheory +open TensorTree +open OverColor.Discrete +noncomputable section + +namespace Fermion +open complexLorentzTensor + +/-- The map to color one gets when lowering the indices of pauli matrices. -/ +def pauliMatrixLowerMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ + ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 1) + +lemma pauliMatrix_contr_down_0 : + (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod + (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor)))).tensor + = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0) + + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [one_smul, zero_smul, smul_zero, add_zero] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_down_0_tree : + (contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod + (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR + PauliMatrix.asConsTensor)))).tensor + = (TensorTree.add (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) + (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)))).tensor := by + exact pauliMatrix_contr_down_0 + +lemma pauliMatrix_contr_down_1 : + {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1) + + basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 1 + funext k + fin_cases k <;> rfl + · congr 1 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_down_1_tree : + {(basisVector ![Color.down, Color.down] fun x => 1) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = (TensorTree.add (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1))) + (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))).tensor := by + exact pauliMatrix_contr_down_1 + +lemma pauliMatrix_contr_down_2 : + {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = (- I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1) + + (I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos, + contrBasisVectorMul_neg, contrBasisVectorMul_neg] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_down_2_tree : + {(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor = + (TensorTree.add + (smul (- I) (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) + (smul I (tensorNode (basisVector + pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))))).tensor := by + exact pauliMatrix_contr_down_2 + +lemma pauliMatrix_contr_down_3 : + {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0) + + (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by + rw [basis_contr_pauliMatrix_basis_tree_expand] + rw [contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_neg, contrBasisVectorMul_neg, + contrBasisVectorMul_pos, contrBasisVectorMul_pos] + /- Simplifying. -/ + simp only [smul_tensor, add_tensor, tensorNode_tensor] + simp only [zero_smul, one_smul, smul_zero, add_zero, zero_add] + congr 1 + · congr 2 + funext k + fin_cases k <;> rfl + · congr 2 + funext k + fin_cases k <;> rfl + +lemma pauliMatrix_contr_down_3_tree : {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗ + PauliMatrix.asConsTensor | μ α β}ᵀ.tensor = + (TensorTree.add + ((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) + (smul (-1) (tensorNode (basisVector pauliMatrixLowerMap + (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by + exact pauliMatrix_contr_down_3 + +lemma pauliMatrix_lower : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0) + + basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) + - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1) + - basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) + + I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1) + - I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) + - basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0) + + basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by + rw [contr_tensor_eq <| prod_tensor_eq_fst <| coMetric_basis_expand_tree] + /- Moving the prod through additions. -/ + rw [contr_tensor_eq <| add_prod _ _ _] + rw [contr_tensor_eq <| add_tensor_eq_snd <| add_prod _ _ _] + rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] + /- Moving the prod through smuls. -/ + rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] + rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst + <| smul_prod _ _ _] + rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd + <| smul_prod _ _ _] + /- Moving contraction through addition. -/ + rw [contr_add] + rw [add_tensor_eq_snd <| contr_add _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] + /- Moving contraction through smul. -/ + rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_smul _ _] + /- Replacing the contractions. -/ + rw [add_tensor_eq_fst <| pauliMatrix_contr_down_0_tree] + rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| pauliMatrix_contr_down_1_tree] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| + pauliMatrix_contr_down_2_tree] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq <| + pauliMatrix_contr_down_3_tree] + /- Simplifying -/ + simp only [add_tensor, smul_tensor, tensorNode_tensor, smul_add,_root_.smul_smul] + simp only [Nat.reduceAdd, Fin.isValue, neg_smul, one_smul, mul_neg, neg_mul, one_mul, + _root_.neg_neg, mul_one] + rfl + +lemma pauliMatrix_lower_tree : {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor + = (TensorTree.add (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <| + TensorTree.add (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))) <| + TensorTree.add (TensorTree.smul (-1) (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))) <| + TensorTree.add (TensorTree.smul (-1) (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))) <| + TensorTree.add (TensorTree.smul I (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <| + TensorTree.add (TensorTree.smul (-I) (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <| + TensorTree.add (TensorTree.smul (-1) (tensorNode + (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) <| + (tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1)))).tensor := by + rw [pauliMatrix_lower] + simp only [Nat.reduceAdd, Fin.isValue, add_tensor, + tensorNode_tensor, smul_tensor, neg_smul, one_smul] + rfl + +lemma pauliMatrix_lower_basis_expand_prod {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (t : TensorTree complexLorentzTensor c) : + (prod {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ t).tensor = + (((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add + (((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add + ((TensorTree.smul I ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add + ((TensorTree.smul (-I) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add + ((TensorTree.smul (-1) ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add + ((tensorNode + (basisVector pauliMatrixLowerMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod + t)))))))).tensor := by + rw [prod_tensor_eq_fst <| pauliMatrix_lower_tree] + /- Moving the prod through additions. -/ + rw [add_prod _ _ _] + rw [add_tensor_eq_snd <| add_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_prod _ _ _] + /- Moving the prod through smuls. -/ + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| + smul_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_fst <| smul_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_prod _ _ _] + rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| + add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| + smul_prod _ _ _] + +end Fermion diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 50e78ec..a6921f0 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -208,7 +208,7 @@ def discreteSumEquiv {X Y : OverColor C} (i : X.left ⊕ Y.left) : | Sum.inr _ => LinearEquiv.refl _ _ /-- An equivalence used in the lemma of `μ_tmul_tprod_mk`. Identical to `μModEquiv` - except with arguments based on maps instead of elements of `OverColor C`. -/ + except with arguments based on maps instead of elements of `OverColor C`. -/ def discreteSumEquiv' {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) : Sum.elim (fun i => F.obj (Discrete.mk (cX i))) (fun i => F.obj (Discrete.mk (cY i))) i ≃ₗ[k] F.obj (Discrete.mk ((Sum.elim cX cY) i)) := @@ -280,9 +280,12 @@ lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C} let q' : (i : (OverColor.mk cY).left) → (F.obj <| Discrete.mk ((OverColor.mk cY).hom i)) := q let p' : (i : (OverColor.mk cX).left) → (F.obj <| Discrete.mk ((OverColor.mk cX).hom i)) := p have h1 := μModEquiv_tmul_tprod F p' q' - simp at h1 + simp only [Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + objObj'_V_carrier, mk_hom, Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom] at h1 erw [h1] - simp [p', q'] + simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left, + instMonoidalCategoryStruct_tensorObj_hom, mk_hom, p', q'] apply congrArg funext i match i with diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean index 51e8ad5..08b3e3f 100644 --- a/HepLean/Tensors/Tree/Elab.lean +++ b/HepLean/Tensors/Tree/Elab.lean @@ -250,7 +250,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do return f T | _ => match type with - | Expr.app _ (Expr.app _ (Expr.app _ c)) => + | Expr.app _ (Expr.app _ (Expr.app _ _)) => return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T] | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T] diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index a047b4c..dbe3ec7 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -125,7 +125,7 @@ These identities are related to the fact that all the maps are linear. lemma smul_smul (t : TensorTree S c) (a b : S.k) : (smul a (smul b t)).tensor = (smul (a * b) t).tensor := by - simp [smul_tensor] + simp only [smul_tensor] exact _root_.smul_smul a b t.tensor lemma smul_one (t : TensorTree S c) : @@ -150,11 +150,21 @@ lemma add_assoc (t1 t2 t3 : TensorTree S c) : /-- When the same permutation acts on both arguments of an addition, the permutation can be moved out of the addition. -/ -lemma add_perm {n : ℕ} {c : Fin n → S.C} {c1 : Fin n → S.C} +lemma add_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) : (add (perm σ t) (perm σ t1)).tensor = (perm σ (add t t1)).tensor := by simp only [add_tensor, perm_tensor, map_add] +lemma perm_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) : + (perm σ (add t t1)).tensor = (add (perm σ t) (perm σ t1)).tensor := by + simp only [add_tensor, perm_tensor, map_add] + +lemma perm_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (a : S.k) (t : TensorTree S c) : + (perm σ (smul a t)).tensor = (smul a (perm σ t)).tensor := by + simp only [smul_tensor, perm_tensor, map_smul] + /-- When the same evaluation acts on both arguments of an addition, the evaluation can be moved out of the addition. -/ lemma add_eval {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t t1 : TensorTree S c) :