Merge pull request #216 from HEPLean/IndexNotation

feat: Units and informalities

HepLean.lean

@@ -117,6 +117,8 @@ import HepLean.Tensors.ComplexLorentz.Metrics.Lemmas
 import HepLean.Tensors.ComplexLorentz.PauliMatrices.Basic
 import HepLean.Tensors.ComplexLorentz.PauliMatrices.Basis
 import HepLean.Tensors.ComplexLorentz.PauliMatrices.CoContractContr
+import HepLean.Tensors.ComplexLorentz.Units.Basic
+import HepLean.Tensors.ComplexLorentz.Units.Symm
 import HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Discrete
 import HepLean.Tensors.OverColor.Functors

HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean

@@ -4,10 +4,11 @@ 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
 /-!
 
-## Metrics and basis expansions
+## Basic lemmas regarding metrics
 
 -/
 open IndexNotation
@@ -25,11 +26,83 @@ 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
 
-lemma leftMetric_mul_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
+/- 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)
@@ -61,8 +134,8 @@ lemma leftMetric_mul_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
     funext x
     fin_cases x <;> rfl
 
-lemma leftMetric_mul_rightMetric_tree :
-    {εL | α α' ⊗ εR | β β'}ᵀ.tensor
+/- 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
@@ -71,7 +144,7 @@ lemma leftMetric_mul_rightMetric_tree :
         (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]
+  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

HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean

@@ -514,6 +514,7 @@ lemma pauliMatrix_contr_down_3 :
     funext k
     fin_cases k <;> rfl
 
+/-- 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)

HepLean/Tensors/ComplexLorentz/PauliMatrices/CoContractContr.lean

@@ -519,7 +519,7 @@ lemma pauliCo_contr_pauliContr_expand :
 theorem pauliCo_contr_pauliContr :
     {pauliCo | ν α β ⊗ pauliContr | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by
   rw [pauliCo_contr_pauliContr_expand]
-  rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_mul_rightMetric_tree]
+  rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_prod_rightMetric_tree]
   rw [perm_smul]
   /- Moving perm through adds. -/
   rw [smul_tensor_eq <| perm_add _ _ _]

HepLean/Tensors/ComplexLorentz/Units/Basic.lean

@@ -0,0 +1,160 @@
+/-
+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

HepLean/Tensors/ComplexLorentz/Units/Symm.lean

@@ -0,0 +1,63 @@
+/-
+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