From c565e7ea1c5763d7e4364c3b576b25444a65d776 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 25 Oct 2024 05:30:04 +0000 Subject: [PATCH] feat: Add defn of bispinors --- HepLean.lean | 1 + HepLean/SpaceTime/WeylFermion/Metric.lean | 16 +++---- .../ComplexLorentz/Bispinors/Basic.lean | 47 +++++++++++++++++++ 3 files changed, 56 insertions(+), 8 deletions(-) create mode 100644 HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean diff --git a/HepLean.lean b/HepLean.lean index 4006143..e59086e 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -110,6 +110,7 @@ import HepLean.StandardModel.Representations import HepLean.Tensors.ComplexLorentz.Basic import HepLean.Tensors.ComplexLorentz.Basis import HepLean.Tensors.ComplexLorentz.BasisTrees +import HepLean.Tensors.ComplexLorentz.Bispinors.Basic import HepLean.Tensors.ComplexLorentz.Lemmas import HepLean.Tensors.ComplexLorentz.PauliContr import HepLean.Tensors.ComplexLorentz.PauliLower diff --git a/HepLean/SpaceTime/WeylFermion/Metric.lean b/HepLean/SpaceTime/WeylFermion/Metric.lean index cf45196..617a50b 100644 --- a/HepLean/SpaceTime/WeylFermion/Metric.lean +++ b/HepLean/SpaceTime/WeylFermion/Metric.lean @@ -67,7 +67,7 @@ lemma metricRaw_comm_star (M : SL(2,ℂ)) : metricRaw * M.1.map star = ((M.1)⁻ rw [eta_fin_two (!![M.1 0 0, M.1 0 1; M.1 1 0, M.1 1 1].map star)] simp -/-- The metric `εₐₐ` as an element of `(leftHanded ⊗ leftHanded).V`. -/ +/-- The metric `εᵃᵃ` as an element of `(leftHanded ⊗ leftHanded).V`. -/ def leftMetricVal : (leftHanded ⊗ leftHanded).V := leftLeftToMatrix.symm (- metricRaw) @@ -80,7 +80,7 @@ lemma leftMetricVal_expand_tmul : leftMetricVal = Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons, neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add] -/-- The metric `εₐₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded`, +/-- The metric `εᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded`, making manifest its invariance under the action of `SL(2,ℂ)`. -/ def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where hom := { @@ -114,7 +114,7 @@ lemma leftMetric_apply_one : leftMetric.hom (1 : ℂ) = leftMetricVal := by simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, leftMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] -/-- The metric `εᵃᵃ` as an element of `(altLeftHanded ⊗ altLeftHanded).V`. -/ +/-- The metric `εₐₐ` as an element of `(altLeftHanded ⊗ altLeftHanded).V`. -/ def altLeftMetricVal : (altLeftHanded ⊗ altLeftHanded).V := altLeftaltLeftToMatrix.symm metricRaw @@ -128,7 +128,7 @@ lemma altLeftMetricVal_expand_tmul : altLeftMetricVal = neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add] rfl -/-- The metric `εᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded`, +/-- The metric `εₐₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded`, making manifest its invariance under the action of `SL(2,ℂ)`. -/ def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded where hom := { @@ -162,7 +162,7 @@ lemma altLeftMetric_apply_one : altLeftMetric.hom (1 : ℂ) = altLeftMetricVal : simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, altLeftMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] -/-- The metric `ε_{dot a}_{dot a}` as an element of `(rightHanded ⊗ rightHanded).V`. -/ +/-- The metric `ε^{dot a}^{dot a}` as an element of `(rightHanded ⊗ rightHanded).V`. -/ def rightMetricVal : (rightHanded ⊗ rightHanded).V := rightRightToMatrix.symm (- metricRaw) @@ -175,7 +175,7 @@ lemma rightMetricVal_expand_tmul : rightMetricVal = Finset.sum_neg_distrib, Fin.sum_univ_two, Fin.isValue, cons_val_zero, cons_val_one, head_cons, neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add] -/-- The metric `ε_{dot a}_{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded`, +/-- The metric `ε^{dot a}^{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded`, making manifest its invariance under the action of `SL(2,ℂ)`. -/ def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded where hom := { @@ -217,7 +217,7 @@ lemma rightMetric_apply_one : rightMetric.hom (1 : ℂ) = rightMetricVal := by simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, rightMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul] -/-- The metric `ε^{dot a}^{dot a}` as an element of `(altRightHanded ⊗ altRightHanded).V`. -/ +/-- The metric `ε_{dot a}_{dot a}` as an element of `(altRightHanded ⊗ altRightHanded).V`. -/ def altRightMetricVal : (altRightHanded ⊗ altRightHanded).V := altRightAltRightToMatrix.symm (metricRaw) @@ -231,7 +231,7 @@ lemma altRightMetricVal_expand_tmul : altRightMetricVal = neg_add_rev, one_smul, zero_smul, neg_zero, add_zero, head_fin_const, neg_neg, zero_add] rfl -/-- The metric `ε^{dot a}^{dot a}` as a morphism +/-- The metric `ε_{dot a}_{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded`, making manifest its invariance under the action of `SL(2,ℂ)`. -/ def altRightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded where diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean new file mode 100644 index 0000000..6e2c614 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean @@ -0,0 +1,47 @@ +/- +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 +/-! + +## 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 Lorentz +namespace complexContr + +/-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/ +def bispinorUp (p : complexContr) := + {p | μ ⊗ (Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β)}ᵀ.tensor + +/-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/ +def bispinorDown (p : complexContr) := + {Fermion.altRightMetric | β β' ⊗ Fermion.altLeftMetric | α α' ⊗ + (complexContr.bispinorUp p) | α β}ᵀ.tensor + +end complexContr +end Lorentz +end