Merge pull request #203 from HEPLean/IndexNotation

feat: TensorSpecies

HepLean.lean

@@ -120,6 +120,7 @@ import HepLean.Tensors.Tree.Dot
 import HepLean.Tensors.Tree.Elab
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.ProdComm

HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean

@@ -82,6 +82,10 @@ def contrCoContraction : complexContr ⊗ complexCo ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)
     rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
     simp
 
+lemma contrCoContraction_hom_tmul (ψ : complexContr) (φ : complexCo) :
+    contrCoContraction.hom (ψ ⊗ₜ φ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ := by
+  rfl
+
 /-- The linear map from complexCo ⊗ complexContr to ℂ given by
     summing over components of covariant Lorentz vector and
     contravariant Lorentz vector in the
@@ -96,5 +100,23 @@ def coContrContraction : complexCo ⊗ complexContr ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)
     rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
     simp
 
+lemma coContrContraction_hom_tmul (φ : complexCo) (ψ : complexContr) :
+    coContrContraction.hom (φ ⊗ₜ ψ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ := by
+  rfl
+
+/-!
+
+## Symmetry
+
+-/
+
+lemma contrCoContraction_tmul_symm (φ : complexContr) (ψ : complexCo) :
+    contrCoContraction.hom (φ ⊗ₜ ψ) = coContrContraction.hom (ψ ⊗ₜ φ) := by
+  rw [contrCoContraction_hom_tmul, coContrContraction_hom_tmul, dotProduct_comm]
+
+lemma coContrContraction_tmul_symm (φ : complexCo) (ψ : complexContr) :
+    coContrContraction.hom (φ ⊗ₜ ψ) = contrCoContraction.hom (ψ ⊗ₜ φ) := by
+  rw [contrCoContraction_hom_tmul, coContrContraction_hom_tmul, dotProduct_comm]
+
 end Lorentz
 end

HepLean/SpaceTime/WeylFermion/Contraction.lean

@@ -178,6 +178,10 @@ def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2
     simp only [one_mulVec, vec2_dotProduct, Fin.isValue, RightHandedModule.toFin2ℂEquiv_apply,
       AltRightHandedModule.toFin2ℂEquiv_apply]
 
+lemma rightAltContraction_hom_tmul (ψ : rightHanded) (φ : altRightHanded) :
+    rightAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
+  rfl
+
 /--
   The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
     summing over components of altRightHandedWeyl and rightHandedWeyl in the
@@ -203,63 +207,31 @@ def altRightContraction : altRightHanded ⊗ rightHanded ⟶ 𝟙_ (Rep ℂ SL(2
     simp only [vecMul_one, vec2_dotProduct, Fin.isValue, AltRightHandedModule.toFin2ℂEquiv_apply,
       RightHandedModule.toFin2ℂEquiv_apply]
 
-lemma leftAltContraction_apply_symm (ψ : leftHanded) (φ : altLeftHanded) :
-    leftAltContraction.hom (ψ ⊗ₜ φ) = altLeftContraction.hom (φ ⊗ₜ ψ) := by
-  rw [altLeftContraction_hom_tmul, leftAltContraction_hom_tmul]
-  exact dotProduct_comm ψ.toFin2ℂ φ.toFin2ℂ
+lemma altRightContraction_hom_tmul (φ : altRightHanded) (ψ : rightHanded) :
+    altRightContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
+  rfl
 
-/-- A manifestation of the statement that `ψ ψ' = - ψ' ψ` where `ψ` and `ψ'`
-  are `leftHandedWeyl`. -/
-lemma leftAltContraction_apply_leftHandedAltEquiv (ψ ψ' : leftHanded) :
-    leftAltContraction.hom (ψ ⊗ₜ leftHandedAltEquiv.hom.hom ψ') =
-    - leftAltContraction.hom (ψ' ⊗ₜ leftHandedAltEquiv.hom.hom ψ) := by
-  rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
-    leftHandedAltEquiv_hom_hom_apply, leftHandedAltEquiv_hom_hom_apply]
-  simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
-    CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
-    Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
-    cons_mulVec, cons_dotProduct, zero_mul, one_mul, dotProduct_empty, add_zero, zero_add, neg_mul,
-    empty_mulVec, LinearEquiv.apply_symm_apply, dotProduct_cons, mul_neg, neg_add_rev, neg_neg]
-  ring
+/-!
 
-/-- A manifestation of the statement that `φ φ' = - φ' φ` where `φ` and `φ'` are
-  `altLeftHandedWeyl`. -/
-lemma leftAltContraction_apply_leftHandedAltEquiv_inv (φ φ' : altLeftHanded) :
-    leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ ⊗ₜ φ') =
-    - leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ' ⊗ₜ φ) := by
-  rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
-    leftHandedAltEquiv_inv_hom_apply, leftHandedAltEquiv_inv_hom_apply]
-  simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
-    CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
-    Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
-    cons_mulVec, cons_dotProduct, zero_mul, neg_mul, one_mul, dotProduct_empty, add_zero, zero_add,
-    empty_mulVec, LinearEquiv.apply_symm_apply, neg_add_rev, neg_neg]
-  ring
+## Symmetry properties
 
-informal_lemma leftAltWeylContraction_symm_altLeftWeylContraction where
-  math :≈ "The linear map altLeftWeylContraction is leftAltWeylContraction composed
-    with the braiding of the tensor product."
-  deps :≈ [``leftAltContraction, ``altLeftContraction]
+-/
 
-informal_lemma altLeftWeylContraction_invariant where
-  math :≈ "The contraction altLeftWeylContraction is invariant with respect to
-    the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl."
-  deps :≈ [``altLeftContraction]
+lemma leftAltContraction_tmul_symm (ψ : leftHanded) (φ : altLeftHanded) :
+    leftAltContraction.hom (ψ ⊗ₜ[ℂ] φ) = altLeftContraction.hom (φ ⊗ₜ[ℂ] ψ) := by
+  rw [leftAltContraction_hom_tmul, altLeftContraction_hom_tmul, dotProduct_comm]
 
-informal_lemma rightAltWeylContraction_invariant where
-  math :≈ "The contraction rightAltWeylContraction is invariant with respect to
-    the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
-  deps :≈ [``rightAltContraction]
+lemma altLeftContraction_tmul_symm (φ : altLeftHanded) (ψ : leftHanded) :
+    altLeftContraction.hom (φ ⊗ₜ[ℂ] ψ) = leftAltContraction.hom (ψ ⊗ₜ[ℂ] φ) := by
+  rw [leftAltContraction_tmul_symm]
 
-informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
-  math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
-    with the braiding of the tensor product."
-  deps :≈ [``rightAltContraction, ``altRightContraction]
+lemma rightAltContraction_tmul_symm (ψ : rightHanded) (φ : altRightHanded) :
+    rightAltContraction.hom (ψ ⊗ₜ[ℂ] φ) = altRightContraction.hom (φ ⊗ₜ[ℂ] ψ) := by
+  rw [rightAltContraction_hom_tmul, altRightContraction_hom_tmul, dotProduct_comm]
 
-informal_lemma altRightWeylContraction_invariant where
-  math :≈ "The contraction altRightWeylContraction is invariant with respect to
-    the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
-  deps :≈ [``altRightContraction]
+lemma altRightContraction_tmul_symm (φ : altRightHanded) (ψ : rightHanded) :
+    altRightContraction.hom (φ ⊗ₜ[ℂ] ψ) = rightAltContraction.hom (ψ ⊗ₜ[ℂ] φ) := by
+  rw [rightAltContraction_tmul_symm]
 
 end
 end Fermion

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -81,7 +81,7 @@ instance : DecidableEq Color := fun x y =>
 noncomputable section
 
 /-- The tensor structure for complex Lorentz tensors. -/
-def complexLorentzTensor : TensorStruct where
+def complexLorentzTensor : TensorSpecies where
   C := Fermion.Color
   G := SL(2, ℂ)
   G_group := inferInstance
@@ -143,6 +143,14 @@ def complexLorentzTensor : TensorStruct where
     | Color.downR => 2
     | Color.up => 4
     | Color.down => 4
+  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
 
 instance : DecidableEq complexLorentzTensor.C := Fermion.instDecidableEqColor
 

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -9,6 +9,8 @@ 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
 /-!
 
@@ -59,7 +61,7 @@ lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
 lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ := by
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, perm_tensor]
   rw [coMetric_expand]
-  simp only [TensorStruct.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
+  simp only [TensorSpecies.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
     map_sub]
   congr 1
   congr 1
@@ -72,6 +74,37 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
     | (0 : Fin 2) => rfl
     | (1 : Fin 2) => rfl
 
+set_option maxRecDepth 20000 in
+lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
+    {T2 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V} :
+    {(T1 | μ ν ⊗ T2 | μ ν) = (T2 | μ ν ⊗ T1 | μ ν)}ᵀ := by
+  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 (perm_contr _ _)]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  · rw [(contr_tensor_eq (contr_swap _ _))]
+    rw [perm_contr]
+    rw [perm_tensor_eq (contr_swap _ _)]
+    rw [perm_perm]
+    rw [perm_eq_id]
+    · rfl
+    · apply OverColor.Hom.ext
+      rfl
+  · apply OverColor.Hom.ext
+    ext x
+    exact Fin.elim0 x
+
+lemma contr_rank_2_symm' {T1 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
+    {T2 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V} :
+    {(T1 | μ ν ⊗ T2 | μ ν) = (T2 | μ ν ⊗ T1 | μ ν)}ᵀ := by
+  rw [perm_tensor_eq contr_rank_2_symm]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  apply OverColor.Hom.ext
+  ext x
+  exact Fin.elim0 x
+
 set_option maxRecDepth 20000 in
 /-- Contracting a rank-2 anti-symmetric tensor with a rank-2 symmetric tensor gives zero. -/
 lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
@@ -102,8 +135,16 @@ lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V
   rw [perm_perm]
   rw [perm_eq_id]
   · rfl
-  · apply OverColor.Hom.ext
-    rfl
+  · rfl
+
+lemma symm_contr_antiSymm {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
+    {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
+    (hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
+    {S | μ ν ⊗ A | μ ν}ᵀ.tensor = 0 := by
+  rw [contr_rank_2_symm']
+  rw [perm_tensor]
+  rw [antiSymm_contr_symm hA hs]
+  rfl
 
 end Fermion
 

HepLean/Tensors/Tree/Basic.lean

@@ -18,9 +18,8 @@ open CategoryTheory
 open MonoidalCategory
 
 /-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
-  complex Lorentz tensors.
-  Note: This structure is not fully defined yet. -/
-structure TensorStruct where
+  complex Lorentz tensors. -/
+structure TensorSpecies where
   /-- The colors of indices e.g. up or down. -/
   C : Type
   /-- The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ). -/
@@ -36,6 +35,7 @@ structure TensorStruct where
   FDiscrete : Discrete C ⥤ Rep k G
   /-- A map from `C` to `C`. An involution. -/
   τ : C → C
+  /-- The condition that `τ` is an involution. -/
   τ_involution : Function.Involutive τ
   /-- The natural transformation describing contraction. -/
   contr : OverColor.Discrete.pairτ FDiscrete τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
@@ -46,13 +46,18 @@ structure TensorStruct where
   /-- A specification of the dimension of each color in C. This will be used for explicit
     evaluation of tensors. -/
   evalNo : C → ℕ
+  /-- Contraction is symmetric with respect to duals. -/
+  contr_tmul_symm (c : C) (x : FDiscrete.obj (Discrete.mk c))
+      (y : FDiscrete.obj (Discrete.mk (τ c))) :
+    (contr.app (Discrete.mk c)).hom (x ⊗ₜ[k] y) = (contr.app (Discrete.mk (τ c))).hom
+      (y ⊗ₜ (FDiscrete.map (Discrete.eqToHom (τ_involution c).symm)).hom x)
 
 noncomputable section
 
-namespace TensorStruct
+namespace TensorSpecies
 open OverColor
 
-variable (S : TensorStruct)
+variable (S : TensorSpecies)
 
 instance : CommRing S.k := S.k_commRing
 
@@ -349,10 +354,10 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
       simp
     exact h1' h1
 
-end TensorStruct
+end TensorSpecies
 
 /-- A syntax tree for tensor expressions. -/
-inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
+inductive TensorTree (S : TensorSpecies) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
   /-- A general tensor node. -/
   | tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c
   /-- A node consisting of a single vector. -/
@@ -398,23 +403,23 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
 
 namespace TensorTree
 
-variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
+variable {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
 
 open MonoidalCategory
 open TensorProduct
 
 /-- The node `twoNode` of a tensor tree, with all arguments explicit. -/
-abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C)
+abbrev twoNodeE (S : TensorSpecies) (c1 c2 : S.C)
     (v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
     TensorTree S ![c1, c2] := twoNode v
 
 /-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
-abbrev constTwoNodeE (S : TensorStruct) (c1 c2 : S.C)
+abbrev constTwoNodeE (S : TensorSpecies) (c1 c2 : S.C)
     (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
     TensorTree S ![c1, c2] := constTwoNode v
 
 /-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/
-abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C)
+abbrev constThreeNodeE (S : TensorSpecies) (c1 c2 c3 : S.C)
     (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
       S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] :=
     constThreeNode v
@@ -443,6 +448,7 @@ noncomputable section
   Note: This function is not fully defined yet. -/
 def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (OverColor.mk c) := fun
   | tensorNode t => t
+  | twoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom t
   | constTwoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (t.hom (1 : S.k))
   | add t1 t2 => t1.tensor + t2.tensor
   | perm σ t => (S.F.map σ).hom t.tensor
@@ -523,6 +529,32 @@ lemma perm_tensor_eq {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
   simp only [perm_tensor]
   rw [h]
 
+/-- A structure containing a pair of indices (i, j) to be contracted in a tensor.
+  This is used in some proofs of node identities for tensor trees. -/
+structure ContrPair {n : ℕ} (c : Fin n.succ.succ → S.C) where
+  /-- The first index in the pair, appearing on the left in the contraction
+    node `contr i j h _`. -/
+  i : Fin n.succ.succ
+  /-- The second index in the pair, appearing on the right in the contraction
+    node `contr i j h _`. -/
+  j : Fin n.succ
+  /-- A proof that the two indices can be contracted. -/
+  h : c (i.succAbove j) = S.τ (c i)
+
+namespace ContrPair
+variable {n : ℕ} {c : Fin n.succ.succ → S.C} {q q' : ContrPair c}
+
+lemma ext (hi : q.i = q'.i) (hj : q.j = q'.j) : q = q' := by
+  cases q
+  cases q'
+  subst hi
+  subst hj
+  rfl
+
+/-- The contraction map for a pair of indices. -/
+def contrMap := S.contrMap c q.i q.j q.h
+
+end ContrPair
 end
 
 end TensorTree

HepLean/Tensors/Tree/Elab.lean

@@ -487,7 +487,7 @@ elab_rules (kind:=tensorExprSyntax) : term
     let tensorTree ← elaborateTensorNode e
     return tensorTree
 
-variable {S : TensorStruct} {c4 : Fin 4 → S.C} (T4 : S.F.obj (OverColor.mk c4))
+variable {S : TensorSpecies} {c4 : Fin 4 → S.C} (T4 : S.F.obj (OverColor.mk c4))
   {c5 : Fin 5 → S.C} (T5 : S.F.obj (OverColor.mk c5)) (a : S.k)
 
 variable (𝓣 : TensorTree S c4)

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -22,7 +22,7 @@ open TensorProduct
 
 namespace TensorTree
 
-variable {S : TensorStruct}
+variable {S : TensorSpecies}
 
 /-!