From 47564660013ecb77c87b39d915bf7326cad78f6f Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 29 Oct 2024 10:37:18 +0000 Subject: [PATCH] feat: Important fix to ContrContr --- HepLean/Tensors/ComplexLorentz/Basic.lean | 12 ++++ .../ComplexLorentz/Bispinors/Basic.lean | 52 ++++++++++++++++ .../ComplexLorentz/PauliMatrices/Basic.lean | 61 +++++++++++++++++++ HepLean/Tensors/OverColor/Basic.lean | 7 +++ .../Tensors/Tree/NodeIdentities/Basic.lean | 2 +- .../Tree/NodeIdentities/ContrContr.lean | 16 ++++- .../Tree/NodeIdentities/PermContr.lean | 36 +++++++++++ 7 files changed, 184 insertions(+), 2 deletions(-) diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean index 484bf44..13d7b4d 100644 --- a/HepLean/Tensors/ComplexLorentz/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Basic.lean @@ -209,5 +209,17 @@ lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.re | Color.up => Lorentz.contrCoContraction_basis _ _ | Color.down => Lorentz.coContrContraction_basis _ _ +instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : + DecidableEq (OverColor.mk c).left := instDecidableEqFin n + +instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : + Fintype (OverColor.mk c).left := Fin.fintype n + +instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C} + {c1 : Fin m → complexLorentzTensor.C} (σ σ' : OverColor.mk c ⟶ OverColor.mk c1) : + Decidable (σ = σ') := + decidable_of_iff _ (OverColor.Hom.ext_iff σ σ') + + end complexLorentzTensor end diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean index 4f5e33a..83e1fd5 100644 --- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean @@ -87,5 +87,57 @@ lemma tensorNode_coBispinorDown (p : complexCo) : ⊗ coBispinorUp p | α β}ᵀ.tensor := by rw [coBispinorDown, tensorNode_tensor] +/-! + +## Basic equalities. + +-/ + +lemma contrBispinorDown_expand (p : complexContr) : + {contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗ + (pauliCo | μ α β ⊗ p | μ)}ᵀ.tensor := by + rw [tensorNode_contrBispinorDown p] + rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_contrBispinorUp p] + +set_option maxRecDepth 5000 in +lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) : + {contrBispinorDown p | α β = pauliCoDown | μ α β ⊗ p | μ}ᵀ := by + conv => + rhs + rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| pauliCoDown_eq_metric_mul_pauliCo] + rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _] + rw [perm_tensor_eq <| perm_contr_congr 2 2] + rw [perm_perm] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _] + rw [perm_tensor_eq <| perm_contr_congr 2 2] + rw [perm_perm] + apply (perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _).trans + rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3] + rw [perm_tensor_eq <| perm_contr_congr 2 2] + rw [perm_perm] + erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_contr_congr 0 4] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3] + rw [perm_tensor_eq <| perm_contr_congr 2 2] + rw [perm_perm] + conv => + lhs + rw [contrBispinorDown_expand p] + rw [contr_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _] + rw [contr_tensor_eq <| perm_contr_congr 0 3] + rw [perm_contr_congr 1 2] + apply (perm_tensor_eq <| contr_tensor_eq <| contr_contr _ _ _).trans + rw [perm_tensor_eq <| perm_contr _ _] + rw [perm_perm] + rw [perm_tensor_eq <| contr_contr _ _ _] + rw [perm_perm] + apply perm_congr _ rfl + decide + + + + end complexLorentzTensor end diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean index ed06882..fdc35eb 100644 --- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc +import HepLean.Tensors.Tree.NodeIdentities.ProdComm import HepLean.Tensors.Tree.NodeIdentities.ProdContr +import HepLean.Tensors.Tree.NodeIdentities.ContrContr +import HepLean.Tensors.Tree.NodeIdentities.ContrSwap +import HepLean.Tensors.Tree.NodeIdentities.PermContr import HepLean.Tensors.Tree.NodeIdentities.Congr /-! @@ -75,4 +79,61 @@ lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor = Fermion.altRightMetric | β β'}ᵀ.tensor := by rfl +/-! + +## Basic equalities + +-/ + +set_option maxRecDepth 5000 in +/-- A rearanging of `pauliCoDown` to place the pauli matrices on the right. -/ +lemma pauliCoDown_eq_metric_mul_pauliCo : + {pauliCoDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗ + Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ := by + conv => + lhs + rw [tensorNode_pauliCoDown] + rw [contr_tensor_eq <| contr_prod _ _ _] + rw [perm_contr] + erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _] + rw [perm_tensor_eq <| contr_congr 1 2] + rw [perm_perm] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_congr 1 2] + rw [perm_tensor_eq <| perm_contr _ _] + rw [perm_perm] + rw [perm_tensor_eq <| contr_congr 1 2] + rw [perm_perm] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 1 2] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _] + rw [perm_tensor_eq <| perm_contr _ _] + rw [perm_perm] + rw [perm_tensor_eq <| contr_congr 1 2] + rw [perm_perm] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_comm _ _ _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _] + rw [perm_tensor_eq <| perm_contr _ _] + rw [perm_perm] + rw [perm_tensor_eq <| contr_congr 4 1] + rw [perm_perm] + conv => + rhs + rw [perm_tensor_eq <| contr_swap _ _] + rw [perm_perm] + erw [perm_tensor_eq <| contr_congr 4 1] + rw [perm_perm] + rw [perm_tensor_eq <| contr_tensor_eq <| contr_swap _ _] + erw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0] + rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _] + rw [perm_tensor_eq <| perm_contr _ _] + rw [perm_perm] + rw [perm_tensor_eq <| contr_congr 4 1] + rw [perm_perm] + apply perm_congr _ rfl + decide + + end complexLorentzTensor diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean index b7a2549..33e8de5 100644 --- a/HepLean/Tensors/OverColor/Basic.lean +++ b/HepLean/Tensors/OverColor/Basic.lean @@ -45,6 +45,13 @@ variable {C : Type} {f g h : OverColor C} lemma ext (m n : f ⟶ g) (h : m.hom = n.hom) : m = n := by apply CategoryTheory.Iso.ext h +lemma ext_iff (m n : f ⟶ g) : (∀ x, m.hom.left x = n.hom.left x) ↔ m = n := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · apply ext + ext x + exact h x + · rw [h] + exact fun x => rfl /-- Given a hom in `OverColor C` the underlying equivalence between types. -/ def toEquiv (m : f ⟶ g) : f.left ≃ g.left where diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index 35fdc31..6b0c847 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -92,7 +92,7 @@ lemma add_neg (t : TensorTree S c) : (add t (neg t)).tensor = 0 := by -/ /-- Applying two permutations is the same as applying the transitive permutation. -/ -lemma perm_perm {n : ℕ} {c : Fin n → S.C} {c1 : Fin n → S.C} {c2 : Fin n → S.C} +lemma perm_perm {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.C} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (σ2 : (OverColor.mk c1) ⟶ (OverColor.mk c2)) (t : TensorTree S c) : (perm σ2 (perm σ t)).tensor = (perm (σ ≫ σ2) t).tensor := by simp [perm_tensor] diff --git a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean index 4c55f86..8420180 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean @@ -281,6 +281,20 @@ lemma contr_contr (t : TensorTree S c) : end end ContrQuartet +def contrContrPerm {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ} + {j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ} + (hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) = + S.τ ((c ∘ i.succAbove ∘ j.succAbove) k)) : + OverColor.mk + ((c ∘ + (ContrQuartet.mk i j k l hij hkl).swapI.succAbove ∘ + (ContrQuartet.mk i j k l hij hkl).swapJ.succAbove) ∘ + (ContrQuartet.mk i j k l hij hkl).swapK.succAbove ∘ + (ContrQuartet.mk i j k l hij hkl).swapL.succAbove) ⟶ + OverColor.mk + ((c ∘ i.succAbove ∘ j.succAbove) ∘ k.succAbove ∘ l.succAbove) + := (ContrQuartet.mk i j k l hij hkl).contrSwapHom + /-- Contraction nodes commute on adjusting indices. -/ theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ} {j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ} @@ -288,7 +302,7 @@ theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n S.τ ((c ∘ i.succAbove ∘ j.succAbove) k)) (t : TensorTree S c) : (contr k l hkl (contr i j hij t)).tensor = - (perm (ContrQuartet.mk i j k l hij hkl).contrSwapHom + (perm (contrContrPerm hij hkl) (contr (ContrQuartet.mk i j k l hij hkl).swapK (ContrQuartet.mk i j k l hij hkl).swapL (ContrQuartet.mk i j k l hij hkl).swap.hkl (contr (ContrQuartet.mk i j k l hij hkl).swapI (ContrQuartet.mk i j k l hij hkl).swapJ diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean index 4efa9f2..7b14161 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Tensors.Tree.Basic +import HepLean.Tensors.Tree.NodeIdentities.Congr +import HepLean.Tensors.Tree.NodeIdentities.Basic /-! # The commutativity of Permutations and contractions. @@ -256,4 +258,38 @@ lemma perm_contr {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ rw [S.contrMap_naturality σ] rfl +lemma perm_contr_congr_mkIso_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C} + {i : Fin n.succ.succ} {j : Fin n.succ} + {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} + {i' : Fin n.succ.succ} {j' : Fin n.succ} + (hi : i' = ((Hom.toEquiv σ).symm i)) + (hj : j' = (((Hom.toEquiv (extractOne i σ))).symm j)) : + c ∘ i'.succAbove ∘ j'.succAbove = + c ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘ Fin.succAbove ((Hom.toEquiv (extractOne i σ)).symm j) := by + rw [hi, hj] + +lemma perm_contr_congr_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C} + {i : Fin n.succ.succ} {j : Fin n.succ} + (h : c1 (i.succAbove j) = S.τ (c1 i)) + {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} + {i' : Fin n.succ.succ} {j' : Fin n.succ} + (hi : i' = ((Hom.toEquiv σ).symm i)) + (hj : j' = (((Hom.toEquiv (extractOne i σ))).symm j)) : + c (i'.succAbove j') = S.τ (c i') := by + rw [hi, hj] + exact S.perm_contr_cond h σ + +lemma perm_contr_congr {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C} + {i : Fin n.succ.succ} {j : Fin n.succ} + {h : c1 (i.succAbove j) = S.τ (c1 i)} {t : TensorTree S c} + {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} + (i' : Fin n.succ.succ) (j' : Fin n.succ) + (hi : i' = ((Hom.toEquiv σ).symm i) := by decide) + (hj : j' = (((Hom.toEquiv (extractOne i σ))).symm j) := by decide) : + (contr i j h (perm σ t)).tensor = (perm ((mkIso (perm_contr_congr_mkIso_cond hi hj)).hom ≫ + extractTwo i j σ) (contr i' j' (perm_contr_congr_contr_cond h hi hj) t)).tensor := by + rw [perm_contr] + rw [perm_tensor_eq <| contr_congr i' j' hi.symm hj.symm] + rw [perm_perm] + end TensorTree