feat: Update Contraction

2024-10-15 06:08:56 +00:00 · 2024-10-15 06:08:56 +00:00 · 98e2f1865d
commit 98e2f1865d
parent b86d97c07c
6 changed files with 572 additions and 180 deletions
--- a/HepLean/SpaceTime/WeylFermion/Basic.lean
+++ b/HepLean/SpaceTime/WeylFermion/Basic.lean
@ -224,174 +224,6 @@ informal_lemma rightHandedWeylAltEquiv_equivariant where
    action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
  deps :≈ [``rightHandedWeylAltEquiv]

-/-!
-
-## Contraction of Weyl fermions.
-
-/
-open CategoryTheory.MonoidalCategory
-
-/-- The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a
-  alt-left-handed Weyl fermion. -/
-def leftAltBi : leftHanded →ₗ[ℂ] altLeftHanded →ₗ[ℂ] ℂ where
-  toFun ψ := {
-    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
-    map_add' := by
-      intro φ φ'
-      simp only [map_add]
-      rw [dotProduct_add]
-    map_smul' := by
-      intro r φ
-      simp only [LinearEquiv.map_smul]
-      rw [dotProduct_smul]
-      rfl}
-  map_add' ψ ψ':= by
-    refine LinearMap.ext (fun φ => ?_)
-    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
-    rw [add_dotProduct]
-  map_smul' r ψ := by
-    refine LinearMap.ext (fun φ => ?_)
-    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
-    rw [smul_dotProduct]
-    rfl
-
-/-- The bi-linear map corresponding to contraction of a alt-left-handed Weyl fermion with a
-  left-handed Weyl fermion. -/
-def altLeftBi : altLeftHanded →ₗ[ℂ] leftHanded →ₗ[ℂ] ℂ where
-  toFun ψ := {
-    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
-    map_add' := by
-      intro φ φ'
-      simp only [map_add]
-      rw [dotProduct_add]
-    map_smul' := by
-      intro r φ
-      simp only [LinearEquiv.map_smul]
-      rw [dotProduct_smul]
-      rfl}
-  map_add' ψ ψ':= by
-    refine LinearMap.ext (fun φ => ?_)
-    simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
-      AddHom.coe_mk, LinearMap.add_apply]
-  map_smul' ψ ψ' := by
-    refine LinearMap.ext (fun φ => ?_)
-    simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
-      LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
-
-/-- The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
-    summing over components of leftHandedWeyl and altLeftHandedWeyl in the
-    standard basis (i.e. the dot product).
-    Physically, the contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion.
-    In index notation this is ψ_a φ^a. -/
-def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
-  hom := TensorProduct.lift leftAltBi
-  comm M := by
-    apply TensorProduct.ext'
-    intro ψ φ
-    change (M.1 *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
-    rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
-    simp
-
-lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
-    leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
-  rw [leftAltContraction]
-  erw [TensorProduct.lift.tmul]
-  rfl
-
-/-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
-    summing over components of altLeftHandedWeyl and leftHandedWeyl in the
-    standard basis (i.e. the dot product).
-    Physically, the contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion.
-    In index notation this is φ^a ψ_a. -/
-def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
-  hom := TensorProduct.lift altLeftBi
-  comm M := by
-    apply TensorProduct.ext'
-    intro φ ψ
-    change (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1 *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
-    rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
-    simp
-
-lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
-    altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
-  rw [altLeftContraction]
-  erw [TensorProduct.lift.tmul]
-  rfl
-
-lemma leftAltContraction_apply_symm (ψ : leftHanded) (φ : altLeftHanded) :
-    leftAltContraction.hom (ψ ⊗ₜ φ) = altLeftContraction.hom (φ ⊗ₜ ψ) := by
-  rw [altLeftContraction_hom_tmul, leftAltContraction_hom_tmul]
-  exact dotProduct_comm ψ.toFin2ℂ φ.toFin2ℂ
-
-/-- 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
-
-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]
-
-informal_definition rightAltWeylContraction where
-  math :≈ "The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
-    summing over components of rightHandedWeyl and altRightHandedWeyl in the
-    standard basis (i.e. the dot product)."
-  physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
-    In index notation this is ψ_{dot a} φ^{dot a}."
-  deps :≈ [``rightHanded, ``altRightHanded]
-
-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 :≈ [``rightAltWeylContraction]
-
-informal_definition altRightWeylContraction where
-  math :≈ "The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
-    summing over components of altRightHandedWeyl and rightHandedWeyl in the
-    standard basis (i.e. the dot product)."
-  physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
-    In index notation this is φ^{dot a} ψ_{dot a}."
-  deps :≈ [``rightHanded, ``altRightHanded]
-
-informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
-  math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
-    with the braiding of the tensor product."
-  deps :≈ [``rightAltWeylContraction, ``altRightWeylContraction]
-
-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 :≈ [``altRightWeylContraction]
-
 end

 end Fermion
--- a/HepLean/SpaceTime/WeylFermion/Contraction.lean
+++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean
@ -0,0 +1,282 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.WeylFermion.Basic
+/-!
+
+# Contraction of Weyl fermions
+
+-/
+
+namespace Fermion
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+
+
+/-!
+
+## Contraction of Weyl fermions.
+
+-/
+open CategoryTheory.MonoidalCategory
+
+/-- The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a
+  alt-left-handed Weyl fermion. -/
+def leftAltBi : leftHanded →ₗ[ℂ] altLeftHanded →ₗ[ℂ] ℂ where
+  toFun ψ := {
+    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
+    map_add' := by
+      intro φ φ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r φ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' ψ ψ':= by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+    rw [add_dotProduct]
+  map_smul' r ψ := by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
+    rw [smul_dotProduct]
+    rfl
+
+/-- The bi-linear map corresponding to contraction of a alt-left-handed Weyl fermion with a
+  left-handed Weyl fermion. -/
+def altLeftBi : altLeftHanded →ₗ[ℂ] leftHanded →ₗ[ℂ] ℂ where
+  toFun ψ := {
+    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
+    map_add' := by
+      intro φ φ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r φ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' ψ ψ':= by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
+      AddHom.coe_mk, LinearMap.add_apply]
+  map_smul' ψ ψ' := by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
+      LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
+
+
+/-- The bi-linear map corresponding to contraction of a right-handed Weyl fermion with a
+  alt-right-handed Weyl fermion. -/
+def rightAltBi : rightHanded →ₗ[ℂ] altRightHanded →ₗ[ℂ] ℂ where
+  toFun ψ := {
+    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
+    map_add' := by
+      intro φ φ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r φ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' ψ ψ':= by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+    rw [add_dotProduct]
+  map_smul' r ψ := by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
+    rw [smul_dotProduct]
+    rfl
+
+/-- The bi-linear map corresponding to contraction of a alt-right-handed Weyl fermion with a
+  right-handed Weyl fermion. -/
+def altRightBi : altRightHanded →ₗ[ℂ] rightHanded →ₗ[ℂ] ℂ where
+  toFun ψ := {
+    toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
+    map_add' := by
+      intro φ φ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r φ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' ψ ψ':= by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
+      AddHom.coe_mk, LinearMap.add_apply]
+  map_smul' ψ ψ' := by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
+      LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
+
+/-- The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
+    summing over components of leftHandedWeyl and altLeftHandedWeyl in the
+    standard basis (i.e. the dot product).
+    Physically, the contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion.
+    In index notation this is ψ_a φ^a. -/
+def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift leftAltBi
+  comm M := by
+    apply TensorProduct.ext'
+    intro ψ φ
+    change (M.1 *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
+    rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
+    simp
+
+lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
+    leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
+  rw [leftAltContraction]
+  erw [TensorProduct.lift.tmul]
+  rfl
+
+/-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
+    summing over components of altLeftHandedWeyl and leftHandedWeyl in the
+    standard basis (i.e. the dot product).
+    Physically, the contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion.
+    In index notation this is φ^a ψ_a. -/
+def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift altLeftBi
+  comm M := by
+    apply TensorProduct.ext'
+    intro φ ψ
+    change (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1 *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
+    rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
+    simp
+
+lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
+    altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
+  rw [altLeftContraction]
+  erw [TensorProduct.lift.tmul]
+  rfl
+
+/--
+The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
+  summing over components of rightHandedWeyl and altRightHandedWeyl in the
+  standard basis (i.e. the dot product).
+  The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
+    In index notation this is ψ_{dot a} φ^{dot a}.
+-/
+def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift rightAltBi
+  comm M := by
+    apply TensorProduct.ext'
+    intro ψ φ
+    change (M.1.map star *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹.conjTranspose *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
+    have h1 : (M.1)⁻¹ᴴ = ((M.1)⁻¹.map star)ᵀ := by
+      rw [conjTranspose]
+      exact rfl
+    rw [dotProduct_mulVec, h1, vecMul_transpose, mulVec_mulVec]
+    have h2 : ((M.1)⁻¹.map star * (M.1).map star) = 1 := by
+      refine transpose_inj.mp ?_
+      rw [transpose_mul]
+      change M.1.conjTranspose * (M.1)⁻¹.conjTranspose = 1ᵀ
+      rw [← @conjTranspose_mul]
+      simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
+        not_false_eq_true, nonsing_inv_mul, conjTranspose_one, transpose_one]
+    rw [h2]
+    simp only [one_mulVec, vec2_dotProduct, Fin.isValue, RightHandedModule.toFin2ℂEquiv_apply,
+      AltRightHandedModule.toFin2ℂEquiv_apply]
+
+informal_definition altRightWeylContraction where
+  math :≈ "The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
+    summing over components of altRightHandedWeyl and rightHandedWeyl in the
+    standard basis (i.e. the dot product)."
+  physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
+    In index notation this is φ^{dot a} ψ_{dot a}."
+  deps :≈ [``rightHanded, ``altRightHanded]
+
+def altRightContraction : altRightHanded ⊗ rightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift altRightBi
+  comm M := by
+    apply TensorProduct.ext'
+    intro φ ψ
+    change (M.1⁻¹.conjTranspose *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1.map star *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
+    have h1 : (M.1)⁻¹ᴴ = ((M.1)⁻¹.map star)ᵀ := by
+      rw [conjTranspose]
+      exact rfl
+    rw [dotProduct_mulVec, h1, mulVec_transpose, vecMul_vecMul]
+    have h2 : ((M.1)⁻¹.map star * (M.1).map star) = 1 := by
+      refine transpose_inj.mp ?_
+      rw [transpose_mul]
+      change M.1.conjTranspose * (M.1)⁻¹.conjTranspose = 1ᵀ
+      rw [← @conjTranspose_mul]
+      simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
+        not_false_eq_true, nonsing_inv_mul, conjTranspose_one, transpose_one]
+    rw [h2]
+    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ℂ
+
+/-- 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
+
+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]
+
+
+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]
+
+informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
+  math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
+    with the braiding of the tensor product."
+  deps :≈ [``rightAltContraction, ``altRightWeylContraction]
+
+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 :≈ [``altRightWeylContraction]
+
+
+end
+end Fermion
--- a/HepLean/Tensors/OverColor/Discrete.lean
+++ b/HepLean/Tensors/OverColor/Discrete.lean
@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Lift
+import HepLean.Mathematics.PiTensorProduct
+import HepLean.Tensors.OverColor.Iso
+/-!
+
+# Discrete color category
+
+-/
+
+namespace IndexNotation
+namespace OverColor
+namespace Discrete
+
+open CategoryTheory
+open MonoidalCategory
+open TensorProduct
+variable {C k : Type} [CommRing k] {G : Type} [Group G]
+
+variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
+noncomputable section
+
+def pair : Discrete C ⥤ Rep k G := F ⊗ F
+
+def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅
+    (lift.obj F).obj (OverColor.mk ![c,c]) := by
+  symm
+  apply ((lift.obj F).mapIso fin2Iso).trans
+  apply ((lift.obj F).μIso _ _).symm.trans
+  apply tensorIso ?_ ?_
+  · symm
+    apply (forgetLiftApp F c).symm.trans
+    refine (lift.obj F).mapIso (mkIso ?_)
+    funext x
+    fin_cases x
+    rfl
+  · symm
+    apply (forgetLiftApp F c).symm.trans
+    refine (lift.obj F).mapIso (mkIso ?_)
+    funext x
+    fin_cases x
+    rfl
+
+
+def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
+  F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤  Discrete C) ⋙ F)
+
+def τPair (τ : C → C) : Discrete C ⥤ Rep k G :=
+  ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤  Discrete C) ⋙ F) ⊗ F
+
+end
+end Discrete
+end OverColor
+end IndexNotation
--- a/HepLean/Tensors/OverColor/Iso.lean
+++ b/HepLean/Tensors/OverColor/Iso.lean
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Functors
+import HepLean.Tensors.OverColor.Lift
 /-!

 ## Isomorphisms in the OverColor category
@ -39,6 +40,18 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
    subst h
    rfl))

+def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by
+  let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm
+  apply (equivToIso e1).trans
+  apply (mkSum _).trans
+  refine tensorIso (mkIso ?_) (mkIso ?_)
+  · funext x
+    fin_cases x
+    rfl
+  · funext x
+    fin_cases x
+    rfl
+
 /-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
  `i`th component. -/
 def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
@ -158,6 +171,9 @@ def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
      rw [h]
      rfl))

+variable {k : Type} [CommRing k] {G : Type} [Group G]
+
+
 /-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the
  image of `contrPair` based on the given values. -/
 def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ)
--- a/HepLean/Tensors/OverColor/Lift.lean
+++ b/HepLean/Tensors/OverColor/Lift.lean
@ -23,6 +23,7 @@ interfact more generally with tensors.

 namespace IndexNotation
 namespace OverColor
+
 open CategoryTheory
 open MonoidalCategory
 open TensorProduct
@ -661,10 +662,39 @@ def forget : MonoidalFunctor (OverColor C) (Rep k G) ⥤ (Discrete C ⥤ Rep k G
  obj F := Discrete.functor fun c => F.obj (incl.obj (Discrete.mk c))
  map η := Discrete.natTrans fun c => η.app (incl.obj c)

+variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
+
+noncomputable section
+
+def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k]
+     (F.obj (Discrete.mk c)).V :=
+  (PiTensorProduct.subsingletonEquiv 0 :
+    (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) )
+
+def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c))
+    ≅ F.obj (Discrete.mk c) :=
+    Action.mkIso (forgetLiftAppV F c).toModuleIso
+  (fun g => by
+    refine LinearMap.ext (fun x => ?_)
+    simp only [forgetLiftAppV, Fin.isValue, LinearEquiv.toModuleIso_hom]
+    refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
+      simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
+        Function.comp_apply, hy]
+    simp only [CategoryStruct.comp, Fin.isValue, Functor.id_obj,
+      PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe,
+      Function.comp_apply]
+    apply congrArg
+    erw [PiTensorProduct.subsingletonEquiv_apply_tprod]
+    simp only [lift, lift.obj', lift.objObj'_V_carrier, Fin.isValue]
+    erw [lift.objObj'_ρ_tprod]
+    erw [PiTensorProduct.subsingletonEquiv_apply_tprod]
+    rfl)
+
 informal_definition forgetLift where
  math :≈ "The natural isomorphism between `lift (C := C) ⋙ forget` and
    `Functor.id (Discrete C ⥤ Rep k G)`."
  deps :≈ [``forget, ``lift]

+end
 end OverColor
 end IndexNotation
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Iso
+import HepLean.Tensors.OverColor.Discrete
+import HepLean.Tensors.OverColor.Lift
 import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
 /-!

@ -31,16 +33,22 @@ structure TensorStruct where
  k_commRing : CommRing k
  /-- A `MonoidalFunctor` from `OverColor C` giving the rep corresponding to a map of colors
    `X → C`. -/
-  F : MonoidalFunctor (OverColor C) (Rep k G)
+  FDiscrete : Discrete C ⥤ Rep k G
  /-- A map from `C` to `C`. An involution. -/
  τ : C → C
-  /-
-  μContr : OverColor.contrPair C τ ⊗⋙ F ⟶ OverColor.const C ⊗⋙ F
-  dual : (OverColor.map τ ⊗⋙ F) ≅ F-/
+  τ_involution : Function.Involutive τ
+  /-- The natural transformation describing contraction. -/
+  contr : OverColor.Discrete.pairτ F τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
+  /-- The natural transformation describing the metric. -/
+  metricNat : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete
+  /-- The natural transformation describing the unit. -/
+  unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FDiscrete τ
  /-- A specification of the dimension of each color in C. This will be used for explicit
    evaluation of tensors. -/
  evalNo : C → ℕ

+noncomputable section
+
 namespace TensorStruct

 variable (S : TensorStruct)
@ -49,6 +57,113 @@ instance : CommRing S.k := S.k_commRing

 instance : Group S.G := S.G_group

+/-- The lift of the functor `S.F` to a monoidal functor. -/
+def F : MonoidalFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
+
+def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) :=
+  (OverColor.Discrete.pairIso S.FDiscrete c).hom.hom <|
+  (S.metricNat.app (Discrete.mk c)).hom (1 : S.k)
+
+def contrNLE {n : ℕ} {i j : Fin n} (h : i ≠ j) : 2 ≤ n := by
+  omega
+
+def contrNPred {n : ℕ} {i j : Fin n} (h : i ≠ j) : n.pred.pred.succ.succ = n := by
+  simp_all only [ne_eq, Nat.pred_eq_sub_one, Nat.succ_eq_add_one]
+  have hi : i < n := i.isLt
+  have hj : j < n := j.isLt
+  by_contra hn
+  have hn : n  = 0 ∨ n =1 := by omega
+  cases hn
+  · omega
+  · omega
+
+def contrFstSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
+    Fin n.pred.pred.succ.succ := Fin.castOrderIso (contrNPred hineqj).symm i
+
+def contrSndSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
+    Fin n.pred.pred.succ := (Fin.predAbove 0 (contrFstSucc hineqj)).predAbove
+    (Fin.castOrderIso (contrNPred hineqj).symm j)
+
+@[simp]
+lemma contrSndSucc_succAbove {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
+    (contrFstSucc hineqj).succAbove (contrSndSucc hineqj) =
+    Fin.castOrderIso (contrNPred hineqj).symm j := by
+  simp [contrFstSucc, contrSndSucc, Fin.succAbove,
+    Fin.predAbove]
+  split_ifs
+  · rename_i h1 h2
+    rw [Fin.lt_def] at h1 h2
+    simp_all [Fin.lt_def, Fin.ext_iff]
+    intro h
+    omega
+  · rename_i h1 h2
+    rw [Fin.lt_def] at h1 h2
+    simp_all [Fin.ext_iff]
+    rw [Fin.lt_def]
+    simp only [Fin.coe_cast, Fin.val_fin_lt]
+    rw [Fin.lt_def]
+    omega
+  · rename_i h1 h2
+    rw [Fin.lt_def] at h1 h2
+    simp_all [Fin.ext_iff]
+    rw [Fin.lt_def]
+    simp only [Fin.coe_cast, Fin.val_fin_lt]
+    omega
+  · rename_i h1 h2
+    rw [Fin.lt_def] at h1 h2
+    simp_all [Fin.ext_iff]
+    rw [Fin.lt_def]
+    simp only [Fin.coe_cast, Fin.val_fin_lt]
+    omega
+
+
+def contrIso {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)) :
+    S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj (Discrete.mk (c i))) ⊗
+      (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
+  (S.F.mapIso (OverColor.equivToIso (OverColor.finExtractTwo i j))).trans <|
+  (S.F.mapIso (OverColor.mkSum (c ∘ (OverColor.finExtractTwo i j).symm))).trans <|
+  (S.F.μIso _ _).symm.trans <| by
+  refine tensorIso ?_ (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
+  apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(OverColor.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
+  apply (S.F.μIso _ _).symm.trans
+  apply tensorIso ?_ ?_
+  · symm
+    apply (OverColor.forgetLiftApp S.FDiscrete (c i)).symm.trans
+    apply S.F.mapIso
+    apply OverColor.mkIso
+    funext x
+    fin_cases x
+    rfl
+  · symm
+    apply (OverColor.forgetLiftApp S.FDiscrete (S.τ (c i))).symm.trans
+    apply S.F.mapIso
+    apply OverColor.mkIso
+    funext x
+    fin_cases x
+    simp [h]
+
+def contrMap' {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)) :
+    S.F.obj (OverColor.mk c) ⟶
+    (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
+  (S.contrIso c i j h).hom ≫
+  (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
+  (MonoidalCategory.leftUnitor _).hom
+
+def contrMap {n : ℕ} (c : Fin n → S.C)
+    (i j : Fin n) (hij : i ≠ j) (h : c j = S.τ (c i)) :
+    S.F.obj (OverColor.mk c) ⟶
+    (OverColor.lift.obj S.FDiscrete).obj
+    (OverColor.mk ((c ∘ Fin.cast (contrNPred hij)) ∘ Fin.succAbove (contrFstSucc hij) ∘
+    Fin.succAbove (contrSndSucc hij))) := by
+  refine (S.F.mapIso (OverColor.equivToIso (Fin.castOrderIso (contrNPred hij)).toEquiv.symm)).hom ≫
+    S.contrMap' (c ∘ Fin.cast (contrNPred hij)) (contrFstSucc hij) (contrSndSucc hij) ?_
+  simp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, contrSndSucc_succAbove,
+    Fin.castOrderIso_apply, Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self]
+  simpa [contrFstSucc] using h
+
+
 end TensorStruct

 /-- A syntax tree for tensor expressions. -/
@ -60,12 +175,11 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
  | 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)
  | smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
-  | mult {n m : ℕ} {c : Fin n.succ → S.C} {c1 : Fin m.succ → S.C} :
-    (i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 →
-    TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm)
-  | 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)
+  | contr {n : ℕ} {c : Fin n → S.C} : (i j : Fin n) →
+    (hij : i ≠ j) → (h : c j = S.τ (c i)) → TensorTree S c →
+    TensorTree S ((c ∘ Fin.cast (TensorStruct.contrNPred hij)) ∘
+      Fin.succAbove (TensorStruct.contrFstSucc hij) ∘
+      Fin.succAbove (TensorStruct.contrSndSucc hij))
  | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
    TensorTree S (Function.update c i (S.τ (c i)))
  | eval {n : ℕ} {c : Fin n.succ → S.C} :
@ -76,6 +190,7 @@ namespace TensorTree

 variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)

+def metric : TensorTree S ![]
 open MonoidalCategory
 open TensorProduct

@ -86,8 +201,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
  | perm _ t => t.size + 1
  | smul _ t => t.size + 1
  | prod t1 t2 => t1.size + t2.size + 1
-  | mult _ _ t1 t2 => t1.size + t2.size + 1
-  | contr _ _ _ t => t.size + 1
+  | contr _ _ _ _ t => t.size + 1
  | jiggle _ t => t.size + 1
  | eval _ _ t => t.size + 1

@ -102,6 +216,63 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
  | smul a t => a • t.tensor
  | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
    ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
+  | contr i j hij h t  => (S.contrMap _ i j hij h).hom t.tensor
+  | jiggle i t => by
+    rename_i n c'
+    let T := (tensorNode (S.metric (S.τ (c' i))))
+    let T2 := (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
+      ((S.F.μ _ _).hom (T.tensor ⊗ₜ t.tensor))
+    let e1 : Fin (2 + n) ≃ Fin (2 + n) :=
+      (Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i))
+    let T3 := (S.F.map ((OverColor.equivToIso e1).hom)).hom  T2
+    let T4 := (S.contrMap _  (Fin.castAdd n (0 : Fin 2)) (Fin.castAdd n (1 : Fin 2))
+       (by
+      simp only [Fin.isValue, ne_eq,
+      Fin.ext_iff, Fin.coe_castAdd, Fin.val_zero, Fin.coe_natAdd]
+      omega)
+      (by
+        simp [e1]
+        rw [Equiv.swap_apply_of_ne_of_ne]
+        · simp [Fin.ext_iff]
+          rfl
+        · simp [Fin.ext_iff]
+        · simp [Fin.ext_iff]
+          omega)).hom T3
+    refine (S.F.map ?_).hom T4
+    refine (OverColor.equivToIso (Fin.castOrderIso (by simp : (2 + n).pred.pred = n)).toEquiv).hom ≫  ?_
+    refine (OverColor.mkIso ?_).hom
+    funext x
+    simp
+    trans Sum.elim ![S.τ (c' i), S.τ (c' i)] c' (finSumFinEquiv.symm
+      (e1.symm (Fin.natAdd 2 x)))
+    congr
+    simp [Fin.ext_iff]
+    simp [Fin.succAbove]
+    split_ifs
+    · rename_i h1 h2
+      rw [Fin.lt_def] at h1 h2
+      simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
+    · rename_i h1 h2
+      rw [Fin.lt_def] at h1 h2
+      simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
+      simp [Fin.predAbove, Fin.lt_def] at h1
+    · rename_i h1 h2
+      rw [Fin.lt_def] at h1 h2
+      simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
+    · simp
+      omega
+    simp [e1]
+    by_cases hi: x= i
+    · subst hi
+      simp
+    · rw [Equiv.swap_apply_of_ne_of_ne]
+      · simp
+        rw [Function.update]
+        simp [hi]
+      · simp [Fin.ext_iff]
+      · simp [Fin.ext_iff]
+        omega
+
  | _ => 0

 lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
@ -110,3 +281,5 @@ lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
 end

 end TensorTree
+
+end