feat: Contractions with pauli matrices
This commit is contained in:
jstoobysmith
parent
ca55da6a34
commit
685c1b293c
4 changed files with 940 additions and 81 deletions
|
|
@ -98,6 +98,34 @@ lemma contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.
|
|||
erw [basis_contr]
|
||||
rfl
|
||||
|
||||
lemma contr_basisVector_tree {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
|
||||
(contr i j h (tensorNode (basisVector c b))).tensor =
|
||||
(smul ((if (b i).val = (b (i.succAbove j)).val
|
||||
then (1 : ℂ) else 0)) (tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
|
||||
(fun k => b (i.succAbove (j.succAbove k)))) )).tensor := by
|
||||
exact contr_basisVector _
|
||||
|
||||
lemma contr_basisVector_tree_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : (b i).val = (b (i.succAbove j)).val := by decide) :
|
||||
(contr i j h (tensorNode (basisVector c b))).tensor =
|
||||
((tensorNode ( basisVector (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
|
||||
(fun k => b (i.succAbove (j.succAbove k)))))).tensor := by
|
||||
rw [contr_basisVector_tree]
|
||||
rw [if_pos hn]
|
||||
simp [smul_tensor]
|
||||
|
||||
lemma contr_basisVector_tree_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)}
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) (hn : ¬ (b i).val = (b (i.succAbove j)).val := by decide) :
|
||||
(contr i j h (tensorNode (basisVector c b))).tensor =
|
||||
(tensorNode 0).tensor := by
|
||||
rw [contr_basisVector_tree]
|
||||
rw [if_neg hn]
|
||||
simp [smul_tensor]
|
||||
|
||||
def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
{c1 : Fin m → complexLorentzTensor.C} (i : Fin n ⊕ Fin m) :
|
||||
Sum.elim (fun i => Fin (complexLorentzTensor.repDim (c i))) (fun i => Fin (complexLorentzTensor.repDim (c1 i)))
|
||||
|
|
@ -135,6 +163,16 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
|
|||
| Sum.inl k => rfl
|
||||
| Sum.inr k => rfl
|
||||
|
||||
lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
{c1 : Fin m → complexLorentzTensor.C}
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k)))
|
||||
(b1 : Π k, Fin (complexLorentzTensor.repDim (c1 k))) :
|
||||
(prod (tensorNode (basisVector c b)) (tensorNode (basisVector c1 b1))).tensor =
|
||||
(tensorNode (basisVector (Sum.elim c c1 ∘ finSumFinEquiv.symm) (fun i =>
|
||||
prodBasisVecEquiv (finSumFinEquiv.symm i)
|
||||
((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
|
||||
exact prod_basisVector _ _
|
||||
|
||||
lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
|
||||
{i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i)))
|
||||
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) :
|
||||
|
|
@ -183,6 +221,13 @@ lemma coMetric_basis_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
|
|||
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)
|
||||
|
|
@ -208,6 +253,13 @@ lemma contrMatrix_basis_expand : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
|
|||
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
|
||||
|
|
@ -225,6 +277,11 @@ lemma leftMetric_expand : {Fermion.leftMetric | α β}ᵀ.tensor =
|
|||
· 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
|
||||
|
|
@ -241,6 +298,11 @@ lemma altLeftMetric_expand : {Fermion.altLeftMetric | α β}ᵀ.tensor =
|
|||
· 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
|
||||
|
|
@ -258,6 +320,11 @@ lemma rightMetric_expand : {Fermion.rightMetric | α β}ᵀ.tensor =
|
|||
· 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
|
||||
|
|
@ -274,6 +341,11 @@ lemma altRightMetric_expand : {Fermion.altRightMetric | α β}ᵀ.tensor =
|
|||
· 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
|
||||
|
||||
/-- The expansion of the Pauli matrices `σ^μ^a^{dot a}` in terms of basis vectors. -/
|
||||
lemma pauliMatrix_basis_expand : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
|
||||
basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
|
|
@ -312,6 +384,27 @@ lemma pauliMatrix_basis_expand : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
|
|||
| (1 : Fin 3) => rfl
|
||||
| (2 : Fin 3) => rfl
|
||||
|
||||
lemma pauliMatrix_basis_expand_tree : {PauliMatrix.asConsTensor | μ α β}ᵀ.tensor =
|
||||
(TensorTree.add (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0))) <|
|
||||
TensorTree.add (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 1 | 2 => 1))) <|
|
||||
TensorTree.add (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 0 | 2 => 1))) <|
|
||||
TensorTree.add (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 1 | 2 => 0))) <|
|
||||
TensorTree.add (smul (-I) (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 0 | 2 => 1)))) <|
|
||||
TensorTree.add (smul I (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 1 | 2 => 0)))) <|
|
||||
TensorTree.add (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 0 | 2 => 0))) <|
|
||||
(smul (-1) (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 1 | 2 => 1))))).tensor := by
|
||||
rw [pauliMatrix_basis_expand]
|
||||
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 Fermion
|
||||
|
|
|
|||
|
|
@ -12,6 +12,8 @@ import HepLean.Tensors.Tree.NodeIdentities.PermContr
|
|||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
||||
import HepLean.Tensors.ComplexLorentz.Basis
|
||||
import LLMLean
|
||||
/-!
|
||||
|
||||
## Lemmas related to complex Lorentz tensors.
|
||||
|
|
@ -32,86 +34,6 @@ noncomputable section
|
|||
|
||||
namespace Fermion
|
||||
|
||||
/-- The vectors forming a basis of
|
||||
`complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down])`.
|
||||
Not proved it is a basis yet. -/
|
||||
def coCoBasis (b : Fin 4 × Fin 4) :
|
||||
complexLorentzTensor.F.obj (OverColor.mk ![Color.down, Color.down]) :=
|
||||
PiTensorProduct.tprod ℂ (fun i => Fin.cases (Lorentz.complexCoBasisFin4 b.1)
|
||||
(fun i => Fin.cases (Lorentz.complexCoBasisFin4 b.2) (fun i => i.elim0) i) i)
|
||||
|
||||
lemma coCoBasis_eval (e1 e2 : Fin (complexLorentzTensor.repDim Color.down)) (i : Fin 4 × Fin 4) :
|
||||
complexLorentzTensor.castFin0ToField
|
||||
((complexLorentzTensor.evalMap 0 e2) ((complexLorentzTensor.evalMap 0 e1) (coCoBasis i))) =
|
||||
if i = (e1, e2) then 1 else 0 := by
|
||||
simp only [coCoBasis]
|
||||
have h1 := @TensorSpecies.evalMap_tprod complexLorentzTensor _ (![Color.down, Color.down]) 0 e1
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Functor.id_obj,
|
||||
OverColor.mk_hom, Function.comp_apply, cons_val_zero, Fin.cases_zero, Fin.cases_succ] at h1
|
||||
erw [h1]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Functor.id_obj, OverColor.mk_hom,
|
||||
Fin.cases_zero, Fin.cases_succ, _root_.map_smul, smul_eq_mul]
|
||||
erw [TensorSpecies.evalMap_tprod]
|
||||
simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.succAbove_zero, Functor.id_obj,
|
||||
OverColor.mk_hom, Function.comp_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons,
|
||||
Fin.cases_zero, Fin.zero_succAbove, Fin.cases_succ, _root_.map_smul, smul_eq_mul]
|
||||
erw [complexLorentzTensor.castFin0ToField_tprod]
|
||||
simp only [Fin.isValue, mul_one]
|
||||
change (Lorentz.complexCoBasisFin4.repr (Lorentz.complexCoBasisFin4 i.1)) e1 *
|
||||
(Lorentz.complexCoBasisFin4.repr (Lorentz.complexCoBasisFin4 i.2)) e2 = _
|
||||
simp only [Basis.repr_self]
|
||||
rw [Finsupp.single_apply, Finsupp.single_apply]
|
||||
rw [@ite_zero_mul_ite_zero]
|
||||
simp only [mul_one]
|
||||
congr
|
||||
simp_all only [Fin.isValue, Fin.succAbove_zero, Fin.zero_succAbove, eq_iff_iff]
|
||||
obtain ⟨fst, snd⟩ := i
|
||||
simp_all only [Fin.isValue, Prod.mk.injEq]
|
||||
|
||||
lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
|
||||
coCoBasis (0, 0) - coCoBasis (1, 1) - coCoBasis (2, 2) - coCoBasis (3, 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, coCoBasis]
|
||||
simp only [Nat.reduceAdd, Nat.succ_eq_add_one, OverColor.mk_hom, Functor.id_obj, Fin.isValue,
|
||||
Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
/-- The covariant Lorentz metric is symmetric. -/
|
||||
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 [TensorSpecies.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
|
||||
map_sub]
|
||||
simp only [coCoBasis, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, OverColor.mk_hom,
|
||||
Lorentz.complexCoBasisFin4, Fin.isValue, Basis.coe_reindex, Function.comp_apply]
|
||||
congr 1
|
||||
congr 1
|
||||
congr 1
|
||||
all_goals
|
||||
erw [OverColor.lift.map_tprod]
|
||||
congr 1
|
||||
funext i
|
||||
match i with
|
||||
| (0 : Fin 2) => rfl
|
||||
| (1 : Fin 2) => rfl
|
||||
|
||||
lemma coMetric_0_0_field : {Lorentz.coMetric | 0 0}ᵀ.field = 1 := by
|
||||
rw [field, eval_tensor, eval_tensor, coMetric_expand]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue,
|
||||
Function.comp_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons, Fin.ofNat'_zero,
|
||||
cons_val_zero, Functor.id_obj, OverColor.mk_hom, map_sub]
|
||||
rw [coCoBasis_eval, coCoBasis_eval, coCoBasis_eval, coCoBasis_eval]
|
||||
simp only [Fin.isValue, Prod.mk_zero_zero, ↓reduceIte, Prod.mk_one_one, one_ne_zero, sub_zero,
|
||||
Prod.mk_eq_zero, Fin.reduceEq, and_self]
|
||||
|
||||
set_option maxRecDepth 20000 in
|
||||
lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
|
||||
{T2 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V} :
|
||||
|
|
@ -188,6 +110,785 @@ 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.
|
||||
|
||||
-/
|
||||
open complexLorentzTensor
|
||||
|
||||
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
|
||||
|
||||
|
||||
def pauliMatrixLowerMap := ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
|
||||
Fin.succAbove 0 ∘ Fin.succAbove 1)
|
||||
|
||||
abbrev pauliMatrixContrMap {n : ℕ} (c : Fin n → complexLorentzTensor.C) := (Sum.elim c ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm)
|
||||
|
||||
lemma pauliMatrix_contr_expand {n : ℕ} {c : Fin n → complexLorentzTensor.C}
|
||||
(t : TensorTree complexLorentzTensor c) (i : Fin (n + 3)) (j : Fin (n +2))
|
||||
(h : (pauliMatrixContrMap c) (i.succAbove j) = complexLorentzTensor.τ ((pauliMatrixContrMap c) i)) :
|
||||
(contr i j h (TensorTree.prod t (constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor))).tensor = (
|
||||
(contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 0 | 2 => 0)))).add
|
||||
((contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 0 | 1 => 1 | 2 => 1)))).add
|
||||
((contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 0 | 2 => 1)))).add
|
||||
((contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 1 | 1 => 1 | 2 => 0)))).add
|
||||
((TensorTree.smul (-I) (contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 0 | 2 => 1))))).add
|
||||
((TensorTree.smul I (contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 2 | 1 => 1 | 2 => 0))))).add
|
||||
((contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 0 | 2 => 0)))).add
|
||||
(TensorTree.smul (-1) (contr i j h (t.prod (tensorNode
|
||||
(basisVector ![Color.up, Color.upL, Color.upR] fun | 0 => 3 | 1 => 1 | 2 => 1)))))))))))).tensor := by
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree]
|
||||
rw [contr_tensor_eq <| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| prod_add _ _ _]
|
||||
/- Moving smuls. -/
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _]
|
||||
rw [contr_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd<| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| prod_smul _ _ _]
|
||||
/- Moving contr over add. -/
|
||||
rw [contr_add]
|
||||
rw [add_tensor_eq_snd <| contr_add _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| contr_add _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _]
|
||||
/- Moving contr over smul. -/
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
contr_smul _ _]
|
||||
rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_0 :
|
||||
(contr 0 1 rfl (((tensorNode (basisVector ![Color.down, Color.down] fun x => 0)).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor
|
||||
= basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_pos _ rfl]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ rfl]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_1 : (contr 0 1 rfl
|
||||
(((tensorNode (basisVector ![Color.down, Color.down] fun x => 1)).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor
|
||||
= basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_pos _ rfl]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_pos _ rfl]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_2 : (contr 0 1 rfl
|
||||
(((tensorNode (basisVector ![Color.down, Color.down] fun x => 2)).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor
|
||||
= (- I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
|
||||
+ (I) • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_down_3 : (contr 0 1 rfl
|
||||
(((tensorNode (basisVector ![Color.down, Color.down] fun x => 3)).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor
|
||||
= basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
|
||||
+ (- 1 : ℂ) • basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
def pauliMatrixContrPauliMatrixMap := ((Sum.elim
|
||||
((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘
|
||||
Fin.succAbove 0 ∘ Fin.succAbove 1)
|
||||
![Color.up, Color.upL, Color.upR] ∘
|
||||
⇑finSumFinEquiv.symm) ∘
|
||||
Fin.succAbove 0 ∘ Fin.succAbove 2)
|
||||
|
||||
lemma pauliMatrix_contr_lower_0_0_0 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor = basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_lower_0_1_1 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor = basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
|
||||
lemma pauliMatrix_contr_lower_1_0_1 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor = basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_pos _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_lower_1_1_0 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor = basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_pos _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_lower_2_0_1 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor =
|
||||
(-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
+ (I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
lemma pauliMatrix_contr_lower_2_1_0 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor =
|
||||
(-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ (I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
|
||||
lemma pauliMatrix_contr_lower_3_0_0 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0)
|
||||
+ (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
|
||||
lemma pauliMatrix_contr_lower_3_1_1 : (contr 0 2 rfl
|
||||
(((tensorNode (basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1))).prod
|
||||
(constThreeNodeE complexLorentzTensor Color.up Color.upL Color.upR
|
||||
PauliMatrix.asConsTensor)))).tensor =
|
||||
basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0)
|
||||
+ (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by
|
||||
rw [pauliMatrix_contr_expand]
|
||||
/- Product of basis vectors . -/
|
||||
rw [add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_tensor_eq
|
||||
<| prod_basisVector_tree _ _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| smul_tensor_eq
|
||||
<| contr_tensor_eq <| prod_basisVector_tree _ _]
|
||||
/- Contracting basis vectors. -/
|
||||
rw [add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst
|
||||
<| contr_basisVector_tree_neg _ ]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_fst <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <|add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq
|
||||
<| contr_basisVector_tree_neg _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd
|
||||
<| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_basisVector_tree_pos _]
|
||||
rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <|
|
||||
smul_tensor_eq <| contr_basisVector_tree_pos _]
|
||||
/- Simplifying. -/
|
||||
simp only [smul_tensor, add_tensor, tensorNode_tensor]
|
||||
simp only [smul_zero, add_zero, zero_add]
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
|
||||
|
||||
|
||||
/-
|
||||
lemma pauliMatrix_lower :
|
||||
{Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β}ᵀ.tensor
|
||||
= basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 0 | 2 => 0)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 0 | 1 => 1 | 2 => 1)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 0 | 2 => 1)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 1 | 1 => 1 | 2 => 0)
|
||||
- I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 0 | 2 => 1)
|
||||
+ I • basisVector pauliMatrixLowerMap (fun | 0 => 2 | 1 => 1 | 2 => 0)
|
||||
+ basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 0 | 2 => 0)
|
||||
- basisVector pauliMatrixLowerMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_fst <| coMetric_basis_expand_tree]
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| pauliMatrix_basis_expand_tree]
|
||||
|
||||
sorry -/
|
||||
|
||||
|
||||
lemma pauliMatrix_contract_pauliMatrix :
|
||||
{Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ.tensor
|
||||
= basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
|
||||
- basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
|
||||
- basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)
|
||||
+ basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by
|
||||
|
||||
end Fermion
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -679,6 +679,8 @@ lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
|
|||
lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t : TensorTree S c) :
|
||||
(eval i e t).tensor = (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor := rfl
|
||||
|
||||
lemma smul_tensor {c : Fin n → S.C} (a : S.k) (T : TensorTree S c) :
|
||||
(smul a T).tensor = a • T.tensor:= rfl
|
||||
/-!
|
||||
|
||||
## Equality of tensors and rewrites.
|
||||
|
|
@ -737,6 +739,11 @@ lemma neg_tensor_eq {T1 T2 : TensorTree S c} (h : T1.tensor = T2.tensor) :
|
|||
simp only [neg_tensor]
|
||||
rw [h]
|
||||
|
||||
lemma smul_tensor_eq {T1 T2 : TensorTree S c} {a : S.k} (h : T1.tensor = T2.tensor) :
|
||||
(smul a T1).tensor = (smul a T2).tensor := by
|
||||
simp only [smul_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
|
||||
|
|
|
|||
|
|
@ -117,12 +117,26 @@ lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
|
||||
/-!
|
||||
|
||||
## Additive identities
|
||||
## Vector based identities
|
||||
|
||||
These identities are related to the fact that all the maps are linear.
|
||||
|
||||
-/
|
||||
|
||||
lemma smul_smul (t : TensorTree S c) (a b : S.k) :
|
||||
(smul a (smul b t)).tensor = (smul (a * b) t).tensor := by
|
||||
simp [smul_tensor]
|
||||
exact _root_.smul_smul a b t.tensor
|
||||
|
||||
lemma smul_one (t : TensorTree S c) :
|
||||
(smul 1 t).tensor = t.tensor := by
|
||||
simp [smul_tensor]
|
||||
|
||||
lemma smul_eq_one (t : TensorTree S c) (a : S.k) (h : a = 1) :
|
||||
(smul a t).tensor = t.tensor := by
|
||||
rw [h]
|
||||
exact smul_one _
|
||||
|
||||
/-- The addition node is commutative. -/
|
||||
lemma add_comm (t1 t2 : TensorTree S c) : (add t1 t2).tensor = (add t2 t1).tensor := by
|
||||
simp only [add_tensor]
|
||||
|
|
@ -147,4 +161,48 @@ lemma add_eval {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t
|
|||
(add (eval i e t) (eval i e t1)).tensor = (eval i e (add t t1)).tensor := by
|
||||
simp only [add_tensor, eval_tensor, Nat.succ_eq_add_one, map_add]
|
||||
|
||||
lemma contr_add {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)} (t1 t2 : TensorTree S c) :
|
||||
(contr i j h (add t1 t2)).tensor = (add (contr i j h t1) (contr i j h t2)).tensor := by
|
||||
simp [contr_tensor, add_tensor]
|
||||
|
||||
lemma contr_smul {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)} (a : S.k) (t : TensorTree S c) :
|
||||
(contr i j h (smul a t)).tensor = (smul a (contr i j h t)).tensor := by
|
||||
simp [contr_tensor, smul_tensor]
|
||||
|
||||
@[simp]
|
||||
lemma add_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 t2 : TensorTree S c) (t3 : TensorTree S c1) :
|
||||
(prod (add t1 t2) t3).tensor = (add (prod t1 t3) (prod t2 t3)).tensor := by
|
||||
simp only [prod_tensor, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, add_tmul, map_add]
|
||||
|
||||
@[simp]
|
||||
lemma prod_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 : TensorTree S c) (t2 t3 : TensorTree S c1) :
|
||||
(prod t1 (add t2 t3)).tensor = (add (prod t1 t2) (prod t1 t3)).tensor := by
|
||||
simp only [prod_tensor, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, tmul_add, map_add]
|
||||
|
||||
lemma smul_prod {n m: ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
|
||||
((prod (smul a t1) t2)).tensor = (smul a (prod t1 t2)).tensor := by
|
||||
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
|
||||
|
||||
lemma prod_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
|
||||
(prod t1 (smul a t2)).tensor = (smul a (prod t1 t2)).tensor := by
|
||||
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
|
||||
|
||||
lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 t2 : TensorTree S c) (t3 t4 : TensorTree S c1) :
|
||||
(prod (add t1 t2) (add t3 t4)).tensor = (add (add (prod t1 t3) (prod t1 t4))
|
||||
(add (prod t2 t3) (prod t2 t4))).tensor := by
|
||||
rw [add_prod]
|
||||
rw [add_tensor_eq_fst (prod_add _ _ _)]
|
||||
rw [add_tensor_eq_snd (prod_add _ _ _)]
|
||||
|
||||
end TensorTree
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue