refactor: Complex lorentz tensor lemmas
This commit is contained in:
jstoobysmith
parent
ba0cdd3897
commit
aae24f3df7
2 changed files with 30 additions and 82 deletions
|
|
@ -4,6 +4,7 @@ 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.
|
||||
|
|
@ -23,82 +24,28 @@ open OverColor.Discrete
|
|||
noncomputable section
|
||||
|
||||
namespace complexLorentzTensor
|
||||
open Fermion
|
||||
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 _ _)]
|
||||
|
||||
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 1]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
rw [perm_eq_id]
|
||||
· rfl
|
||||
· 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}
|
||||
{S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
|
||||
(hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
|
||||
{A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
|
||||
have h1 {M : Type} [AddCommGroup M] [Module ℂ M] {x : M} (h : x = - x) : x = 0 := by
|
||||
rw [eq_neg_iff_add_eq_zero, ← two_smul ℂ x] at h
|
||||
simpa using h
|
||||
refine h1 ?_
|
||||
rw [← neg_tensor]
|
||||
rw [neg_perm] at hA
|
||||
nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
|
||||
nth_rewrite 1 [(contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_snd hs)))]
|
||||
rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
|
||||
rw [contr_tensor_eq (neg_contr _)]
|
||||
rw [neg_contr]
|
||||
rw [neg_tensor]
|
||||
apply congrArg
|
||||
rw [contr_tensor_eq (contr_tensor_eq (prod_perm_left _ _ _ _))]
|
||||
rw [contr_tensor_eq (perm_contr _ _)]
|
||||
rw [perm_contr]
|
||||
rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
|
||||
rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
|
||||
rw [perm_tensor_eq (perm_contr _ _)]
|
||||
rw [perm_perm]
|
||||
nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
|
||||
rw [perm_perm]
|
||||
rw [perm_eq_id]
|
||||
· 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', perm_tensor, antiSymm_contr_symm hA hs]
|
||||
rfl
|
||||
|
||||
lemma antiSymm_add_self {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
|
||||
(hA : {A | μ ν = - (A | ν μ)}ᵀ) :
|
||||
{A | μ ν + A | ν μ}ᵀ.tensor = 0 := by
|
||||
rw [← TensorTree.add_neg (twoNodeE complexLorentzTensor Color.up Color.up A)]
|
||||
apply TensorTree.add_tensor_eq_snd
|
||||
rw [neg_tensor_eq hA, neg_tensor_eq (neg_perm _ _), neg_neg]
|
||||
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
|
||||
|
||||
|
|
|
|||
|
|
@ -551,7 +551,7 @@ lemma evalMap_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin
|
|||
end TensorSpecies
|
||||
|
||||
/-- A syntax tree for tensor expressions. -/
|
||||
inductive TensorTree (S : TensorSpecies) : ∀ {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 corresponding to the addition of two tensors. -/
|
||||
|
|
@ -559,20 +559,21 @@ inductive TensorTree (S : TensorSpecies) : ∀ {n : ℕ}, (Fin n → S.C) → Ty
|
|||
/-- A node corresponding to the permutation of indices of a tensor. -/
|
||||
| perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) : TensorTree S c1
|
||||
/-- A node corresponding to the product of two tensors. -/
|
||||
| prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ finSumFinEquiv.symm)
|
||||
/-- A node correpsonding to the scalar multiple of a tensor by a element of the field. -/
|
||||
| smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
|
||||
/-- The negative of a node. -/
|
||||
/-- A node corresponding to negation of a tensor. -/
|
||||
| neg {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c
|
||||
/-- The contraction of indices. -/
|
||||
/-- A node corresponding to the contraction of indices of a tensor. -/
|
||||
| contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
|
||||
(j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
|
||||
TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
|
||||
/-- The group action on a tensor. -/
|
||||
/-- A node correpsonding to the action of a group element on a tensor. -/
|
||||
| action {n : ℕ} {c : Fin n → S.C} : S.G → TensorTree S c → TensorTree S c
|
||||
/-- The evaluation of an index-/
|
||||
| eval {n : ℕ} {c : Fin n.succ → S.C} :
|
||||
(i : Fin n.succ) → (x : ℕ) → TensorTree S c →
|
||||
/-- A node corresponding to the evaluation of an index of a tensor. -/
|
||||
| eval {n : ℕ} {c : Fin n.succ → S.C} : (i : Fin n.succ) → (x : ℕ) → TensorTree S c →
|
||||
TensorTree S (c ∘ Fin.succAbove i)
|
||||
|
||||
namespace TensorTree
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue