feat: Add expansion of Pauli matrices as basis vect

HepLean/SpaceTime/PauliMatrices/AsTensor.lean

@@ -35,6 +35,76 @@ open SpaceTime
 def asTensor : (complexContr ⊗ leftHanded ⊗ rightHanded).V :=
   ∑ i, complexContrBasis i ⊗ₜ leftRightToMatrix.symm (σSA i)
 
+/-- The expansion of `asTensor` into complexContrBasis basis vectors . -/
+lemma asTensor_expand_complexContrBasis : asTensor =
+    complexContrBasis (Sum.inl 0) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inl 0))
+    + complexContrBasis (Sum.inr 0) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 0))
+    + complexContrBasis (Sum.inr 1) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 1))
+    + complexContrBasis (Sum.inr 2) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 2)) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, asTensor,
+    CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, Fintype.sum_sum_type, Finset.univ_unique,
+    Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three]
+  rfl
+
+/-- The expansion of the pauli matrix `σ₀` in terms of a basis of tensor product vectors. -/
+lemma leftRightToMatrix_σSA_inl_0_expand : leftRightToMatrix.symm (σSA (Sum.inl 0)) =
+    leftBasis 0 ⊗ₜ rightBasis 0 + leftBasis 1 ⊗ₜ rightBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Fin.isValue]
+  erw [leftRightToMatrix_symm_expand_tmul]
+  simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', σ0, of_apply, cons_val', empty_val',
+    cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, head_cons, one_smul, zero_smul,
+    add_zero, head_fin_const, zero_add, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
+
+  /-- The expansion of the pauli matrix `σ₁` in terms of a basis of tensor product vectors. -/
+lemma leftRightToMatrix_σSA_inr_0_expand : leftRightToMatrix.symm (σSA (Sum.inr 0)) =
+    leftBasis 0 ⊗ₜ rightBasis 1 + leftBasis 1 ⊗ₜ rightBasis 0:= by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Fin.isValue]
+  erw [leftRightToMatrix_symm_expand_tmul]
+  simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', σ1, of_apply, cons_val', empty_val',
+    cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, head_cons, zero_smul, one_smul,
+    zero_add, head_fin_const, add_zero, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
+
+/-- The expansion of the pauli matrix `σ₂` in terms of a basis of tensor product vectors. -/
+lemma leftRightToMatrix_σSA_inr_1_expand : leftRightToMatrix.symm (σSA (Sum.inr 1)) =
+    -(I • leftBasis 0 ⊗ₜ[ℂ] rightBasis 1) + I • leftBasis 1 ⊗ₜ[ℂ] rightBasis 0 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Fin.isValue]
+  erw [leftRightToMatrix_symm_expand_tmul]
+  simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', σ2, of_apply, cons_val', empty_val',
+    cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, head_cons, zero_smul, neg_smul,
+    zero_add, head_fin_const, add_zero]
+
+/-- The expansion of the pauli matrix `σ₃` in terms of a basis of tensor product vectors. -/
+lemma leftRightToMatrix_σSA_inr_2_expand : leftRightToMatrix.symm (σSA (Sum.inr 2)) =
+    leftBasis 0 ⊗ₜ rightBasis 0 - leftBasis 1 ⊗ₜ rightBasis 1 := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Fin.isValue]
+  erw [leftRightToMatrix_symm_expand_tmul]
+  simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', σ3, of_apply, cons_val', empty_val',
+    cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, head_cons, one_smul, zero_smul,
+    add_zero, head_fin_const, neg_smul, zero_add, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
+  rfl
+
+/-- The expansion of `asTensor` into complexContrBasis basis of tensor product vectors. -/
+lemma asTensor_expand : asTensor =
+    complexContrBasis (Sum.inl 0) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 0)
+    + complexContrBasis (Sum.inl 0) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 1)
+    + complexContrBasis (Sum.inr 0) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 1)
+    + complexContrBasis (Sum.inr 0) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 0)
+    - I • complexContrBasis (Sum.inr 1) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 1)
+    + I • complexContrBasis (Sum.inr 1) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 0)
+    + complexContrBasis (Sum.inr 2) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 0)
+    - complexContrBasis (Sum.inr 2) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 1) := by
+  rw [asTensor_expand_complexContrBasis]
+  rw [leftRightToMatrix_σSA_inl_0_expand, leftRightToMatrix_σSA_inr_0_expand,
+    leftRightToMatrix_σSA_inr_1_expand, leftRightToMatrix_σSA_inr_2_expand]
+  simp only [Action.instMonoidalCategory_tensorObj_V, CategoryTheory.Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Fin.isValue, tmul_add, tmul_neg, tmul_smul, tmul_sub]
+  rfl
+
 /-- The tensor `σ^μ^a^{dot a}` based on the Pauli-matrices as a morphism,
   `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded` manifesting
   the invariance under the `SL(2,ℂ)` action. -/
@@ -124,5 +194,10 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗
           CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
           Action.FunctorCategoryEquivalence.functor_obj_obj]
 
+lemma asConsTensor_apply_one : asConsTensor.hom (1 : ℂ) = asTensor := by
+  change asConsTensor.hom.toFun (1 : ℂ) = asTensor
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    asConsTensor, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 end
 end PauliMatrix

HepLean/Tensors/ComplexLorentz/Basis.lean

@@ -81,8 +81,7 @@ lemma contrMatrix_basis_expand : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
     - basisVector ![Color.up, Color.up] (fun _ => 2)
     - basisVector ![Color.up, Color.up] (fun _ => 3) := by
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
-    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V]
-    Functor.id_obj, Fin.isValue]
   erw [Lorentz.contrMetric_apply_one, Lorentz.contrMetricVal_expand_tmul]
   simp only [Fin.isValue, map_sub]
   congr 1
@@ -100,6 +99,45 @@ lemma contrMatrix_basis_expand : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+/-- 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)
+    + basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 1 | 2 => 1)
+    + basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 0 | 2 => 1)
+    + basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 1 | 1 => 1 | 2 => 0)
+    - I • basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 0 | 2 => 1)
+    + I • basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 2 | 1 => 1 | 2 => 0)
+    + basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 0 | 2 => 0)
+    - basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 3 | 1 => 1 | 2 => 1) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constThreeNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue]
+  erw [PauliMatrix.asConsTensor_apply_one, PauliMatrix.asTensor_expand]
+  simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, Action.instMonoidalCategory_tensorObj_V,
+    Fin.isValue, map_sub, map_add, _root_.map_smul]
+  congr 1
+  congr 1
+  congr 1
+  congr 1
+  congr 1
+  congr 1
+  congr 1
+  all_goals
+    erw [tripleIsoSep_tmul, basisVector]
+    apply congrArg
+    try apply congrArg
+    funext i
+    match i with
+    | (0 : Fin 3) =>
+      simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom,
+        cons_val_zero, Fin.cases_zero]
+      change _ = Lorentz.complexContrBasisFin4 _
+      simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
+      rfl
+    | (1 : Fin 3) => rfl
+    | (2 : Fin 3) => rfl
+
+
 end complexLorentzTensor
 end Fermion
 end

HepLean/Tensors/OverColor/Discrete.lean

@@ -91,8 +91,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
     (((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
       ((PiTensorProduct.tprod k) _)) = _
   rw [lift.map_tprod]
-  change ((lift.obj F).map fin2Iso.inv).hom ((PiTensorProduct.tprod k) fun i => _) = _
+  erw [lift.map_tprod]
-  rw [lift.map_tprod]
   congr
   funext i
   match i with
@@ -122,6 +121,44 @@ def tripleIsoSep {c1 c2 c3 : C} :
   ((lift.obj F).μIso _ _).trans <|
   (lift.obj F).mapIso fin3Iso'.symm
 
+lemma tripleIsoSep_tmul {c1 c2 c3 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2))
+    (z : F.obj (Discrete.mk c3)) :
+    (tripleIsoSep F).hom.hom (x ⊗ₜ[k] y ⊗ₜ[k] z) = PiTensorProduct.tprod k
+      (fun | (0 : Fin 3) => x | (1 : Fin 3) => y | (2 : Fin 3) => z) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V,
+    tripleIsoSep, Functor.mapIso_symm, Iso.trans_hom, whiskerLeftIso_hom, whiskerRightIso_hom,
+    Iso.symm_hom, MonoidalFunctor.μIso_hom, Functor.mapIso_inv, Action.comp_hom,
+    Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply,
+    ModuleCat.MonoidalCategory.whiskerLeft_apply, ModuleCat.MonoidalCategory.whiskerRight_apply,
+    Functor.id_obj, mk_hom]
+  erw [pairIsoSep_tmul F y z]
+  erw [forgetLiftAppV_symm_apply F c1]
+  erw [lift.obj_μ_tprod_tmul F _ _]
+  erw [lift.map_tprod]
+  apply congrArg
+  funext i
+  match i with
+  | (0 : Fin 3) =>
+    simp only [mk_hom, Fin.isValue, Matrix.cons_val_zero, instMonoidalCategoryStruct_tensorObj_left,
+      instMonoidalCategoryStruct_tensorObj_hom, lift.discreteFunctorMapEqIso, eqToIso_refl,
+      Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.id_obj, Nat.reduceAdd,
+      Nat.succ_eq_add_one, LinearEquiv.ofLinear_apply]
+    rfl
+  | (1 : Fin 3) =>
+    simp only [mk_hom, Fin.isValue, Matrix.cons_val_one, Matrix.head_cons,
+      instMonoidalCategoryStruct_tensorObj_left, instMonoidalCategoryStruct_tensorObj_hom,
+      lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom,
+      Iso.refl_inv, Functor.id_obj, Nat.reduceAdd, Nat.succ_eq_add_one, LinearEquiv.ofLinear_apply]
+    rfl
+  | (2 : Fin 3) =>
+    simp only [mk_hom, Fin.isValue, Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
+      instMonoidalCategoryStruct_tensorObj_left, instMonoidalCategoryStruct_tensorObj_hom,
+      lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom,
+      Iso.refl_inv, Functor.id_obj, LinearEquiv.ofLinear_apply]
+    rfl
+
 /-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
 def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
   F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F)

HepLean/Tensors/Tree/Basic.lean

@@ -652,6 +652,14 @@ lemma constTwoNode_tensor {c1 c2 : S.C}
     (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (v.hom (1 : S.k)) :=
   rfl
 
+@[simp]
+lemma constThreeNode_tensor {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)) :
+    (constThreeNode v).tensor =
+    (OverColor.Discrete.tripleIsoSep S.FDiscrete).hom.hom (v.hom (1 : S.k)) :=
+  rfl
+
 lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1)
     (t2 : TensorTree S c2) :
     (prod t1 t2).tensor = (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom