refactor: Tensors

2025-02-04 14:17:09 +00:00 · 2025-02-04 14:17:09 +00:00 · a35a8b8884
commit a35a8b8884
parent 2a5193d5c9
5 changed files with 40 additions and 34 deletions
--- a/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean
@ -33,14 +33,15 @@ open Lorentz

 /-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
 def contrBispinorUp (p : complexContr) :=
-  {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor
+  {pauliCo | μ α β ⊗ (vecNodeE complexLorentzTensor .up p).tensor | μ}ᵀ.tensor

 /-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
 def contrBispinorDown (p : complexContr) :=
  {εL' | α α' ⊗ εR' | β β' ⊗ contrBispinorUp p | α β}ᵀ.tensor

 /-- A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`. -/
-def coBispinorUp (p : complexCo) := {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor
+def coBispinorUp (p : complexCo) :=
+  {pauliContr | μ α β ⊗ (vecNodeE complexLorentzTensor .down p).tensor | μ}ᵀ.tensor

 /-- A bispinor `pₐₐ` created from a lorentz vector `p_μ`. -/
 def coBispinorDown (p : complexCo) :=
@ -54,7 +55,8 @@ def coBispinorDown (p : complexCo) :=

 /-- The definitional tensor node relation for `contrBispinorUp`. -/
 lemma tensorNode_contrBispinorUp (p : complexContr) :
-    {contrBispinorUp p | α β}ᵀ.tensor = {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor := by
+    {contrBispinorUp p | α β}ᵀ.tensor = {pauliCo | μ α β ⊗
+      (vecNodeE complexLorentzTensor .up p).tensor  | μ}ᵀ.tensor := by
  rw [contrBispinorUp, tensorNode_tensor]

 /-- The definitional tensor node relation for `contrBispinorDown`. -/
@ -65,7 +67,8 @@ lemma tensorNode_contrBispinorDown (p : complexContr) :

 /-- The definitional tensor node relation for `coBispinorUp`. -/
 lemma tensorNode_coBispinorUp (p : complexCo) :
-    {coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor := by
+    {coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗
+    (vecNodeE complexLorentzTensor .down p).tensor | μ}ᵀ.tensor := by
  rw [coBispinorUp, tensorNode_tensor]

 /-- The definitional tensor node relation for `coBispinorDown`. -/
@ -97,20 +100,21 @@ informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where
 lemma contrBispinorDown_expand (p : complexContr) :
    {contrBispinorDown p | α β}ᵀ.tensor =
    {εL' | α α' ⊗ εR' | β β' ⊗
-    (pauliCo | μ α β ⊗ p | μ)}ᵀ.tensor := by
+    (pauliCo | μ α β ⊗ (vecNodeE complexLorentzTensor .up p).tensor | μ)}ᵀ.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 =
    {εL' | α α' ⊗ εR' | β β' ⊗
-    (pauliContr | μ α β ⊗ p | μ)}ᵀ.tensor := by
+    (pauliContr | μ α β ⊗ (vecNodeE complexLorentzTensor .down p).tensor | μ)}ᵀ.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 | μ α β ⊗
+    (vecNodeE complexLorentzTensor .up p).tensor | μ}ᵀ := by
  conv =>
    rhs
    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <|
@ -150,7 +154,8 @@ 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 | μ α β ⊗
+    (vecNodeE complexLorentzTensor .down p).tensor | μ}ᵀ := by
  conv =>
    rhs
    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <|
--- a/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Metrics/Basic.lean
@ -37,22 +37,27 @@ open Fermion
 -/

 /-- The metric `ηᵢᵢ` as a complex Lorentz tensor. -/
-def coMetric := {Lorentz.coMetric | μ ν}ᵀ.tensor
+def coMetric := (TensorTree.constTwoNodeE complexLorentzTensor .down .down Lorentz.coMetric).tensor

 /-- The metric `ηⁱⁱ` as a complex Lorentz tensor. -/
-def contrMetric := {Lorentz.contrMetric | μ ν}ᵀ.tensor
+def contrMetric := (TensorTree.constTwoNodeE complexLorentzTensor
+  .up .up Lorentz.contrMetric).tensor

 /-- The metric `εᵃᵃ` as a complex Lorentz tensor. -/
-def leftMetric := {Fermion.leftMetric | α α'}ᵀ.tensor
+def leftMetric := (TensorTree.constTwoNodeE complexLorentzTensor
+  .upL .upL Fermion.leftMetric).tensor

 /-- The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor. -/
-def rightMetric := {Fermion.rightMetric | β β'}ᵀ.tensor
+def rightMetric := (TensorTree.constTwoNodeE complexLorentzTensor
+  .upR .upR Fermion.rightMetric).tensor

 /-- The metric `εₐₐ` as a complex Lorentz tensor. -/
-def altLeftMetric := {Fermion.altLeftMetric | α α'}ᵀ.tensor
+def altLeftMetric := (TensorTree.constTwoNodeE complexLorentzTensor
+  .downL .downL Fermion.altLeftMetric).tensor

 /-- The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor. -/
-def altRightMetric := {Fermion.altRightMetric | β β'}ᵀ.tensor
+def altRightMetric := (TensorTree.constTwoNodeE complexLorentzTensor
+  .downR .downR Fermion.altRightMetric).tensor

 /-!

@ -85,29 +90,35 @@ scoped[complexLorentzTensor] notation "εR'" => altRightMetric
 -/

 /-- The definitional tensor node relation for `coMetric`. -/
-lemma tensorNode_coMetric : {η' | μ ν}ᵀ.tensor = {Lorentz.coMetric | μ ν}ᵀ.tensor := by
+lemma tensorNode_coMetric : {η' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
+    .down .down Lorentz.coMetric).tensor := by
  rfl

 /-- The definitional tensor node relation for `contrMetric`. -/
-lemma tensorNode_contrMetric : {η | μ ν}ᵀ.tensor = {Lorentz.contrMetric | μ ν}ᵀ.tensor := by
+lemma tensorNode_contrMetric : {η | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
+  .up .up Lorentz.contrMetric).tensor := by
  rfl

 /-- The definitional tensor node relation for `leftMetric`. -/
-lemma tensorNode_leftMetric : {εL | α α'}ᵀ.tensor = {Fermion.leftMetric | α α'}ᵀ.tensor := by
+lemma tensorNode_leftMetric : {εL | α α'}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
+  .upL .upL Fermion.leftMetric).tensor := by
  rfl

 /-- The definitional tensor node relation for `rightMetric`. -/
-lemma tensorNode_rightMetric : {εR | β β'}ᵀ.tensor = {Fermion.rightMetric | β β'}ᵀ.tensor := by
+lemma tensorNode_rightMetric : {εR | β β'}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
+  .upR .upR Fermion.rightMetric).tensor:= by
  rfl

 /-- The definitional tensor node relation for `altLeftMetric`. -/
 lemma tensorNode_altLeftMetric :
-    {εL' | α α'}ᵀ.tensor = {Fermion.altLeftMetric | α α'}ᵀ.tensor := by
+    {εL' | α α'}ᵀ.tensor =  (TensorTree.constTwoNodeE complexLorentzTensor
+  .downL .downL Fermion.altLeftMetric).tensor := by
  rfl

 /-- The definitional tensor node relation for `altRightMetric`. -/
 lemma tensorNode_altRightMetric :
-    {εR' | β β'}ᵀ.tensor = {Fermion.altRightMetric | β β'}ᵀ.tensor := by
+    {εR' | β β'}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
+  .downR .downR Fermion.altRightMetric).tensor:= by
  rfl

 /-!
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean
@ -32,7 +32,8 @@ open Fermion
 -/

 /-- The Pauli matrices as the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
-def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
+def pauliContr := (TensorTree.constThreeNodeE complexLorentzTensor .up .upL .upR
+  PauliMatrix.asConsTensor).tensor

 /-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/
 def pauliCo := {η' | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor
@ -51,7 +52,8 @@ def pauliContrDown := {pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'

 /-- The definitional tensor node relation for `pauliContr`. -/
 lemma tensorNode_pauliContr : {pauliContr | μ α β}ᵀ.tensor =
-    {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by
+    (TensorTree.constThreeNodeE complexLorentzTensor .up .upL .upR
+  PauliMatrix.asConsTensor).tensor := by
  rfl

 /-- The definitional tensor node relation for `pauliCo`. -/
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexTensor.PauliMatrices.Basis
-import HepLean.Lorentz.ComplexTensor.Lemmas
 /-!

 ## Contractiong of indices of Pauli matrix.
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@ -279,17 +279,6 @@ def specialTypes : List (String × (Term → Term)) := [
 def termNodeSyntax (T : Term) : TermElabM Term := do
  let expr ← elabTerm T none
  let type ← inferType expr
-  let defEqList ← specialTypes.filterM (fun x => do
-    let type' ← stringToType x.1
-    match type' with
-    | none => return false
-    | some type' =>
-    let defEq ← isDefEq type type'
-    return defEq)
-  match defEqList with
-  | [(_, f)] =>
-    return f T
-  | _ =>
  match type with
  | Expr.app _ (Expr.app _ (Expr.app _ _)) =>
      return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]