From 34c3643bac707a61f2690b4b6aa4f75dbbe9be15 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 29 Oct 2024 13:46:18 +0000 Subject: [PATCH] Refactor: Metrics as complex lorentz tensors --- HepLean.lean | 3 + HepLean/Tensors/ComplexLorentz/Basis.lean | 163 --------------- HepLean/Tensors/ComplexLorentz/Lemmas.lean | 59 ------ .../Tensors/ComplexLorentz/Metrics/Basic.lean | 162 +++++++++++++++ .../Tensors/ComplexLorentz/Metrics/Basis.lean | 191 ++++++++++++++++++ .../ComplexLorentz/Metrics/Lemmas.lean | 79 ++++++++ .../ComplexLorentz/PauliMatrices/Basic.lean | 28 ++- .../PauliMatrices/CoContractContr.lean | 3 +- 8 files changed, 448 insertions(+), 240 deletions(-) create mode 100644 HepLean/Tensors/ComplexLorentz/Metrics/Basic.lean create mode 100644 HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean create mode 100644 HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean diff --git a/HepLean.lean b/HepLean.lean index 1cd9425..9b9d98d 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -111,6 +111,9 @@ import HepLean.Tensors.ComplexLorentz.Basic import HepLean.Tensors.ComplexLorentz.Basis import HepLean.Tensors.ComplexLorentz.Bispinors.Basic import HepLean.Tensors.ComplexLorentz.Lemmas +import HepLean.Tensors.ComplexLorentz.Metrics.Basic +import HepLean.Tensors.ComplexLorentz.Metrics.Basis +import HepLean.Tensors.ComplexLorentz.Metrics.Lemmas import HepLean.Tensors.ComplexLorentz.PauliMatrices.Basic import HepLean.Tensors.ComplexLorentz.PauliMatrices.Basis import HepLean.Tensors.ComplexLorentz.PauliMatrices.CoContractContr diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean index 06bf7c8..b7cf1f6 100644 --- a/HepLean/Tensors/ComplexLorentz/Basis.lean +++ b/HepLean/Tensors/ComplexLorentz/Basis.lean @@ -223,168 +223,5 @@ lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C} exact ite_congr (Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)) (congrFun rfl) (congrFun rfl) -/-! - -## Useful expansions. - --/ - -/-- The expansion of the Lorentz covariant metric in terms of basis vectors. -/ -lemma coMetric_basis_expand : {Lorentz.coMetric | μ ν}ᵀ.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 - 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 - -lemma coMetric_basis_expand_tree : {Lorentz.coMetric | μ ν}ᵀ.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 : {Lorentz.contrMetric | μ ν}ᵀ.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 - 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 : {Lorentz.contrMetric | μ ν}ᵀ.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 : {Fermion.leftMetric | α β}ᵀ.tensor = - - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1) - + basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by - 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 : {Fermion.leftMetric | α β}ᵀ.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 : {Fermion.altLeftMetric | α β}ᵀ.tensor = - basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1) - - basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by - 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 : {Fermion.altLeftMetric | α β}ᵀ.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 : {Fermion.rightMetric | α β}ᵀ.tensor = - - basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1) - + basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by - 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 : {Fermion.rightMetric | α β}ᵀ.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 : {Fermion.altRightMetric | α β}ᵀ.tensor = - basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1) - - basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by - 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 : {Fermion.altRightMetric | α β}ᵀ.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 end diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean index 5f96839..c4e94b8 100644 --- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean +++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean @@ -100,65 +100,6 @@ lemma antiSymm_add_self {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V} apply TensorTree.add_tensor_eq_snd rw [neg_tensor_eq hA, neg_tensor_eq (neg_perm _ _), neg_neg] -/-! - -## The contraction of Pauli matrices with Pauli matrices - -And related results. - --/ - -/-- 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 - -lemma leftMetric_mul_rightMetric : {Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ.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 - -lemma leftMetric_mul_rightMetric_tree : - {Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ.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_mul_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 end diff --git a/HepLean/Tensors/ComplexLorentz/Metrics/Basic.lean b/HepLean/Tensors/ComplexLorentz/Metrics/Basic.lean new file mode 100644 index 0000000..d6d66d9 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/Metrics/Basic.lean @@ -0,0 +1,162 @@ +/- +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 diff --git a/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean new file mode 100644 index 0000000..37a1e14 --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean @@ -0,0 +1,191 @@ +/- +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 + +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 diff --git a/HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean new file mode 100644 index 0000000..12e6a3b --- /dev/null +++ b/HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean @@ -0,0 +1,79 @@ +/- +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.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 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 + +lemma leftMetric_mul_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 + +lemma leftMetric_mul_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_mul_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 diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean index 879f1dd..8506bf2 100644 --- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean @@ -10,6 +10,7 @@ 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 @@ -41,15 +42,13 @@ open Fermion def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor /-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/ -def pauliCo := {Lorentz.coMetric | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor +def pauliCo := {η' | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor /-- The Pauli matrices as the complex Lorentz tensor `σ_μ_α_{dot β}`. -/ -def pauliCoDown := {pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β'}ᵀ.tensor +def pauliCoDown := {pauliCo | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor /-- The Pauli matrices as the complex Lorentz tensor `σ^μ_α_{dot β}`. -/ -def pauliContrDown := {pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β'}ᵀ.tensor +def pauliContrDown := {pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor /-! @@ -64,19 +63,17 @@ lemma tensorNode_pauliContr : {pauliContr | μ α β}ᵀ.tensor = /-- The definitional tensor node relation for `pauliCo`. -/ lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor = - {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by + {η' | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by rfl /-- The definitional tensor node relation for `pauliCoDown`. -/ lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor = - {pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β'}ᵀ.tensor := by + {pauliCo | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by rfl /-- The definitional tensor node relation for `pauliContrDown`. -/ lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor = - {pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β'}ᵀ.tensor := by + {pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by rfl /-! @@ -88,8 +85,7 @@ lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor = set_option maxRecDepth 5000 in /-- A rearanging of `pauliCoDown` to place the pauli matrices on the right. -/ lemma pauliCoDown_eq_metric_mul_pauliCo : - {pauliCoDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ := by + {pauliCoDown | μ α' β' = εL' | α α' ⊗ εR' | β β' ⊗ pauliCo | μ α β}ᵀ := by conv => lhs rw [tensorNode_pauliCoDown] @@ -138,8 +134,8 @@ lemma pauliCoDown_eq_metric_mul_pauliCo : set_option maxRecDepth 5000 in /-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/ lemma pauliContrDown_eq_metric_mul_pauliContr : - {pauliContrDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗ - Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ := by + {pauliContrDown | μ α' β' = εL' | α α' ⊗ + εR' | β β' ⊗ pauliContr | μ α β}ᵀ := by conv => lhs rw [tensorNode_pauliContrDown] @@ -224,7 +220,7 @@ lemma action_pauliCoDown (g : SL(2,ℂ)) : {g •ₐ pauliCoDown | μ α β}ᵀ. action_pauliCo _] rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] - rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] + erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] rfl /-- The tensor `pauliContrDown` is invariant under the action of `SL(2,ℂ)`. -/ @@ -241,7 +237,7 @@ lemma action_pauliContrDown (g : SL(2,ℂ)) : {g •ₐ pauliContrDown | μ α action_pauliContr _] rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] - rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] + erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _] rfl end complexLorentzTensor diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/CoContractContr.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/CoContractContr.lean index db047a4..085155f 100644 --- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/CoContractContr.lean +++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/CoContractContr.lean @@ -517,8 +517,7 @@ lemma pauliCo_contr_pauliContr_expand : /-- The statement that `η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. -/ theorem pauliCo_contr_pauliContr : - {pauliCo | ν α β ⊗ pauliContr | ν α' β' = - 2 •ₜ Fermion.leftMetric | α α' ⊗ Fermion.rightMetric | β β'}ᵀ := by + {pauliCo | ν α β ⊗ pauliContr | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by rw [pauliCo_contr_pauliContr_expand] rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_mul_rightMetric_tree] rw [perm_smul]