/-
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.NodeIdentities.ProdAssoc
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
import HepLean.Tensors.Tree.NodeIdentities.Congr
/-!

## Pauli matrices as complex Lorentz tensors

-/
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 complexLorentzTensor
open Fermion

/-!

## Definitions.

-/

/- The Pauli matrices as `σ^μ^α^{dot β}`. -/
def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor

/-- The Pauli matrices as `σ_μ^α^{dot β}`. -/
def pauliCo := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor

/-- The Pauli matrices as `σ_μ_α_{dot β}`. -/
def pauliCoDown := {Fermion.altLeftMetric | α α' ⊗
  Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor

/-- The Pauli matrices as `σ^μ_α_{dot β}`. -/
def pauliContrDown := {Fermion.altLeftMetric | α α' ⊗
  Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor

/-!

## Tensor nodes.

-/

/-- The definitional tensor node relation for `pauliContr`. -/
lemma tensorNode_pauliContr : {pauliContr | μ α β}ᵀ.tensor =
    {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by
  rfl

/-- The definitional tensor node relation for `pauliCo`. -/
lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor  =
    {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by
  rfl

/-- The definitional tensor node relation for `pauliCoDown`. -/
lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor =
    {Fermion.altLeftMetric | α α' ⊗
    Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor := by
  rfl

/-- The definitional tensor node relation for `pauliContrDown`. -/
lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
    {Fermion.altLeftMetric | α α' ⊗
    Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor := by
  rfl

end complexLorentzTensor