refactor: Move ComplexTensor
This commit is contained in:
jstoobysmith
parent
78c0046c49
commit
a7142ef99b
14 changed files with 29 additions and 29 deletions
|
|
@ -1,224 +0,0 @@
|
|||
/-
|
||||
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.OverColor.Basic
|
||||
import HepLean.Tensors.Tree.Dot
|
||||
import HepLean.Lorentz.Weyl.Contraction
|
||||
import HepLean.Lorentz.Weyl.Metric
|
||||
import HepLean.Lorentz.Weyl.Unit
|
||||
import HepLean.Lorentz.ComplexVector.Contraction
|
||||
import HepLean.Lorentz.ComplexVector.Metric
|
||||
import HepLean.Lorentz.ComplexVector.Unit
|
||||
import HepLean.Mathematics.PiTensorProduct
|
||||
import HepLean.Lorentz.PauliMatrices.AsTensor
|
||||
/-!
|
||||
|
||||
## Complex Lorentz tensors
|
||||
|
||||
-/
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
namespace complexLorentzTensor
|
||||
|
||||
/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
|
||||
inductive Color
|
||||
| upL : Color
|
||||
| downL : Color
|
||||
| upR : Color
|
||||
| downR : Color
|
||||
| up : Color
|
||||
| down : Color
|
||||
|
||||
instance : DecidableEq Color := fun x y =>
|
||||
match x, y with
|
||||
| Color.upL, Color.upL => isTrue rfl
|
||||
| Color.downL, Color.downL => isTrue rfl
|
||||
| Color.upR, Color.upR => isTrue rfl
|
||||
| Color.downR, Color.downR => isTrue rfl
|
||||
| Color.up, Color.up => isTrue rfl
|
||||
| Color.down, Color.down => isTrue rfl
|
||||
/- The false -/
|
||||
| Color.upL, Color.downL => isFalse fun h => Color.noConfusion h
|
||||
| Color.upL, Color.upR => isFalse fun h => Color.noConfusion h
|
||||
| Color.upL, Color.downR => isFalse fun h => Color.noConfusion h
|
||||
| Color.upL, Color.up => isFalse fun h => Color.noConfusion h
|
||||
| Color.upL, Color.down => isFalse fun h => Color.noConfusion h
|
||||
| Color.downL, Color.upL => isFalse fun h => Color.noConfusion h
|
||||
| Color.downL, Color.upR => isFalse fun h => Color.noConfusion h
|
||||
| Color.downL, Color.downR => isFalse fun h => Color.noConfusion h
|
||||
| Color.downL, Color.up => isFalse fun h => Color.noConfusion h
|
||||
| Color.downL, Color.down => isFalse fun h => Color.noConfusion h
|
||||
| Color.upR, Color.upL => isFalse fun h => Color.noConfusion h
|
||||
| Color.upR, Color.downL => isFalse fun h => Color.noConfusion h
|
||||
| Color.upR, Color.downR => isFalse fun h => Color.noConfusion h
|
||||
| Color.upR, Color.up => isFalse fun h => Color.noConfusion h
|
||||
| Color.upR, Color.down => isFalse fun h => Color.noConfusion h
|
||||
| Color.downR, Color.upL => isFalse fun h => Color.noConfusion h
|
||||
| Color.downR, Color.downL => isFalse fun h => Color.noConfusion h
|
||||
| Color.downR, Color.upR => isFalse fun h => Color.noConfusion h
|
||||
| Color.downR, Color.up => isFalse fun h => Color.noConfusion h
|
||||
| Color.downR, Color.down => isFalse fun h => Color.noConfusion h
|
||||
| Color.up, Color.upL => isFalse fun h => Color.noConfusion h
|
||||
| Color.up, Color.downL => isFalse fun h => Color.noConfusion h
|
||||
| Color.up, Color.upR => isFalse fun h => Color.noConfusion h
|
||||
| Color.up, Color.downR => isFalse fun h => Color.noConfusion h
|
||||
| Color.up, Color.down => isFalse fun h => Color.noConfusion h
|
||||
| Color.down, Color.upL => isFalse fun h => Color.noConfusion h
|
||||
| Color.down, Color.downL => isFalse fun h => Color.noConfusion h
|
||||
| Color.down, Color.upR => isFalse fun h => Color.noConfusion h
|
||||
| Color.down, Color.downR => isFalse fun h => Color.noConfusion h
|
||||
| Color.down, Color.up => isFalse fun h => Color.noConfusion h
|
||||
|
||||
end complexLorentzTensor
|
||||
|
||||
noncomputable section
|
||||
open complexLorentzTensor in
|
||||
/-- The tensor structure for complex Lorentz tensors. -/
|
||||
def complexLorentzTensor : TensorSpecies where
|
||||
C := complexLorentzTensor.Color
|
||||
G := SL(2, ℂ)
|
||||
G_group := inferInstance
|
||||
k := ℂ
|
||||
k_commRing := inferInstance
|
||||
FD := Discrete.functor fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.leftHanded
|
||||
| Color.downL => Fermion.altLeftHanded
|
||||
| Color.upR => Fermion.rightHanded
|
||||
| Color.downR => Fermion.altRightHanded
|
||||
| Color.up => Lorentz.complexContr
|
||||
| Color.down => Lorentz.complexCo
|
||||
τ := fun c =>
|
||||
match c with
|
||||
| Color.upL => Color.downL
|
||||
| Color.downL => Color.upL
|
||||
| Color.upR => Color.downR
|
||||
| Color.downR => Color.upR
|
||||
| Color.up => Color.down
|
||||
| Color.down => Color.up
|
||||
τ_involution c := by
|
||||
match c with
|
||||
| Color.upL => rfl
|
||||
| Color.downL => rfl
|
||||
| Color.upR => rfl
|
||||
| Color.downR => rfl
|
||||
| Color.up => rfl
|
||||
| Color.down => rfl
|
||||
contr := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.leftAltContraction
|
||||
| Discrete.mk Color.downL => Fermion.altLeftContraction
|
||||
| Discrete.mk Color.upR => Fermion.rightAltContraction
|
||||
| Discrete.mk Color.downR => Fermion.altRightContraction
|
||||
| Discrete.mk Color.up => Lorentz.contrCoContraction
|
||||
| Discrete.mk Color.down => Lorentz.coContrContraction
|
||||
metric := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.leftMetric
|
||||
| Discrete.mk Color.downL => Fermion.altLeftMetric
|
||||
| Discrete.mk Color.upR => Fermion.rightMetric
|
||||
| Discrete.mk Color.downR => Fermion.altRightMetric
|
||||
| Discrete.mk Color.up => Lorentz.contrMetric
|
||||
| Discrete.mk Color.down => Lorentz.coMetric
|
||||
unit := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.altLeftLeftUnit
|
||||
| Discrete.mk Color.downL => Fermion.leftAltLeftUnit
|
||||
| Discrete.mk Color.upR => Fermion.altRightRightUnit
|
||||
| Discrete.mk Color.downR => Fermion.rightAltRightUnit
|
||||
| Discrete.mk Color.up => Lorentz.coContrUnit
|
||||
| Discrete.mk Color.down => Lorentz.contrCoUnit
|
||||
repDim := fun c =>
|
||||
match c with
|
||||
| Color.upL => 2
|
||||
| Color.downL => 2
|
||||
| Color.upR => 2
|
||||
| Color.downR => 2
|
||||
| Color.up => 4
|
||||
| Color.down => 4
|
||||
repDim_neZero := fun c =>
|
||||
match c with
|
||||
| Color.upL => inferInstance
|
||||
| Color.downL => inferInstance
|
||||
| Color.upR => inferInstance
|
||||
| Color.downR => inferInstance
|
||||
| Color.up => inferInstance
|
||||
| Color.down => inferInstance
|
||||
basis := fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.leftBasis
|
||||
| Color.downL => Fermion.altLeftBasis
|
||||
| Color.upR => Fermion.rightBasis
|
||||
| Color.downR => Fermion.altRightBasis
|
||||
| Color.up => Lorentz.complexContrBasisFin4
|
||||
| Color.down => Lorentz.complexCoBasisFin4
|
||||
contr_tmul_symm := fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.leftAltContraction_tmul_symm
|
||||
| Color.downL => Fermion.altLeftContraction_tmul_symm
|
||||
| Color.upR => Fermion.rightAltContraction_tmul_symm
|
||||
| Color.downR => Fermion.altRightContraction_tmul_symm
|
||||
| Color.up => Lorentz.contrCoContraction_tmul_symm
|
||||
| Color.down => Lorentz.coContrContraction_tmul_symm
|
||||
contr_unit := fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.contr_altLeftLeftUnit
|
||||
| Color.downL => Fermion.contr_leftAltLeftUnit
|
||||
| Color.upR => Fermion.contr_altRightRightUnit
|
||||
| Color.downR => Fermion.contr_rightAltRightUnit
|
||||
| Color.up => Lorentz.contr_coContrUnit
|
||||
| Color.down => Lorentz.contr_contrCoUnit
|
||||
unit_symm := fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.altLeftLeftUnit_symm
|
||||
| Color.downL => Fermion.leftAltLeftUnit_symm
|
||||
| Color.upR => Fermion.altRightRightUnit_symm
|
||||
| Color.downR => Fermion.rightAltRightUnit_symm
|
||||
| Color.up => Lorentz.coContrUnit_symm
|
||||
| Color.down => Lorentz.contrCoUnit_symm
|
||||
contr_metric := fun c =>
|
||||
match c with
|
||||
| Color.upL => by simpa using Fermion.leftAltContraction_apply_metric
|
||||
| Color.downL => by simpa using Fermion.altLeftContraction_apply_metric
|
||||
| Color.upR => by simpa using Fermion.rightAltContraction_apply_metric
|
||||
| Color.downR => by simpa using Fermion.altRightContraction_apply_metric
|
||||
| Color.up => by simpa using Lorentz.contrCoContraction_apply_metric
|
||||
| Color.down => by simpa using Lorentz.coContrContraction_apply_metric
|
||||
namespace complexLorentzTensor
|
||||
instance : DecidableEq complexLorentzTensor.C := complexLorentzTensor.instDecidableEqColor
|
||||
|
||||
lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c))
|
||||
(j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
|
||||
complexLorentzTensor.castToField
|
||||
((complexLorentzTensor.contr.app {as := c}).hom
|
||||
(complexLorentzTensor.basis c i ⊗ₜ complexLorentzTensor.basis (complexLorentzTensor.τ c) j)) =
|
||||
if i.val = j.val then 1 else 0 :=
|
||||
match c with
|
||||
| Color.upL => Fermion.leftAltContraction_basis _ _
|
||||
| Color.downL => Fermion.altLeftContraction_basis _ _
|
||||
| Color.upR => Fermion.rightAltContraction_basis _ _
|
||||
| Color.downR => Fermion.altRightContraction_basis _ _
|
||||
| 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
|
||||
|
|
@ -1,227 +0,0 @@
|
|||
/-
|
||||
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
|
||||
/-!
|
||||
|
||||
## Basis vectors associated with complex Lorentz tensors
|
||||
|
||||
Note that this file will be much improved once:
|
||||
https://github.com/leanprover-community/mathlib4/pull/11156
|
||||
is merged.
|
||||
|
||||
-/
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open TensorTree
|
||||
open OverColor.Discrete
|
||||
open Fermion
|
||||
noncomputable section
|
||||
namespace complexLorentzTensor
|
||||
|
||||
/-- Basis vectors for complex Lorentz tensors. -/
|
||||
def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C)
|
||||
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
|
||||
complexLorentzTensor.F.obj (OverColor.mk c) :=
|
||||
PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i))
|
||||
|
||||
lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
{c1 : Fin m → complexLorentzTensor.C}
|
||||
(σ : OverColor.mk c ⟶ OverColor.mk c1) (i : Fin m) :
|
||||
complexLorentzTensor.repDim (c ((OverColor.Hom.toEquiv σ).symm i)) =
|
||||
complexLorentzTensor.repDim (c1 i) := by
|
||||
have h1 := OverColor.Hom.toEquiv_symm_apply σ i
|
||||
simp only [Functor.const_obj_obj, OverColor.mk_hom] at h1
|
||||
rw [h1]
|
||||
|
||||
/-! TODO: Generalize `basis_eq_FD`. -/
|
||||
lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
|
||||
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) (i : Fin n)
|
||||
(h : { as := c i } = { as := c1 }) :
|
||||
(complexLorentzTensor.FD.map (eqToHom h)).hom
|
||||
(complexLorentzTensor.basis (c i) (b i)) =
|
||||
(complexLorentzTensor.basis c1 (Fin.cast (by simp_all) (b i))) := by
|
||||
have h' : c i = c1 := by
|
||||
simp_all only [Discrete.mk.injEq]
|
||||
subst h'
|
||||
rfl
|
||||
|
||||
lemma perm_basisVector {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 =
|
||||
(basisVector c1 (fun i => Fin.cast (perm_basisVector_cast σ i)
|
||||
(b ((OverColor.Hom.toEquiv σ).symm i)))) := by
|
||||
rw [perm_tensor]
|
||||
simp only [TensorSpecies.F_def, tensorNode_tensor]
|
||||
rw [basisVector, basisVector]
|
||||
erw [OverColor.lift.map_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
simp only [OverColor.mk_hom, OverColor.lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
|
||||
eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
|
||||
rw [basis_eq_FD]
|
||||
|
||||
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))) : ℂ :=
|
||||
(if (b i).val = (b (i.succAbove j)).val then (1 : ℂ) else 0)
|
||||
|
||||
lemma contrBasisVectorMul_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {b : Π k, Fin (complexLorentzTensor.repDim (c k))}
|
||||
(h : ¬ (b i).val = (b (i.succAbove j)).val) :
|
||||
contrBasisVectorMul i j b = 0 := by
|
||||
rw [contrBasisVectorMul]
|
||||
simp only [ite_eq_right_iff, one_ne_zero, imp_false]
|
||||
exact h
|
||||
|
||||
lemma contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {b : Π k, Fin (complexLorentzTensor.repDim (c k))}
|
||||
(h : (b i).val = (b (i.succAbove j)).val) :
|
||||
contrBasisVectorMul i j b = 1 := by
|
||||
rw [contrBasisVectorMul]
|
||||
simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
|
||||
exact h
|
||||
|
||||
lemma contr_basisVector {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 = (contrBasisVectorMul i j b) •
|
||||
basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
|
||||
(fun k => b (i.succAbove (j.succAbove k))) := by
|
||||
rw [contr_tensor]
|
||||
simp only [Nat.succ_eq_add_one, tensorNode_tensor]
|
||||
rw [basisVector]
|
||||
erw [TensorSpecies.contrMap_tprod]
|
||||
congr 1
|
||||
rw [basis_eq_FD]
|
||||
simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as,
|
||||
Function.comp_apply]
|
||||
erw [basis_contr]
|
||||
rfl
|
||||
|
||||
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
|
||||
exact contr_basisVector _
|
||||
|
||||
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) :
|
||||
(contr i j h (tensorNode (basisVector c b))).tensor =
|
||||
((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}
|
||||
{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) :
|
||||
(contr i j h (tensorNode (basisVector c b))).tensor =
|
||||
(tensorNode 0).tensor := by
|
||||
rw [contr_basisVector_tree, contrBasisVectorMul]
|
||||
rw [if_neg hn]
|
||||
simp only [Nat.succ_eq_add_one, smul_tensor, tensorNode_tensor, _root_.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)))
|
||||
i ≃ Fin (complexLorentzTensor.repDim ((Sum.elim c c1 i))) :=
|
||||
match i with
|
||||
| Sum.inl _ => Equiv.refl _
|
||||
| Sum.inr _ => Equiv.refl _
|
||||
|
||||
lemma prod_basisVector {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 =
|
||||
basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
|
||||
prodBasisVecEquiv (finSumFinEquiv.symm i)
|
||||
((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))) := by
|
||||
rw [prod_tensor, basisVector, basisVector]
|
||||
simp only [TensorSpecies.F_def, Functor.id_obj, OverColor.mk_hom,
|
||||
Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
tensorNode_tensor]
|
||||
have h1 := OverColor.lift.μ_tmul_tprod_mk complexLorentzTensor.FD
|
||||
(fun i => (complexLorentzTensor.basis (c i)) (b i))
|
||||
(fun i => (complexLorentzTensor.basis (c1 i)) (b1 i))
|
||||
erw [h1, OverColor.lift.map_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
obtain ⟨k, hk⟩ := finSumFinEquiv.surjective i
|
||||
subst hk
|
||||
simp only [Functor.id_obj, OverColor.mk_hom, Function.comp_apply,
|
||||
OverColor.lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom,
|
||||
Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
erw [← (Equiv.apply_eq_iff_eq_symm_apply finSumFinEquiv).mp rfl]
|
||||
match k with
|
||||
| Sum.inl k => rfl
|
||||
| Sum.inr k => rfl
|
||||
|
||||
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 =
|
||||
(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}
|
||||
{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) •
|
||||
basisVector (c ∘ Fin.succAbove i) (fun k => b (i.succAbove k)) := by
|
||||
rw [eval_tensor, basisVector, basisVector]
|
||||
simp only [Nat.succ_eq_add_one, Functor.id_obj, OverColor.mk_hom, tensorNode_tensor,
|
||||
Function.comp_apply, one_smul, _root_.zero_smul]
|
||||
erw [TensorSpecies.evalMap_tprod]
|
||||
congr 1
|
||||
have h1 : Fin.ofNat' _ ↑j = j := by
|
||||
simp [Fin.ext_iff]
|
||||
rw [Basis.repr_self, Finsupp.single_apply, h1]
|
||||
exact ite_congr (Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a))
|
||||
(congrFun rfl) (congrFun rfl)
|
||||
|
||||
end complexLorentzTensor
|
||||
end
|
||||
|
|
@ -1,196 +0,0 @@
|
|||
/-
|
||||
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.PauliMatrices.Basic
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Congr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
|
||||
/-!
|
||||
|
||||
## Bispinors
|
||||
|
||||
-/
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open TensorTree
|
||||
open OverColor.Discrete
|
||||
open Fermion
|
||||
noncomputable section
|
||||
namespace complexLorentzTensor
|
||||
open Lorentz
|
||||
|
||||
/-!
|
||||
|
||||
## Definitions
|
||||
|
||||
-/
|
||||
|
||||
/-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
|
||||
def contrBispinorUp (p : complexContr) :=
|
||||
{pauliCo | μ α β ⊗ p | μ}ᵀ.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
|
||||
|
||||
/-- A bispinor `pₐₐ` created from a lorentz vector `p_μ`. -/
|
||||
def coBispinorDown (p : complexCo) :=
|
||||
{εL' | α α' ⊗ εR' | β β' ⊗ coBispinorUp p | α β}ᵀ.tensor
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor nodes
|
||||
|
||||
-/
|
||||
|
||||
/-- The definitional tensor node relation for `contrBispinorUp`. -/
|
||||
lemma tensorNode_contrBispinorUp (p : complexContr) :
|
||||
{contrBispinorUp p | α β}ᵀ.tensor = {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor := by
|
||||
rw [contrBispinorUp, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `contrBispinorDown`. -/
|
||||
lemma tensorNode_contrBispinorDown (p : complexContr) :
|
||||
{contrBispinorDown p | α β}ᵀ.tensor =
|
||||
{εL' | α α' ⊗ εR' | β β' ⊗ contrBispinorUp p | α β}ᵀ.tensor := by
|
||||
rw [contrBispinorDown, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `coBispinorUp`. -/
|
||||
lemma tensorNode_coBispinorUp (p : complexCo) :
|
||||
{coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor := by
|
||||
rw [coBispinorUp, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `coBispinorDown`. -/
|
||||
lemma tensorNode_coBispinorDown (p : complexCo) :
|
||||
{coBispinorDown p | α β}ᵀ.tensor =
|
||||
{εL' | α α' ⊗ εR' | β β' ⊗ coBispinorUp p | α β}ᵀ.tensor := by
|
||||
rw [coBispinorDown, tensorNode_tensor]
|
||||
|
||||
/-!
|
||||
|
||||
## Basic equalities.
|
||||
|
||||
-/
|
||||
|
||||
informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where
|
||||
math :≈ "{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ"
|
||||
proof :≈ "Expand `contrBispinorDown` and use fact that metrics contract to the identity."
|
||||
deps :≈ [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric]
|
||||
|
||||
informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where
|
||||
math :≈ "{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ"
|
||||
proof :≈ "Expand `coBispinorDown` and use fact that metrics contract to the identity."
|
||||
deps :≈ [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric]
|
||||
|
||||
lemma contrBispinorDown_expand (p : complexContr) :
|
||||
{contrBispinorDown p | α β}ᵀ.tensor =
|
||||
{εL' | α α' ⊗ εR' | β β' ⊗
|
||||
(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 =
|
||||
{εL' | α α' ⊗ εR' | β β' ⊗
|
||||
(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
|
||||
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
|
||||
|
||||
set_option maxRecDepth 5000 in
|
||||
lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) :
|
||||
{coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀ := 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_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 [coBispinorDown_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
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
/-
|
||||
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.Basis
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
/-!
|
||||
|
||||
## Lemmas related to 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
|
||||
|
||||
set_option maxRecDepth 5000 in
|
||||
lemma antiSymm_contr_symm {A : complexLorentzTensor.F.obj (OverColor.mk ![Color.up, Color.up])}
|
||||
{S : complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down])}
|
||||
(hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
|
||||
{A | μ ν ⊗ S | μ ν = - A | μ ν ⊗ S | μ ν}ᵀ := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| hA]
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| hs]
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| prod_perm_right _ _ _ _]
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
|
||||
rw [contr_tensor_eq <| perm_contr_congr 1 2]
|
||||
rw [perm_contr_congr 0 0]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| neg_fst_prod _ _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| neg_contr _]
|
||||
rw [perm_tensor_eq <| neg_contr _]
|
||||
apply perm_congr _ rfl
|
||||
decide
|
||||
|
||||
end complexLorentzTensor
|
||||
|
||||
end
|
||||
|
|
@ -1,162 +0,0 @@
|
|||
/-
|
||||
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.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
|
||||
/-!
|
||||
|
||||
## Metrics 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 metric `ηᵢᵢ` as a complex Lorentz tensor. -/
|
||||
def coMetric := {Lorentz.coMetric | μ ν}ᵀ.tensor
|
||||
|
||||
/-- The metric `ηⁱⁱ` as a complex Lorentz tensor. -/
|
||||
def contrMetric := {Lorentz.contrMetric | μ ν}ᵀ.tensor
|
||||
|
||||
/-- The metric `εᵃᵃ` as a complex Lorentz tensor. -/
|
||||
def leftMetric := {Fermion.leftMetric | α α'}ᵀ.tensor
|
||||
|
||||
/-- The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor. -/
|
||||
def rightMetric := {Fermion.rightMetric | β β'}ᵀ.tensor
|
||||
|
||||
/-- The metric `εₐₐ` as a complex Lorentz tensor. -/
|
||||
def altLeftMetric := {Fermion.altLeftMetric | α α'}ᵀ.tensor
|
||||
|
||||
/-- The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor. -/
|
||||
def altRightMetric := {Fermion.altRightMetric | β β'}ᵀ.tensor
|
||||
|
||||
/-!
|
||||
|
||||
## Notation
|
||||
|
||||
-/
|
||||
|
||||
/-- The metric `ηᵢᵢ` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "η'" => coMetric
|
||||
|
||||
/-- The metric `ηⁱⁱ` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "η" => contrMetric
|
||||
|
||||
/-- The metric `εᵃᵃ` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "εL" => leftMetric
|
||||
|
||||
/-- The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "εR" => rightMetric
|
||||
|
||||
/-- The metric `εₐₐ` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "εL'" => altLeftMetric
|
||||
|
||||
/-- The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensors. -/
|
||||
scoped[complexLorentzTensor] notation "εR'" => altRightMetric
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor nodes.
|
||||
|
||||
-/
|
||||
|
||||
/-- The definitional tensor node relation for `coMetric`. -/
|
||||
lemma tensorNode_coMetric : {η' | μ ν}ᵀ.tensor = {Lorentz.coMetric | μ ν}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `contrMetric`. -/
|
||||
lemma tensorNode_contrMetric : {η | μ ν}ᵀ.tensor = {Lorentz.contrMetric | μ ν}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `leftMetric`. -/
|
||||
lemma tensorNode_leftMetric : {εL | α α'}ᵀ.tensor = {Fermion.leftMetric | α α'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `rightMetric`. -/
|
||||
lemma tensorNode_rightMetric : {εR | β β'}ᵀ.tensor = {Fermion.rightMetric | β β'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `altLeftMetric`. -/
|
||||
lemma tensorNode_altLeftMetric :
|
||||
{εL' | α α'}ᵀ.tensor = {Fermion.altLeftMetric | α α'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `altRightMetric`. -/
|
||||
lemma tensorNode_altRightMetric :
|
||||
{εR' | β β'}ᵀ.tensor = {Fermion.altRightMetric | β β'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Group actions
|
||||
|
||||
-/
|
||||
|
||||
/-- The tensor `coMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_coMetric (g : SL(2,ℂ)) : {g •ₐ η' | μ ν}ᵀ.tensor =
|
||||
{η' | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_coMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `contrMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_contrMetric (g : SL(2,ℂ)) : {g •ₐ η | μ ν}ᵀ.tensor =
|
||||
{η | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_contrMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `leftMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_leftMetric (g : SL(2,ℂ)) : {g •ₐ εL | α α'}ᵀ.tensor =
|
||||
{εL | α α'}ᵀ.tensor := by
|
||||
rw [tensorNode_leftMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `rightMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_rightMetric (g : SL(2,ℂ)) : {g •ₐ εR | β β'}ᵀ.tensor =
|
||||
{εR | β β'}ᵀ.tensor := by
|
||||
rw [tensorNode_rightMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `altLeftMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_altLeftMetric (g : SL(2,ℂ)) : {g •ₐ εL' | α α'}ᵀ.tensor =
|
||||
{εL' | α α'}ᵀ.tensor := by
|
||||
rw [tensorNode_altLeftMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `altRightMetric` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_altRightMetric (g : SL(2,ℂ)) : {g •ₐ εR' | β β'}ᵀ.tensor =
|
||||
{εR' | β β'}ᵀ.tensor := by
|
||||
rw [tensorNode_altRightMetric, constTwoNodeE]
|
||||
rw [← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -1,193 +0,0 @@
|
|||
/-
|
||||
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.Metrics.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.Basis
|
||||
/-!
|
||||
|
||||
## Metrics and basis expansions
|
||||
|
||||
-/
|
||||
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
|
||||
|
||||
/-- The expansion of the Lorentz covariant metric in terms of basis vectors. -/
|
||||
lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor =
|
||||
basisVector ![Color.down, Color.down] (fun _ => 0)
|
||||
- basisVector ![Color.down, Color.down] (fun _ => 1)
|
||||
- basisVector ![Color.down, Color.down] (fun _ => 2)
|
||||
- basisVector ![Color.down, Color.down] (fun _ => 3) := by
|
||||
rw [tensorNode_coMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Functor.id_obj, Fin.isValue]
|
||||
erw [Lorentz.coMetric_apply_one, Lorentz.coMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_sub]
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
all_goals
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom,
|
||||
cons_val_zero, Fin.cases_zero]
|
||||
change _ = Lorentz.complexCoBasisFin4 _
|
||||
simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
/-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as
|
||||
a tensor tree. -/
|
||||
lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
|
||||
(TensorTree.add (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 0))) <|
|
||||
TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 1)))) <|
|
||||
TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 2)))) <|
|
||||
(smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 3))))).tensor :=
|
||||
coMetric_basis_expand
|
||||
|
||||
/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors. -/
|
||||
lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
|
||||
basisVector ![Color.up, Color.up] (fun _ => 0)
|
||||
- basisVector ![Color.up, Color.up] (fun _ => 1)
|
||||
- basisVector ![Color.up, Color.up] (fun _ => 2)
|
||||
- basisVector ![Color.up, Color.up] (fun _ => 3) := by
|
||||
rw [tensorNode_contrMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V]
|
||||
erw [Lorentz.contrMetric_apply_one, Lorentz.contrMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_sub]
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
all_goals
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom,
|
||||
cons_val_zero, Fin.cases_zero]
|
||||
change _ = Lorentz.complexContrBasisFin4 _
|
||||
simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
|
||||
(TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
|
||||
TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 1)))) <|
|
||||
TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 2)))) <|
|
||||
(smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 3))))).tensor :=
|
||||
contrMatrix_basis_expand
|
||||
|
||||
lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
|
||||
- basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
|
||||
+ basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
|
||||
rw [tensorNode_leftMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
|
||||
erw [Fermion.leftMetric_apply_one, Fermion.leftMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_add, map_neg]
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
lemma leftMetric_expand_tree : {εL | α β}ᵀ.tensor =
|
||||
(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
|
||||
|
||||
lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
|
||||
basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1)
|
||||
- basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by
|
||||
rw [tensorNode_altLeftMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
|
||||
erw [Fermion.altLeftMetric_apply_one, Fermion.altLeftMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_sub]
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.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 : {εR | α β}ᵀ.tensor =
|
||||
- basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)
|
||||
+ basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by
|
||||
rw [tensorNode_rightMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
|
||||
erw [Fermion.rightMetric_apply_one, Fermion.rightMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_add, map_neg]
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
lemma rightMetric_expand_tree : {εR | α β}ᵀ.tensor =
|
||||
(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
|
||||
|
||||
lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
|
||||
basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1)
|
||||
- basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by
|
||||
rw [tensorNode_altRightMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
|
||||
erw [Fermion.altRightMetric_apply_one, Fermion.altRightMetricVal_expand_tmul]
|
||||
simp only [Fin.isValue, map_sub]
|
||||
congr 1
|
||||
all_goals
|
||||
erw [pairIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
lemma altRightMetric_expand_tree : {εR' | α β}ᵀ.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
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -1,152 +0,0 @@
|
|||
/-
|
||||
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.Metrics.Basis
|
||||
import HepLean.Tensors.ComplexLorentz.Units.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.Basis
|
||||
/-!
|
||||
|
||||
## Basic lemmas regarding metrics
|
||||
|
||||
-/
|
||||
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
|
||||
|
||||
/-!
|
||||
|
||||
## Symmetry properties
|
||||
|
||||
-/
|
||||
|
||||
informal_lemma coMetric_symm where
|
||||
math :≈ "The covariant metric is symmetric {η' | μ ν = η' | ν μ}ᵀ"
|
||||
deps :≈ [``coMetric]
|
||||
|
||||
informal_lemma contrMetric_symm where
|
||||
math :≈ "The contravariant metric is symmetric {η | μ ν = η | ν μ}ᵀ"
|
||||
deps :≈ [``contrMetric]
|
||||
|
||||
informal_lemma leftMetric_antisymm where
|
||||
math :≈ "The left metric is antisymmetric {εL | α α' = - εL | α' α}ᵀ"
|
||||
deps :≈ [``leftMetric]
|
||||
|
||||
informal_lemma rightMetric_antisymm where
|
||||
math :≈ "The right metric is antisymmetric {εR | β β' = - εR | β' β}ᵀ"
|
||||
deps :≈ [``rightMetric]
|
||||
|
||||
informal_lemma altLeftMetric_antisymm where
|
||||
math :≈ "The alt-left metric is antisymmetric {εL' | α α' = - εL' | α' α}ᵀ"
|
||||
deps :≈ [``altLeftMetric]
|
||||
|
||||
informal_lemma altRightMetric_antisymm where
|
||||
math :≈ "The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ"
|
||||
deps :≈ [``altRightMetric]
|
||||
|
||||
/-!
|
||||
|
||||
## Contractions with each other
|
||||
|
||||
-/
|
||||
|
||||
informal_lemma coMetric_contr_contrMetric where
|
||||
math :≈ "The contraction of the covariant metric with the contravariant metric is the unit
|
||||
{η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ"
|
||||
deps :≈ [``coMetric, ``contrMetric, ``coContrUnit]
|
||||
|
||||
informal_lemma contrMetric_contr_coMetric where
|
||||
math :≈ "The contraction of the contravariant metric with the covariant metric is the unit
|
||||
{η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ"
|
||||
deps :≈ [``contrMetric, ``coMetric, ``contrCoUnit]
|
||||
|
||||
informal_lemma leftMetric_contr_altLeftMetric where
|
||||
math :≈ "The contraction of the left metric with the alt-left metric is the unit
|
||||
{εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ"
|
||||
deps :≈ [``leftMetric, ``altLeftMetric, ``leftAltLeftUnit]
|
||||
|
||||
informal_lemma rightMetric_contr_altRightMetric where
|
||||
math :≈ "The contraction of the right metric with the alt-right metric is the unit
|
||||
{εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ"
|
||||
deps :≈ [``rightMetric, ``altRightMetric, ``rightAltRightUnit]
|
||||
|
||||
informal_lemma altLeftMetric_contr_leftMetric where
|
||||
math :≈ "The contraction of the alt-left metric with the left metric is the unit
|
||||
{εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ"
|
||||
deps :≈ [``altLeftMetric, ``leftMetric, ``altLeftLeftUnit]
|
||||
|
||||
informal_lemma altRightMetric_contr_rightMetric where
|
||||
math :≈ "The contraction of the alt-right metric with the right metric is the unit
|
||||
{εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ"
|
||||
deps :≈ [``altRightMetric, ``rightMetric, ``altRightRightUnit]
|
||||
|
||||
/-!
|
||||
|
||||
## Other relations
|
||||
|
||||
-/
|
||||
/-- 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
|
||||
|
||||
/- Expansion of the product of `εL` and `εR` in terms of a basis. -/
|
||||
lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
|
||||
= basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
- basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
|
||||
- basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
|
||||
rw [prod_tensor_eq_fst (leftMetric_expand_tree)]
|
||||
rw [prod_tensor_eq_snd (rightMetric_expand_tree)]
|
||||
rw [prod_add_both]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_prod _ _ _]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_tensor_eq <| prod_smul _ _ _]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_smul _ _ _]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_eq_one _ _ (by simp)]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_snd <| smul_prod _ _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_fst <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_fst <| add_tensor_eq_snd <| smul_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_basisVector_tree _ _]
|
||||
rw [← add_assoc]
|
||||
simp only [add_tensor, smul_tensor, tensorNode_tensor]
|
||||
change _ = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
+- basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
|
||||
+- basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
congr
|
||||
funext x
|
||||
fin_cases x <;> rfl
|
||||
|
||||
/- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/
|
||||
lemma leftMetric_prod_rightMetric_tree : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
|
||||
= (TensorTree.add (tensorNode
|
||||
(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 leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)))).tensor := by
|
||||
rw [leftMetric_prod_rightMetric]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor,
|
||||
smul_tensor, neg_smul, one_smul]
|
||||
rfl
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -1,253 +0,0 @@
|
|||
/-
|
||||
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.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
|
||||
import HepLean.Tensors.ComplexLorentz.Metrics.Lemmas
|
||||
/-!
|
||||
|
||||
## 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 the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
|
||||
def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/
|
||||
def pauliCo := {η' | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ_μ_α_{dot β}`. -/
|
||||
def pauliCoDown := {pauliCo | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ^μ_α_{dot β}`. -/
|
||||
def pauliContrDown := {pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.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 =
|
||||
{η' | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor := by
|
||||
rw [pauliCo, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `pauliCoDown`. -/
|
||||
lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor =
|
||||
{pauliCo | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by
|
||||
rw [pauliCoDown, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `pauliContrDown`. -/
|
||||
lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
|
||||
{pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by
|
||||
rw [pauliContr, tensorNode_tensor]
|
||||
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 | μ α' β' = εL' | α α' ⊗ εR' | β β' ⊗ 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
|
||||
|
||||
set_option maxRecDepth 5000 in
|
||||
/-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/
|
||||
lemma pauliContrDown_eq_metric_mul_pauliContr :
|
||||
{pauliContrDown | μ α' β' = εL' | α α' ⊗
|
||||
εR' | β β' ⊗ pauliContr | μ α β}ᵀ := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [tensorNode_pauliContrDown]
|
||||
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
|
||||
|
||||
/-!
|
||||
|
||||
## Group actions
|
||||
|
||||
-/
|
||||
|
||||
/-- The tensor `pauliContr` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_pauliContr (g : SL(2,ℂ)) : {g •ₐ pauliContr | μ α β}ᵀ.tensor =
|
||||
{pauliContr | μ α β}ᵀ.tensor := by
|
||||
rw [tensorNode_pauliContr, constThreeNodeE]
|
||||
rw [← action_constThreeNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `pauliCo` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_pauliCo (g : SL(2,ℂ)) : {g •ₐ pauliCo | μ α β}ᵀ.tensor =
|
||||
{pauliCo | μ α β}ᵀ.tensor := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [action_tensor_eq <| tensorNode_pauliCo]
|
||||
rw [action_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_pauliContr]
|
||||
rw [(contr_action _ _).symm]
|
||||
rw [contr_tensor_eq <| (prod_action _ _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| action_constTwoNode _ _]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constThreeNode _ _]
|
||||
conv =>
|
||||
rhs
|
||||
rw [tensorNode_pauliCo]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_pauliContr]
|
||||
rfl
|
||||
|
||||
/-- The tensor `pauliCoDown` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_pauliCoDown (g : SL(2,ℂ)) : {g •ₐ pauliCoDown | μ α β}ᵀ.tensor =
|
||||
{pauliCoDown | μ α β}ᵀ.tensor := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [action_tensor_eq <| tensorNode_pauliCoDown]
|
||||
rw [(contr_action _ _).symm]
|
||||
rw [contr_tensor_eq <| (prod_action _ _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| (contr_action _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| (prod_action _ _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_fst <|
|
||||
action_pauliCo _]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <|
|
||||
action_altLeftMetric _]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_altRightMetric _]
|
||||
conv =>
|
||||
rhs
|
||||
rw [tensorNode_pauliCoDown]
|
||||
|
||||
/-- The tensor `pauliContrDown` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_pauliContrDown (g : SL(2,ℂ)) : {g •ₐ pauliContrDown | μ α β}ᵀ.tensor =
|
||||
{pauliContrDown | μ α β}ᵀ.tensor := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [action_tensor_eq <| tensorNode_pauliContrDown]
|
||||
rw [(contr_action _ _).symm]
|
||||
rw [contr_tensor_eq <| (prod_action _ _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| (contr_action _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| (prod_action _ _ _).symm]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_fst <|
|
||||
action_pauliContr _]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <|
|
||||
action_altLeftMetric _]
|
||||
erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_altRightMetric _]
|
||||
conv =>
|
||||
rhs
|
||||
rw [tensorNode_pauliContrDown]
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -1,622 +0,0 @@
|
|||
/-
|
||||
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.PauliMatrices.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.Basis
|
||||
/-!
|
||||
|
||||
## Pauli matrices and the basis of 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
|
||||
|
||||
/-!
|
||||
|
||||
## Expanding pauliContr in a basis.
|
||||
|
||||
-/
|
||||
/-- The expansion of the Pauli matrices `σ^μ^a^{dot a}` in terms of basis vectors. -/
|
||||
lemma pauliContr_in_basis : {pauliContr | μ α β}ᵀ.tensor =
|
||||
basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
+ basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 1 | 2 => 1)
|
||||
+ basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 0 | 2 => 1)
|
||||
+ basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 1 | 2 => 0)
|
||||
- I • basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 0 | 2 => 1)
|
||||
+ I • basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 1 | 2 => 0)
|
||||
+ basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 0 | 2 => 0)
|
||||
- basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
|
||||
rw [tensorNode_pauliContr]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constThreeNode_tensor,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
|
||||
erw [PauliMatrix.asConsTensor_apply_one, PauliMatrix.asTensor_expand]
|
||||
simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Action.instMonoidalCategory_tensorObj_V,
|
||||
Fin.isValue, map_sub, map_add, _root_.map_smul]
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [tripleIsoSep_tmul, basisVector]
|
||||
apply congrArg
|
||||
try apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| (0 : Fin 3) =>
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom,
|
||||
cons_val_zero, Fin.cases_zero]
|
||||
change _ = Lorentz.complexContrBasisFin4 _
|
||||
simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
|
||||
rfl
|
||||
| (1 : Fin 3) => rfl
|
||||
| (2 : Fin 3) => rfl
|
||||
|
||||
lemma pauliContr_basis_expand_tree : {pauliContr | μ α β}ᵀ.tensor =
|
||||
(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
|
||||
(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)))) <|
|
||||
TensorTree.add (smul I (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <|
|
||||
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
|
||||
rw [pauliContr_in_basis]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_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)
|
||||
|
||||
lemma prod_pauliMatrix_basis_tree_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(t : TensorTree complexLorentzTensor c) :
|
||||
(TensorTree.prod t (tensorNode pauliContr)).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 <| pauliContr_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 _ _ _]
|
||||
|
||||
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 (tensorNode pauliContr))).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))
|
||||
(tensorNode pauliContr))).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
|
||||
|
||||
/-- The map to color which appears when contracting a basis vector with
|
||||
puali matrices. -/
|
||||
def pauliMatrixBasisProdMap
|
||||
{n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) (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))
|
||||
|
||||
/-- The new basis vectors which appear when contracting pauli matrices with
|
||||
basis vectors. -/
|
||||
def basisVectorContrPauli {n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(i : Fin (n + 3)) (j : Fin (n +2))
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k)))
|
||||
(i1 i2 i3 : Fin 4) :=
|
||||
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) := fun k => (pauliMatrixBasisProdMap b i1 i2 i3)
|
||||
(i.succAbove (j.succAbove k))
|
||||
basisVector c' (b' i1 i2 i3)
|
||||
|
||||
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) := fun k => (pauliMatrixBasisProdMap b i1 i2 i3)
|
||||
(i.succAbove (j.succAbove k))
|
||||
(contr i j h (TensorTree.prod (tensorNode (basisVector c b))
|
||||
(tensorNode pauliContr))).tensor =
|
||||
(((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 0 0))
|
||||
(tensorNode (basisVector c' (b' 0 0 0))))).add
|
||||
(((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 1 1))
|
||||
(tensorNode (basisVector c' (b' 0 1 1))))).add
|
||||
(((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 0 1))
|
||||
(tensorNode (basisVector c' (b' 1 0 1))))).add
|
||||
(((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 1 0))
|
||||
(tensorNode (basisVector c' (b' 1 1 0))))).add
|
||||
((TensorTree.smul (-I) ((TensorTree.smul
|
||||
(contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1))
|
||||
(tensorNode (basisVector c' (b' 2 0 1)))))).add
|
||||
((TensorTree.smul I ((TensorTree.smul
|
||||
(contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0))
|
||||
(tensorNode (basisVector c' (b' 2 1 0)))))).add
|
||||
(((TensorTree.smul (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 0 0))
|
||||
(tensorNode (basisVector c' (b' 3 0 0))))).add
|
||||
(TensorTree.smul (-1) ((TensorTree.smul
|
||||
(contrBasisVectorMul i j (pauliMatrixBasisProdMap 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 _]
|
||||
rfl
|
||||
|
||||
lemma basis_contr_pauliMatrix_basis_tree_expand_tensor {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))) :
|
||||
(contr i j h (TensorTree.prod (tensorNode (basisVector c b))
|
||||
(tensorNode pauliContr))).tensor =
|
||||
(contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 0 0)) •
|
||||
(basisVectorContrPauli i j b 0 0 0)
|
||||
+ (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 0 1 1)) •
|
||||
(basisVectorContrPauli i j b 0 1 1)
|
||||
+ (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 0 1)) •
|
||||
(basisVectorContrPauli i j b 1 0 1)
|
||||
+ (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 1 1 0)) •
|
||||
(basisVectorContrPauli i j b 1 1 0)
|
||||
+ (-I) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 0 1)) •
|
||||
(basisVectorContrPauli i j b 2 0 1)
|
||||
+ I • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 2 1 0)) •
|
||||
(basisVectorContrPauli i j b 2 1 0)
|
||||
+ (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 0 0)) •
|
||||
(basisVectorContrPauli i j b 3 0 0)
|
||||
+ (-1 : ℂ) • (contrBasisVectorMul i j (pauliMatrixBasisProdMap b 3 1 1)) •
|
||||
(basisVectorContrPauli i j b 3 1 1) := by
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val_one, head_cons, Fin.val_zero,
|
||||
Nat.cast_zero, cons_val_two, Fin.val_one, Nat.cast_one, add_tensor, smul_tensor,
|
||||
tensorNode_tensor, neg_smul, one_smul, Int.reduceNeg]
|
||||
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)
|
||||
|
||||
lemma pauliMatrix_contr_down_0 :
|
||||
(contr 1 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
|
||||
(tensorNode pauliContr)))).tensor
|
||||
= basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
+ basisVector pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
congr 1
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_1 :
|
||||
{(basisVector ![Color.down, Color.down] fun x => 1) | ν μ ⊗
|
||||
pauliContr | μ α β}ᵀ.tensor
|
||||
= basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
|
||||
+ basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
congr 1
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_2 :
|
||||
{(basisVector ![Color.down, Color.down] fun x => 2) | μ ν ⊗
|
||||
pauliContr | ν α β}ᵀ.tensor
|
||||
= (- I) • basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
|
||||
+ (I) • basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
congr 3
|
||||
· decide
|
||||
· decide
|
||||
|
||||
lemma pauliMatrix_contr_down_3 :
|
||||
{(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
|
||||
pauliContr | ν α β}ᵀ.tensor
|
||||
= basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
|
||||
+ (- 1 : ℂ) • basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
congr 3
|
||||
· decide
|
||||
· decide
|
||||
|
||||
/-- The expansion of `pauliCo` in terms of a basis. -/
|
||||
lemma pauliCo_basis_expand : pauliCo
|
||||
= basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
+ basisVector pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1)
|
||||
- basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
|
||||
- basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0)
|
||||
+ I • basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
|
||||
- I • basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0)
|
||||
- basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
|
||||
+ basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [pauliCo]
|
||||
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 _ _]
|
||||
simp only [tensorNode_tensor, add_tensor, smul_tensor]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, neg_smul, one_smul]
|
||||
conv =>
|
||||
lhs; lhs;
|
||||
rw [pauliMatrix_contr_down_0]
|
||||
conv =>
|
||||
lhs; rhs; lhs; rhs;
|
||||
rw [pauliMatrix_contr_down_1]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs; rhs;
|
||||
rw [pauliMatrix_contr_down_2]
|
||||
conv =>
|
||||
lhs; rhs; rhs; rhs; rhs;
|
||||
rw [pauliMatrix_contr_down_3]
|
||||
simp only [neg_smul, one_smul]
|
||||
abel
|
||||
|
||||
lemma pauliCo_basis_expand_tree : {pauliCo | μ α β}ᵀ.tensor
|
||||
= (TensorTree.add (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
|
||||
TensorTree.add (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1))) <|
|
||||
TensorTree.add (TensorTree.smul (-1) (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)))) <|
|
||||
TensorTree.add (TensorTree.smul (-1) (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0)))) <|
|
||||
TensorTree.add (TensorTree.smul I (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <|
|
||||
TensorTree.add (TensorTree.smul (-I) (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <|
|
||||
TensorTree.add (TensorTree.smul (-1) (tensorNode
|
||||
(basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)))) <|
|
||||
(tensorNode (basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1)))).tensor := by
|
||||
rw [pauliCo_basis_expand]
|
||||
simp only [Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor, smul_tensor, neg_smul,
|
||||
one_smul]
|
||||
rfl
|
||||
|
||||
lemma pauliCo_prod_basis_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(t : TensorTree complexLorentzTensor c) :
|
||||
(prod (tensorNode pauliCo) t).tensor =
|
||||
(((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add
|
||||
(((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add
|
||||
((TensorTree.smul I ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add
|
||||
((TensorTree.smul (-I) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add
|
||||
((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod
|
||||
t)))))))).tensor := by
|
||||
rw [prod_tensor_eq_fst <| pauliCo_basis_expand_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 complexLorentzTensor
|
||||
|
|
@ -1,561 +0,0 @@
|
|||
/-
|
||||
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.PauliMatrices.Basis
|
||||
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 complexLorentzTensor
|
||||
open Fermion
|
||||
|
||||
/-- 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 1 ∘ 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 pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.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
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.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
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.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
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
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 pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗
|
||||
pauliContr | μ α' β'}ᵀ.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
|
||||
conv =>
|
||||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
rw [basisVectorContrPauli, basisVectorContrPauli]
|
||||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
/-! TODO: Work out why `pauliCo_prod_basis_expand'` is needed. -/
|
||||
/-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
|
||||
It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
|
||||
`pauliMatrix_lower_basis_expand_prod` does not work. -/
|
||||
private lemma pauliCo_prod_basis_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(t : TensorTree complexLorentzTensor c) :
|
||||
(TensorTree.prod (tensorNode pauliCo) t).tensor =
|
||||
((((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add
|
||||
(((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add
|
||||
((TensorTree.smul I ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add
|
||||
((TensorTree.smul (-I) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add
|
||||
((TensorTree.smul (-1) ((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add
|
||||
((tensorNode
|
||||
(basisVector pauliCoMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod
|
||||
t))))))))).tensor := by
|
||||
exact pauliCo_prod_basis_expand _
|
||||
|
||||
lemma pauliCo_contr_pauliContr_expand_aux :
|
||||
{pauliCo | μ α β ⊗ pauliContr | μ α' β'}ᵀ.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 <| pauliCo_prod_basis_expand' _]
|
||||
/- 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 pauliCo_contr_pauliContr_expand :
|
||||
{pauliCo | ν α β ⊗ pauliContr | ν α' β'}ᵀ.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 [pauliCo_contr_pauliContr_expand_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 pauliCo_contr_pauliContr :
|
||||
{pauliCo | ν α β ⊗ pauliContr | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by
|
||||
rw [pauliCo_contr_pauliContr_expand]
|
||||
rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_prod_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 complexLorentzTensor
|
||||
|
|
@ -1,160 +0,0 @@
|
|||
/-
|
||||
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.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
|
||||
/-!
|
||||
|
||||
## Metrics 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 unit `δᵢⁱ` as a complex Lorentz tensor. -/
|
||||
def coContrUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.down Color.up
|
||||
Lorentz.coContrUnit).tensor
|
||||
|
||||
/-- The unit `δⁱᵢ` as a complex Lorentz tensor. -/
|
||||
def contrCoUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.up Color.down
|
||||
Lorentz.contrCoUnit).tensor
|
||||
|
||||
/-- The unit `δₐᵃ` as a complex Lorentz tensor. -/
|
||||
def altLeftLeftUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.downL Color.upL
|
||||
Fermion.altLeftLeftUnit).tensor
|
||||
|
||||
/-- The unit `δᵃₐ` as a complex Lorentz tensor. -/
|
||||
def leftAltLeftUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.upL Color.downL
|
||||
Fermion.leftAltLeftUnit).tensor
|
||||
|
||||
/-- The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor. -/
|
||||
def altRightRightUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.downR Color.upR
|
||||
Fermion.altRightRightUnit).tensor
|
||||
|
||||
/-- The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor. -/
|
||||
def rightAltRightUnit := (TensorTree.constTwoNodeE complexLorentzTensor Color.upR Color.downR
|
||||
Fermion.rightAltRightUnit).tensor
|
||||
|
||||
/-!
|
||||
|
||||
## Notation
|
||||
|
||||
-/
|
||||
|
||||
/-- The unit `δᵢⁱ` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δ'" => coContrUnit
|
||||
|
||||
/-- The unit `δⁱᵢ` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δ" => contrCoUnit
|
||||
|
||||
/-- The unit `δₐᵃ` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δL'" => altLeftLeftUnit
|
||||
|
||||
/-- The unit `δᵃₐ` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δL" => leftAltLeftUnit
|
||||
|
||||
/-- The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δR'" => altRightRightUnit
|
||||
|
||||
/-- The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor. -/
|
||||
scoped[complexLorentzTensor] notation "δR" => rightAltRightUnit
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor nodes.
|
||||
|
||||
-/
|
||||
|
||||
/-- The definitional tensor node relation for `coContrUnit`. -/
|
||||
lemma tensorNode_coContrUnit : {δ' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
|
||||
Color.down Color.up Lorentz.coContrUnit).tensor:= by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `contrCoUnit`. -/
|
||||
lemma tensorNode_contrCoUnit: {δ | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
|
||||
Color.up Color.down Lorentz.contrCoUnit).tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `altLeftLeftUnit`. -/
|
||||
lemma tensorNode_altLeftLeftUnit : {δL' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
|
||||
complexLorentzTensor Color.downL Color.upL Fermion.altLeftLeftUnit).tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `leftAltLeftUnit`. -/
|
||||
lemma tensorNode_leftAltLeftUnit : {δL | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
|
||||
complexLorentzTensor Color.upL Color.downL Fermion.leftAltLeftUnit).tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `altRightRightUnit`. -/
|
||||
lemma tensorNode_altRightRightUnit: {δR' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
|
||||
complexLorentzTensor Color.downR Color.upR Fermion.altRightRightUnit).tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `rightAltRightUnit`. -/
|
||||
lemma tensorNode_rightAltRightUnit: {δR | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
|
||||
complexLorentzTensor Color.upR Color.downR Fermion.rightAltRightUnit).tensor := by
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Group actions
|
||||
|
||||
-/
|
||||
|
||||
/-- The tensor `coContrUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_coContrUnit (g : SL(2,ℂ)) : {g •ₐ δ' | μ ν}ᵀ.tensor = {δ' | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_coContrUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `contrCoUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_contrCoUnit (g : SL(2,ℂ)) : {g •ₐ δ | μ ν}ᵀ.tensor = {δ | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_contrCoUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `altLeftLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_altLeftLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL' | μ ν}ᵀ.tensor = {δL' | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_altLeftLeftUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `leftAltLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_leftAltLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL | μ ν}ᵀ.tensor = {δL | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_leftAltLeftUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `altRightRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_altRightRightUnit (g : SL(2,ℂ)) : {g •ₐ δR' | μ ν}ᵀ.tensor = {δR' | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_altRightRightUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
/-- The tensor `rightAltRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
|
||||
lemma action_rightAltRightUnit (g : SL(2,ℂ)) : {g •ₐ δR | μ ν}ᵀ.tensor = {δR | μ ν}ᵀ.tensor := by
|
||||
rw [tensorNode_rightAltRightUnit, constTwoNodeE, ← action_constTwoNode _ g]
|
||||
rfl
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -1,63 +0,0 @@
|
|||
/-
|
||||
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.Metrics.Basis
|
||||
import HepLean.Tensors.ComplexLorentz.Units.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.Basis
|
||||
/-!
|
||||
|
||||
## Symmetry lemmas relating to units
|
||||
|
||||
-/
|
||||
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
|
||||
|
||||
/-!
|
||||
|
||||
## Symmetry properties
|
||||
|
||||
-/
|
||||
|
||||
informal_lemma coContrUnit_symm where
|
||||
math :≈ "Swapping indices of coContrUnit returns contrCoUnit, i.e. {δ' | μ ν = δ | ν μ}.ᵀ"
|
||||
deps :≈ [``coContrUnit, ``contrCoUnit]
|
||||
|
||||
informal_lemma contrCoUnit_symm where
|
||||
math :≈ "Swapping indices of contrCoUnit returns coContrUnit, i.e. {δ | μ ν = δ' | ν μ}ᵀ"
|
||||
deps :≈ [``contrCoUnit, ``coContrUnit]
|
||||
|
||||
informal_lemma altLeftLeftUnit_symm where
|
||||
math :≈ "Swapping indices of altLeftLeftUnit returns leftAltLeftUnit, i.e.
|
||||
{δL' | α α' = δL | α' α}ᵀ"
|
||||
deps :≈ [``altLeftLeftUnit, ``leftAltLeftUnit]
|
||||
|
||||
informal_lemma leftAltLeftUnit_symm where
|
||||
math :≈ "Swapping indices of leftAltLeftUnit returns altLeftLeftUnit, i.e.
|
||||
{δL | α α' = δL' | α' α}ᵀ"
|
||||
deps :≈ [``leftAltLeftUnit, ``altLeftLeftUnit]
|
||||
|
||||
informal_lemma altRightRightUnit_symm where
|
||||
math :≈ "Swapping indices of altRightRightUnit returns rightAltRightUnit, i.e.
|
||||
{δR' | β β' = δR | β' β}ᵀ"
|
||||
deps :≈ [``altRightRightUnit, ``rightAltRightUnit]
|
||||
|
||||
informal_lemma rightAltRightUnit_symm where
|
||||
math :≈ "Swapping indices of rightAltRightUnit returns altRightRightUnit, i.e.
|
||||
{δR | β β' = δR' | β' β}ᵀ"
|
||||
deps :≈ [``rightAltRightUnit, ``altRightRightUnit]
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.Tensors.Tree.Basic
|
||||
import Lean.Elab.Term
|
||||
import HepLean.Tensors.Tree.Dot
|
||||
import HepLean.Tensors.ComplexLorentz.Basic
|
||||
import HepLean.Lorentz.ComplexTensor.Basic
|
||||
/-!
|
||||
|
||||
# Elaboration of tensor trees
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue