From 7010a1dae229d26e0e07bd4a5708bf803cd7fd13 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 29 Oct 2024 11:23:08 +0000 Subject: [PATCH] refactor: Text based Lint --- HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 4 +-- .../MSSMNu/OrthogY3B3/PlaneWithY3B3.lean | 4 +-- .../MSSMNu/OrthogY3B3/ToSols.lean | 4 +-- .../PureU1/Permutations.lean | 4 +-- HepLean/Tensors/ComplexLorentz/Basic.lean | 5 ++- .../ComplexLorentz/Bispinors/Basic.lean | 34 ++++++++++++------- .../ComplexLorentz/PauliMatrices/Basic.lean | 8 ++--- .../ComplexLorentz/PauliMatrices/Basis.lean | 4 --- .../Tensors/Tree/NodeIdentities/Basic.lean | 10 +++--- .../Tensors/Tree/NodeIdentities/Congr.lean | 11 +++--- .../Tree/NodeIdentities/ContrContr.lean | 14 ++++---- .../Tree/NodeIdentities/PermContr.lean | 4 +-- 12 files changed, 54 insertions(+), 52 deletions(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean index d62af84..de29231 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -275,8 +275,8 @@ lemma accYY_ext {S T : MSSMCharges.Charges} /-- The symmetric bilinear function used to define the quadratic ACC. -/ @[simps!] -def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ ( - fun (S, T) => ∑ i, (Q S i * Q T i + (- 2) * (U S i * U T i) + +def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ + (fun (S, T) => ∑ i, (Q S i * Q T i + (- 2) * (U S i * U T i) + D S i * D T i + (- 1) * (L S i * L T i) + E S i * E T i) + (- Hd S * Hd T + Hu S * Hu T)) (by diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean index c4fbd45..c893886 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean @@ -206,8 +206,8 @@ lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : section proj lemma α₃_proj (T : MSSMACC.Sols) : α₃ (proj T.1.1) = - 6 * dot Y₃.val B₃.val ^ 3 * ( - cubeTriLin T.val T.val Y₃.val * quadBiLin B₃.val T.val - + 6 * dot Y₃.val B₃.val ^ 3 * + (cubeTriLin T.val T.val Y₃.val * quadBiLin B₃.val T.val - cubeTriLin T.val T.val B₃.val * quadBiLin Y₃.val T.val) := by rw [α₃] rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, quad_B₃_proj, quad_Y₃_proj] diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean index af068c9..877cbe2 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean @@ -253,8 +253,8 @@ def inLineEqProj (T : InLineEqSol) : InLineEq × ℚ × ℚ × ℚ := (⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩, (quadCoeff T.val)⁻¹ * quadBiLin B₃.val T.val.val, (quadCoeff T.val)⁻¹ * (- quadBiLin Y₃.val T.val.val), - (quadCoeff T.val)⁻¹ * ( - quadBiLin B₃.val T.val.val * (dot B₃.val T.val.val - dot Y₃.val T.val.val) + (quadCoeff T.val)⁻¹ * + (quadBiLin B₃.val T.val.val * (dot B₃.val T.val.val - dot Y₃.val T.val.val) - quadBiLin Y₃.val T.val.val * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val))) lemma inLineEqTo_smul (R : InLineEq) (c₁ c₂ c₃ d : ℚ) : diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean index 4a375d6..7341358 100644 --- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean +++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean @@ -307,8 +307,8 @@ lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} {a b c : Fin n} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (h : ∀ (f : (FamilyPermutations n).group), - P ((((FamilyPermutations n).linSolRep f S).val a),( - (((FamilyPermutations n).linSolRep f S).val b), + P ((((FamilyPermutations n).linSolRep f S).val a), + ((((FamilyPermutations n).linSolRep f S).val b), (((FamilyPermutations n).linSolRep f S).val c)))) : ∀ (i j k : Fin n) (_ : i ≠ j) (_ : j ≠ k) (_ : i ≠ k), P (S.val i, (S.val j, S.val k)) := by intro i j k hij hjk hik diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean index 13d7b4d..dc0db4d 100644 --- a/HepLean/Tensors/ComplexLorentz/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Basic.lean @@ -209,10 +209,10 @@ 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} : +instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : DecidableEq (OverColor.mk c).left := instDecidableEqFin n -instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : +instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : Fintype (OverColor.mk c).left := Fin.fintype n instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C} @@ -220,6 +220,5 @@ instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C} 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 d0267f5..395cda4 100644 --- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean @@ -76,7 +76,7 @@ lemma tensorNode_contrBispinorDown (p : complexContr) : rw [contrBispinorDown, tensorNode_tensor] /-- The definitional tensor node relation for `coBispinorUp`. -/ -lemma tensorNode_coBispinorUp (p : complexCo) : +lemma tensorNode_coBispinorUp (p : complexCo) : {coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor := by rw [coBispinorUp, tensorNode_tensor] @@ -94,23 +94,26 @@ lemma tensorNode_coBispinorDown (p : complexCo) : -/ lemma contrBispinorDown_expand (p : complexContr) : - {contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗ + {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] lemma coBispinorDown_expand (p : complexCo) : - {coBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗ + {coBispinorDown p | α β}ᵀ.tensor = + {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗ (pauliContr | μ α β ⊗ p | μ)}ᵀ.tensor := by rw [tensorNode_coBispinorDown p] rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_coBispinorUp p] set_option maxRecDepth 5000 in lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) : - {contrBispinorDown p | α β = pauliCoDown | μ α β ⊗ p | μ}ᵀ := by + {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_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] @@ -118,12 +121,14 @@ lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) : 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 <| 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' _ _ _ _ _ _] + 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] @@ -144,10 +149,11 @@ lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) : set_option maxRecDepth 5000 in lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) : - {coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀ := by + {coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀs := by conv => rhs - rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| pauliContrDown_eq_metric_mul_pauliContr] + rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| + pauliContrDown_eq_metric_mul_pauliContr] rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _] rw [perm_tensor_eq <| perm_contr_congr 2 2] rw [perm_perm] @@ -155,12 +161,14 @@ lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) : 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 <| 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' _ _ _ _ _ _] + 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] diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean index 0cb3884..bc48973 100644 --- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean @@ -63,7 +63,7 @@ lemma tensorNode_pauliContr : {pauliContr | μ α β}ᵀ.tensor = rfl /-- The definitional tensor node relation for `pauliCo`. -/ -lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor = +lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor = {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by rfl @@ -111,7 +111,7 @@ lemma pauliCoDown_eq_metric_mul_pauliCo : 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 <| 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 _ _ _] @@ -138,7 +138,7 @@ lemma pauliCoDown_eq_metric_mul_pauliCo : set_option maxRecDepth 5000 in /-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/ lemma pauliContrDown_eq_metric_mul_pauliContr : - {pauliContrDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗ + {pauliContrDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ := by conv => lhs @@ -161,7 +161,7 @@ lemma pauliContrDown_eq_metric_mul_pauliContr : 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 <| 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 _ _ _] diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean index 1a99723..59f5cda 100644 --- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean +++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean @@ -26,7 +26,6 @@ noncomputable section namespace complexLorentzTensor open Fermion - /-! ## Expanding pauliContr in a basis. @@ -94,7 +93,6 @@ lemma pauliContr_basis_expand_tree : {pauliContr | μ α β}ᵀ.tensor = smul_tensor, neg_smul, one_smul] rfl - /-- 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) @@ -325,14 +323,12 @@ lemma basis_contr_pauliMatrix_basis_tree_expand_tensor {n : ℕ} {c : Fin n → simp_all only [Function.comp_apply, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue] rfl - /-! ## Expanding pauliCo in a basis. -/ - /-- The map to color one gets when lowering the indices of pauli matrices. -/ def pauliCoMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index 6b0c847..ea19d5f 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -116,15 +116,16 @@ lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} simp only [Iso.map_hom_inv_id, Action.id_hom, ModuleCat.id_apply] lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} - (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) + (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) {t : TensorTree S c} {t2 : TensorTree S c1} : (perm σ t).tensor = t2.tensor ↔ t.tensor = (perm (equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x)) t2).tensor := by - refine Iff.intro (fun h => ?_) (fun h => ?_) + refine Iff.intro (fun h => ?_) (fun h => ?_) · simp [perm_tensor, ← h] change _ = (S.F.map _ ≫ S.F.map _).hom _ rw [← S.F.map_comp] - have h1 : (σ ≫ equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x)) = 𝟙 _ := by + have h1 : (σ ≫ equivToHomEq (Hom.toEquiv σ).symm + (fun x => Hom.toEquiv_comp_apply σ x)) = 𝟙 _ := by apply Hom.ext ext x change (Hom.toEquiv σ).symm ((Hom.toEquiv σ) x) = x @@ -134,7 +135,8 @@ lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} · rw [perm_tensor, h] change (S.F.map _ ≫ S.F.map _).hom _ = _ rw [← S.F.map_comp] - have h1 : (equivToHomEq (Hom.toEquiv σ).symm (fun x => Hom.toEquiv_comp_apply σ x) ≫ σ) = 𝟙 _ := by + have h1 : (equivToHomEq (Hom.toEquiv σ).symm + (fun x => Hom.toEquiv_comp_apply σ x) ≫ σ) = 𝟙 _ := by apply Hom.ext ext x change (Hom.toEquiv σ) ((Hom.toEquiv σ).symm x) = x diff --git a/HepLean/Tensors/Tree/NodeIdentities/Congr.lean b/HepLean/Tensors/Tree/NodeIdentities/Congr.lean index cfccdf5..20996d7 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Congr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Congr.lean @@ -30,21 +30,20 @@ variable {n m : ℕ} lemma perm_congr {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T T' : TensorTree S c1} {σ σ' : OverColor.mk c1 ⟶ OverColor.mk c2} - (h : σ = σ') (hT : T.tensor = T'.tensor): + (h : σ = σ') (hT : T.tensor = T'.tensor) : (perm σ T).tensor = (perm σ' T').tensor := by rw [h] simp only [perm_tensor, hT] -lemma perm_update {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T : TensorTree S c1} +lemma perm_update {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T : TensorTree S c1} {σ : OverColor.mk c1 ⟶ OverColor.mk c2} (σ' : OverColor.mk c1 ⟶ OverColor.mk c2) (h : σ = σ') : (perm σ T).tensor = (perm σ' T).tensor := by rw [h] lemma contr_congr {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} - (i' : Fin n.succ.succ) {j : Fin n.succ} (j' : Fin n.succ) - {h : c (i.succAbove j) = S.τ (c i)} {t : TensorTree S c} - (hi : i = i' := by decide) (hj : j = j' := by decide) - :(contr i j h t).tensor = + (i' : Fin n.succ.succ) {j : Fin n.succ} (j' : Fin n.succ){h : c (i.succAbove j) = S.τ (c i)} + {t : TensorTree S c} (hi : i = i' := by decide) (hj : j = j' := by decide) : + (contr i j h t).tensor = (perm (mkIso (by rw [hi, hj])).hom (contr i' j' (by rw [← hi, ← hj, h]) t)).tensor := by subst hi subst hj diff --git a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean index 8420180..acd10cf 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean @@ -285,15 +285,13 @@ def contrContrPerm {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n. {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) ∘ + 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 + (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} diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean index 7b14161..a757c3f 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean @@ -264,8 +264,8 @@ lemma perm_contr_congr_mkIso_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {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 + 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}