Merge pull request #177 from HEPLean/Fermions

feat: Properties of fermions

HepLean.lean

@@ -88,6 +88,8 @@ import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.SL2C.Basic
 import HepLean.SpaceTime.WeylFermion.Basic
+import HepLean.SpaceTime.WeylFermion.Modules
+import HepLean.SpaceTime.WeylFermion.OverCat
 import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.HiggsBoson.GaugeAction

HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean

@@ -75,8 +75,8 @@ lemma prodMatrix_hermitian (Φ1 Φ2 : HiggsField) (x : SpaceTime) :
 
 /-- The map `prodMatrix` is a smooth function on spacetime. -/
 lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) :
-    Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ,  Matrix (Fin 2) (Fin 2) ℂ) (prodMatrix Φ1 Φ2) := by
-  rw [show 𝓘(ℝ,  Matrix (Fin 2) (Fin 2) ℂ) = modelWithCornersSelf ℝ (Fin 2 → Fin 2 → ℂ) from rfl,
+    Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Matrix (Fin 2) (Fin 2) ℂ) (prodMatrix Φ1 Φ2) := by
+  rw [show 𝓘(ℝ, Matrix (Fin 2) (Fin 2) ℂ) = modelWithCornersSelf ℝ (Fin 2 → Fin 2 → ℂ) from rfl,
     smooth_pi_space]
   intro i
   rw [smooth_pi_space]
@@ -87,7 +87,7 @@ lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) :
 
 informal_lemma prodMatrix_invariant where
   math :≈ "The map ``prodMatrix is invariant under the simultanous action of ``gaugeAction
-   on the two Higgs fields."
+    on the two Higgs fields."
   deps :≈ [``prodMatrix, ``gaugeAction]
 
 informal_lemma prodMatrix_to_higgsField where

HepLean/SpaceTime/SL2C/Basic.lean

@@ -28,6 +28,23 @@ noncomputable section
 
 /-!
 
+## Some basic properties about SL(2, ℂ)
+
+Possibly to be moved to mathlib at some point.
+-/
+
+lemma inverse_coe (M : SL(2, ℂ)) : M.1⁻¹ = (M⁻¹).1 := by
+  apply Matrix.inv_inj
+  simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero, not_false_eq_true,
+    nonsing_inv_nonsing_inv, SpecialLinearGroup.coe_inv]
+  have h1 : IsUnit M.1.det := by
+    simp
+  rw [Matrix.inv_adjugate M.1 h1]
+  · simp
+  · simp
+
+/-!
+
 ## Representation of SL(2, ℂ) on spacetime
 
 Through the correspondence between spacetime and self-adjoint matrices,

HepLean/SpaceTime/WeylFermion/Basic.lean

@@ -4,44 +4,115 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Informal
+import HepLean.SpaceTime.SL2C.Basic
+import Mathlib.RepresentationTheory.Rep
+import HepLean.Tensors.Basic
+import HepLean.SpaceTime.WeylFermion.Modules
+import Mathlib.Logic.Equiv.TransferInstance
 /-!
 
 # Weyl fermions
 
--/
+A good reference for the material in this file is:
+https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf
 
-/-!
-
-## The definition of Weyl fermion vector spaces.
-
-We define the vector spaces corresponding to different types of Weyl fermions.
-
-Note: We should prevent casting between these vector spaces.
 -/
 
 namespace Fermion
+noncomputable section
 
-informal_definition leftHandedWeyl where
-  math :≈ "The vector space ℂ^2 carrying the fundamental representation of SL(2,C)."
-  physics :≈ "A Weyl fermion with indices ψ_a."
-  ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
 
-informal_definition rightHandedWeyl where
-  math :≈ "The vector space ℂ^2 carrying the conjguate representation of SL(2,C)."
-  physics :≈ "A Weyl fermion with indices ψ_{dot a}."
-  ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
+/-- The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
+  In index notation corresponds to a Weyl fermion with indices ψ_a. -/
+def leftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
+  toFun := fun M => {
+    toFun := fun (ψ : LeftHandedModule) =>
+      LeftHandedModule.toFin2ℂEquiv.symm (M.1 *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp [mulVec_add]
+    map_smul' := by
+      intro r ψ
+      simp [mulVec_smul]}
+  map_one' := by
+    ext i
+    simp
+  map_mul' := fun M N => by
+    simp only [SpecialLinearGroup.coe_mul]
+    ext1 x
+    simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply, LinearEquiv.apply_symm_apply,
+      mulVec_mulVec]}
 
-informal_definition altLeftHandedWeyl where
-  math :≈ "The vector space ℂ^2 carrying the representation of SL(2,C) given by
-    M → (M⁻¹)ᵀ."
-  physics :≈ "A Weyl fermion with indices ψ^a."
-  ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
+/-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
+    M → (M⁻¹)ᵀ. In index notation corresponds to a Weyl fermion with indices ψ^a. -/
+def altLeftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
+  toFun := fun M => {
+    toFun := fun (ψ : AltLeftHandedModule) =>
+      AltLeftHandedModule.toFin2ℂEquiv.symm ((M.1⁻¹)ᵀ *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp [mulVec_add]
+    map_smul' := by
+      intro r ψ
+      simp [mulVec_smul]}
+  map_one' := by
+    ext i
+    simp
+  map_mul' := fun M N => by
+    ext1 x
+    simp only [SpecialLinearGroup.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
+      LinearEquiv.apply_symm_apply, mulVec_mulVec, EmbeddingLike.apply_eq_iff_eq]
+    refine (congrFun (congrArg _ ?_) _)
+    rw [Matrix.mul_inv_rev]
+    exact transpose_mul _ _}
 
-informal_definition altRightHandedWeyl where
-  math :≈ "The vector space ℂ^2 carrying the representation of SL(2,C) given by
-    M → (M⁻¹)^†."
-  physics :≈ "A Weyl fermion with indices ψ^{dot a}."
-  ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
+/-- The vector space ℂ^2 carrying the conjugate representation of SL(2,C).
+  In index notation corresponds to a Weyl fermion with indices ψ_{dot a}. -/
+def rightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
+  toFun := fun M => {
+    toFun := fun (ψ : RightHandedModule) =>
+      RightHandedModule.toFin2ℂEquiv.symm (M.1.map star *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp [mulVec_add]
+    map_smul' := by
+      intro r ψ
+      simp [mulVec_smul]}
+  map_one' := by
+    ext i
+    simp
+  map_mul' := fun M N => by
+    ext1 x
+    simp only [SpecialLinearGroup.coe_mul, RCLike.star_def, Matrix.map_mul, LinearMap.coe_mk,
+      AddHom.coe_mk, LinearMap.mul_apply, LinearEquiv.apply_symm_apply, mulVec_mulVec]}
+
+/-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
+    M → (M⁻¹)^†.
+    In index notation this corresponds to a Weyl fermion with index `ψ^{dot a}`. -/
+def altRightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
+  toFun := fun M => {
+    toFun := fun (ψ : AltRightHandedModule) =>
+      AltRightHandedModule.toFin2ℂEquiv.symm ((M.1⁻¹).conjTranspose *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp [mulVec_add]
+    map_smul' := by
+      intro r ψ
+      simp [mulVec_smul]}
+  map_one' := by
+    ext i
+    simp
+  map_mul' := fun M N => by
+    ext1 x
+    simp only [SpecialLinearGroup.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
+      LinearEquiv.apply_symm_apply, mulVec_mulVec, EmbeddingLike.apply_eq_iff_eq]
+    refine (congrFun (congrArg _ ?_) _)
+    rw [Matrix.mul_inv_rev]
+    exact conjTranspose_mul _ _}
 
 /-!
 
@@ -49,20 +120,104 @@ informal_definition altRightHandedWeyl where
 
 -/
 
-informal_definition leftHandedWeylAltEquiv where
-  math :≈ "The linear equiv between leftHandedWeyl and altLeftHandedWeyl given
-    by multiplying an element of rightHandedWeyl by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`."
-  deps :≈ [``leftHandedWeyl, ``altLeftHandedWeyl]
+/-- The morphism between the representation `leftHanded` and the representation
+  `altLeftHanded` defined by multiplying an element of
+  `leftHanded` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`. -/
+def leftHandedToAlt : leftHanded ⟶ altLeftHanded where
+  hom := {
+    toFun := fun ψ => AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp only [mulVec_add, LinearEquiv.map_add]
+    map_smul' := by
+      intro a ψ
+      simp only [mulVec_smul, LinearEquiv.map_smul]
+      rfl}
+  comm := by
+    intro M
+    refine LinearMap.ext (fun ψ => ?_)
+    change AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ M.1 *ᵥ ψ.val) =
+      AltLeftHandedModule.toFin2ℂEquiv.symm ((M.1⁻¹)ᵀ *ᵥ !![0, 1; -1, 0] *ᵥ ψ.val)
+    apply congrArg
+    rw [mulVec_mulVec, mulVec_mulVec, SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+    refine congrFun (congrArg _ ?_) _
+    rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
+      Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
+    simp
 
-informal_lemma leftHandedWeylAltEquiv_equivariant where
-  math :≈ "The linear equiv leftHandedWeylAltEquiv is equivariant with respect to the
-    action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl."
-  deps :≈ [``leftHandedWeylAltEquiv]
+lemma leftHandedToAlt_hom_apply (ψ : leftHanded) :
+    leftHandedToAlt.hom ψ =
+    AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
+
+/-- The morphism from `altLeftHanded` to
+  `leftHanded` defined by multiplying an element of
+  altLeftHandedWeyl by the matrix `εₐ₁ₐ₂ = !![0, -1; 1, 0]`. -/
+def leftHandedAltTo : altLeftHanded ⟶ leftHanded where
+  hom := {
+    toFun := fun ψ =>
+      LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ),
+    map_add' := by
+      intro ψ ψ'
+      simp only [map_add]
+      rw [mulVec_add, LinearEquiv.map_add]
+    map_smul' := by
+      intro a ψ
+      simp only [LinearEquiv.map_smul]
+      rw [mulVec_smul, LinearEquiv.map_smul]
+      rfl}
+  comm := by
+    intro M
+    refine LinearMap.ext (fun ψ => ?_)
+    change LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ (M.1⁻¹)ᵀ *ᵥ ψ.val) =
+      LeftHandedModule.toFin2ℂEquiv.symm (M.1 *ᵥ !![0, -1; 1, 0] *ᵥ ψ.val)
+    rw [EquivLike.apply_eq_iff_eq, mulVec_mulVec, mulVec_mulVec, SpaceTime.SL2C.inverse_coe,
+      eta_fin_two M.1]
+    refine congrFun (congrArg _ ?_) _
+    rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
+      Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
+    simp
+
+lemma leftHandedAltTo_hom_apply (ψ : altLeftHanded) :
+    leftHandedAltTo.hom ψ =
+    LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
+
+/-- The equivalence between the representation `leftHanded` and the representation
+  `altLeftHanded` defined by multiplying an element of
+  `leftHanded` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`. -/
+def leftHandedAltEquiv : leftHanded ≅ altLeftHanded where
+  hom := leftHandedToAlt
+  inv := leftHandedAltTo
+  hom_inv_id := by
+    ext ψ
+    simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Action.id_hom,
+      ModuleCat.id_apply]
+    rw [leftHandedAltTo_hom_apply, leftHandedToAlt_hom_apply]
+    rw [AltLeftHandedModule.toFin2ℂ, LinearEquiv.apply_symm_apply, mulVec_mulVec]
+    rw [show (!![0, -1; (1 : ℂ), 0] * !![0, 1; -1, 0]) = 1 by simpa using Eq.symm one_fin_two]
+    rw [one_mulVec]
+    rfl
+  inv_hom_id := by
+    ext ψ
+    simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Action.id_hom,
+      ModuleCat.id_apply]
+    rw [leftHandedAltTo_hom_apply, leftHandedToAlt_hom_apply, LeftHandedModule.toFin2ℂ,
+      LinearEquiv.apply_symm_apply, mulVec_mulVec]
+    rw [show (!![0, (1 : ℂ); -1, 0] * !![0, -1; 1, 0]) = 1 by simpa using Eq.symm one_fin_two]
+    rw [one_mulVec]
+    rfl
+
+lemma leftHandedAltEquiv_hom_hom_apply (ψ : leftHanded) :
+    leftHandedAltEquiv.hom.hom ψ =
+    AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
+
+lemma leftHandedAltEquiv_inv_hom_apply (ψ : altLeftHanded) :
+    leftHandedAltEquiv.inv.hom ψ =
+    LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
 
 informal_definition rightHandedWeylAltEquiv where
   math :≈ "The linear equiv between rightHandedWeyl and altRightHandedWeyl given
     by multiplying an element of rightHandedWeyl by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`"
-  deps :≈ [``rightHandedWeyl, ``altRightHandedWeyl]
+  deps :≈ [``rightHanded, ``altRightHanded]
 
 informal_lemma rightHandedWeylAltEquiv_equivariant where
   math :≈ "The linear equiv rightHandedWeylAltEquiv is equivariant with respect to the
@@ -74,37 +229,137 @@ informal_lemma rightHandedWeylAltEquiv_equivariant where
 ## Contraction of Weyl fermions.
 
 -/
+open CategoryTheory.MonoidalCategory
 
-informal_definition leftAltWeylContraction where
-  math :≈ "The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
+/-- 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)."
-  physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
-    In index notation this is ψ_a φ^a."
-  deps :≈ [``leftHandedWeyl, ``altLeftHandedWeyl]
+    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
 
-informal_lemma leftAltWeylContraction_invariant where
-  math :≈ "The contraction leftAltWeylContraction is invariant with respect to
-    the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl."
-  deps :≈ [``leftAltWeylContraction]
+lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
+    leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
+  rw [leftAltContraction]
+  erw [TensorProduct.lift.tmul]
+  rfl
 
-informal_definition altLeftWeylContraction where
-  math :≈ "The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
+/-- 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)."
-  physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
-    In index notation this is φ^a ψ_a ."
-  deps :≈ [``leftHandedWeyl, ``altLeftHandedWeyl]
+    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 :≈ [``leftAltWeylContraction, ``altLeftWeylContraction]
+  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 :≈ [``altLeftWeylContraction]
+  deps :≈ [``altLeftContraction]
 
 informal_definition rightAltWeylContraction where
   math :≈ "The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
@@ -112,7 +367,7 @@ informal_definition rightAltWeylContraction where
     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 :≈ [``rightHandedWeyl, ``altRightHandedWeyl]
+  deps :≈ [``rightHanded, ``altRightHanded]
 
 informal_lemma rightAltWeylContraction_invariant where
   math :≈ "The contraction rightAltWeylContraction is invariant with respect to
@@ -125,7 +380,7 @@ informal_definition altRightWeylContraction where
     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 :≈ [``rightHandedWeyl, ``altRightHandedWeyl]
+  deps :≈ [``rightHanded, ``altRightHanded]
 
 informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
   math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
@@ -137,4 +392,6 @@ informal_lemma altRightWeylContraction_invariant where
     the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
   deps :≈ [``altRightWeylContraction]
 
+end
+
 end Fermion

HepLean/SpaceTime/WeylFermion/Modules.lean

@@ -0,0 +1,212 @@
+/-
+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.Meta.Informal
+import HepLean.SpaceTime.SL2C.Basic
+import Mathlib.RepresentationTheory.Rep
+import HepLean.Tensors.Basic
+import Mathlib.Logic.Equiv.TransferInstance
+/-!
+
+## Modules associated with Fermions
+
+Weyl fermions live in the vector space `ℂ^2`, defined here as `Fin 2 → ℂ`.
+However if we simply define the Module of Weyl fermions as `Fin 2 → ℂ` we get casting problems,
+where e.g. left-handed fermions can be cast to right-handed fermions etc.
+To overcome this, for each type of Weyl fermion we define a structure that wraps `Fin 2 → ℂ`,
+and these structures we define the instance of a module. This prevents casting between different
+types of fermions.
+
+-/
+
+namespace Fermion
+noncomputable section
+
+section LeftHanded
+
+/-- The module in which left handed fermions live. This is equivalent to `Fin 2 → ℂ`. -/
+structure LeftHandedModule where
+  /-- The underlying value in `Fin 2 → ℂ`. -/
+  val : Fin 2 → ℂ
+
+namespace LeftHandedModule
+
+/-- The equivalence between `LeftHandedModule` and `Fin 2 → ℂ`. -/
+def toFin2ℂFun : LeftHandedModule ≃ (Fin 2 → ℂ) where
+  toFun v := v.val
+  invFun f := ⟨f⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The instance of `AddCommMonoid` on `LeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommMonoid LeftHandedModule := Equiv.addCommMonoid toFin2ℂFun
+
+/-- The instance of `AddCommGroup` on `LeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommGroup LeftHandedModule := Equiv.addCommGroup toFin2ℂFun
+
+/-- The instance of `Module` on `LeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : Module ℂ LeftHandedModule := Equiv.module ℂ toFin2ℂFun
+
+/-- The linear equivalence between `LeftHandedModule` and `(Fin 2 → ℂ)`. -/
+@[simps!]
+def toFin2ℂEquiv : LeftHandedModule ≃ₗ[ℂ] (Fin 2 → ℂ) where
+  toFun := toFin2ℂFun
+  map_add' := fun _ _ => rfl
+  map_smul' := fun _ _ => rfl
+  invFun := toFin2ℂFun.symm
+  left_inv := fun _ => rfl
+  right_inv := fun _ => rfl
+
+/-- The underlying element of `Fin 2 → ℂ` of a element in `LeftHandedModule` defined
+  through the linear equivalence `toFin2ℂEquiv`. -/
+abbrev toFin2ℂ (ψ : LeftHandedModule) := toFin2ℂEquiv ψ
+
+end LeftHandedModule
+
+end LeftHanded
+
+section AltLeftHanded
+
+/-- The module in which alt-left handed fermions live. This is equivalent to `Fin 2 → ℂ`. -/
+structure AltLeftHandedModule where
+  /-- The underlying value in `Fin 2 → ℂ`. -/
+  val : Fin 2 → ℂ
+
+namespace AltLeftHandedModule
+
+/-- The equivalence between `AltLeftHandedModule` and `Fin 2 → ℂ`. -/
+def toFin2ℂFun : AltLeftHandedModule ≃ (Fin 2 → ℂ) where
+  toFun v := v.val
+  invFun f := ⟨f⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The instance of `AddCommMonoid` on `AltLeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommMonoid AltLeftHandedModule := Equiv.addCommMonoid toFin2ℂFun
+
+/-- The instance of `AddCommGroup` on `AltLeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommGroup AltLeftHandedModule := Equiv.addCommGroup toFin2ℂFun
+
+/-- The instance of `Module` on `AltLeftHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : Module ℂ AltLeftHandedModule := Equiv.module ℂ toFin2ℂFun
+
+/-- The linear equivalence between `AltLeftHandedModule` and `(Fin 2 → ℂ)`. -/
+@[simps!]
+def toFin2ℂEquiv : AltLeftHandedModule ≃ₗ[ℂ] (Fin 2 → ℂ) where
+  toFun := toFin2ℂFun
+  map_add' := fun _ _ => rfl
+  map_smul' := fun _ _ => rfl
+  invFun := toFin2ℂFun.symm
+  left_inv := fun _ => rfl
+  right_inv := fun _ => rfl
+
+/-- The underlying element of `Fin 2 → ℂ` of a element in `AltLeftHandedModule` defined
+  through the linear equivalence `toFin2ℂEquiv`. -/
+abbrev toFin2ℂ (ψ : AltLeftHandedModule) := toFin2ℂEquiv ψ
+
+end AltLeftHandedModule
+
+end AltLeftHanded
+
+section RightHanded
+
+/-- The module in which right handed fermions live. This is equivalent to `Fin 2 → ℂ`. -/
+structure RightHandedModule where
+  /-- The underlying value in `Fin 2 → ℂ`. -/
+  val : Fin 2 → ℂ
+
+namespace RightHandedModule
+
+/-- The equivalence between `RightHandedModule` and `Fin 2 → ℂ`. -/
+def toFin2ℂFun : RightHandedModule ≃ (Fin 2 → ℂ) where
+  toFun v := v.val
+  invFun f := ⟨f⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The instance of `AddCommMonoid` on `RightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommMonoid RightHandedModule := Equiv.addCommMonoid toFin2ℂFun
+
+/-- The instance of `AddCommGroup` on `RightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommGroup RightHandedModule := Equiv.addCommGroup toFin2ℂFun
+
+/-- The instance of `Module` on `RightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : Module ℂ RightHandedModule := Equiv.module ℂ toFin2ℂFun
+
+/-- The linear equivalence between `RightHandedModule` and `(Fin 2 → ℂ)`. -/
+@[simps!]
+def toFin2ℂEquiv : RightHandedModule ≃ₗ[ℂ] (Fin 2 → ℂ) where
+  toFun := toFin2ℂFun
+  map_add' := fun _ _ => rfl
+  map_smul' := fun _ _ => rfl
+  invFun := toFin2ℂFun.symm
+  left_inv := fun _ => rfl
+  right_inv := fun _ => rfl
+
+/-- The underlying element of `Fin 2 → ℂ` of a element in `RightHandedModule` defined
+  through the linear equivalence `toFin2ℂEquiv`. -/
+abbrev toFin2ℂ (ψ : RightHandedModule) := toFin2ℂEquiv ψ
+
+end RightHandedModule
+
+end RightHanded
+
+section AltRightHanded
+
+/-- The module in which alt-right handed fermions live. This is equivalent to `Fin 2 → ℂ`. -/
+structure AltRightHandedModule where
+  /-- The underlying value in `Fin 2 → ℂ`. -/
+  val : Fin 2 → ℂ
+
+namespace AltRightHandedModule
+
+/-- The equivalence between `AltRightHandedModule` and `Fin 2 → ℂ`. -/
+def toFin2ℂFun : AltRightHandedModule ≃ (Fin 2 → ℂ) where
+  toFun v := v.val
+  invFun f := ⟨f⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The instance of `AddCommMonoid` on `AltRightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommMonoid AltRightHandedModule := Equiv.addCommMonoid toFin2ℂFun
+
+/-- The instance of `AddCommGroup` on `AltRightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : AddCommGroup AltRightHandedModule := Equiv.addCommGroup toFin2ℂFun
+
+/-- The instance of `Module` on `AltRightHandedModule` defined via its equivalence
+  with `Fin 2 → ℂ`. -/
+instance : Module ℂ AltRightHandedModule := Equiv.module ℂ toFin2ℂFun
+
+/-- The linear equivalence between `AltRightHandedModule` and `(Fin 2 → ℂ)`. -/
+@[simps!]
+def toFin2ℂEquiv : AltRightHandedModule ≃ₗ[ℂ] (Fin 2 → ℂ) where
+  toFun := toFin2ℂFun
+  map_add' := fun _ _ => rfl
+  map_smul' := fun _ _ => rfl
+  invFun := toFin2ℂFun.symm
+  left_inv := fun _ => rfl
+  right_inv := fun _ => rfl
+
+/-- The underlying element of `Fin 2 → ℂ` of a element in `AltRightHandedModule` defined
+  through the linear equivalence `toFin2ℂEquiv`. -/
+abbrev toFin2ℂ (ψ : AltRightHandedModule) := toFin2ℂEquiv ψ
+
+end AltRightHandedModule
+
+end AltRightHanded
+
+end
+end Fermion

HepLean/SpaceTime/WeylFermion/OverCat.lean

@@ -0,0 +1,215 @@
+/-
+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 Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Types
+import Mathlib.CategoryTheory.Monoidal.Category
+import Mathlib.CategoryTheory.Comma.Over
+import Mathlib.CategoryTheory.Core
+import HepLean.SpaceTime.WeylFermion.Basic
+/-!
+
+## Category over color
+
+-/
+
+namespace IndexNotation
+open CategoryTheory
+
+/-- The core of the category of Types over C. -/
+def OverColor (C : Type) := CategoryTheory.Core (CategoryTheory.Over C)
+
+/-- The instance of `OverColor C` as a groupoid. -/
+instance (C : Type) : Groupoid (OverColor C) := coreCategory
+
+namespace OverColor
+
+namespace Hom
+
+variable {C : Type} {f g h : OverColor C}
+
+/-- Given a hom in `OverColor C` the underlying equivalence between types. -/
+def toEquiv (m : f ⟶ g) : f.left ≃ g.left where
+  toFun := m.hom.left
+  invFun := m.inv.left
+  left_inv := by
+    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.hom_inv_id)
+  right_inv := by
+    simpa only [Over.comp_left] using congrFun (congrArg (fun x => x.left) m.inv_hom_id)
+
+@[simp]
+lemma toEquiv_comp (m : f ⟶ g) (n : g ⟶ h) : toEquiv (m ≫ n) = (toEquiv m).trans (toEquiv n) := by
+  ext x
+  simp [toEquiv]
+  rfl
+
+lemma toEquiv_symm_apply (m : f ⟶ g) (i : g.left) :
+    f.hom ((toEquiv m).symm i) = g.hom i := by
+  simpa [toEquiv, types_comp] using congrFun m.inv.w i
+
+end Hom
+
+end OverColor
+
+end IndexNotation
+
+namespace Fermion
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open IndexNotation
+open CategoryTheory
+
+/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
+inductive Color
+  | upL : Color
+  | downL : Color
+  | upR : Color
+  | downR : Color
+
+/-- The corresponding representations associated with a color. -/
+def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
+  match c with
+  | Color.upL => altLeftHanded
+  | Color.downL => leftHanded
+  | Color.upR => altRightHanded
+  | Color.downR => rightHanded
+
+/-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/
+def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where
+  toFun := Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)
+  invFun := (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)).symm
+  map_add' x y := by
+    subst h
+    rfl
+  map_smul' x y := by
+    subst h
+    rfl
+  left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x
+  right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x
+
+lemma colorToRepCongr_comm_ρ {c1 c2 : Color} (h : c1 = c2) (M : SL(2, ℂ)) (x : (colorToRep c1)) :
+    (colorToRepCongr h) ((colorToRep c1).ρ M x) = (colorToRep c2).ρ M ((colorToRepCongr h) x) := by
+  subst h
+  rfl
+
+namespace colorFun
+
+/-- Given a object in `OverColor Color` the correpsonding tensor product of representations. -/
+def obj' (f : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
+  toFun := fun M => PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M),
+  map_one' := by
+    simp
+  map_mul' := fun M N => by
+    simp only [CategoryTheory.Functor.id_obj, _root_.map_mul]
+    ext x : 2
+    simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]}
+
+lemma obj'_ρ (f : OverColor Color) (M : SL(2, ℂ)) : (obj' f).ρ M =
+    PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M) := rfl
+
+lemma obj'_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ))
+    (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
+    (obj' f).ρ M ((PiTensorProduct.tprod ℂ) x) =
+    PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by
+  rw [obj'_ρ]
+  change (PiTensorProduct.map fun x => (colorToRep (f.hom x)).ρ M) ((PiTensorProduct.tprod ℂ) x) =
+    (PiTensorProduct.tprod ℂ) fun i => ((colorToRep (f.hom i)).ρ M) (x i)
+  rw [PiTensorProduct.map_tprod]
+
+/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _`
+  induced by reindexing. -/
+def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V :=
+  (PiTensorProduct.reindex ℂ (fun x => colorToRep (f.hom x)) (OverColor.Hom.toEquiv m)).trans
+  (PiTensorProduct.congr (fun i => colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i)))
+
+lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
+    (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
+    mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
+    PiTensorProduct.tprod ℂ (fun i => (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
+    (x ((OverColor.Hom.toEquiv m).symm i))) := by
+  rw [mapToLinearEquiv']
+  simp only [CategoryTheory.Functor.id_obj, LinearEquiv.trans_apply]
+  change (PiTensorProduct.congr fun i => colorToRepCongr _)
+    ((PiTensorProduct.reindex ℂ (fun x => CoeSort.coe (colorToRep (f.hom x)))
+    (OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _
+  rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
+  rfl
+
+/-- Given a morphism in `OverColor Color` the corresopnding map of representations induced by
+  reindexing. -/
+def map' {f g : OverColor Color} (m : f ⟶ g) : obj' f ⟶ obj' g where
+  hom := (mapToLinearEquiv' m).toLinearMap
+  comm M := by
+    ext x : 2
+    refine PiTensorProduct.induction_on' x ?_ (by
+      intro x y hx hy
+      simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
+        Function.comp_apply, hy])
+    intro r x
+    simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
+      _root_.map_smul, ModuleCat.coe_comp, Function.comp_apply]
+    apply congrArg
+    change (mapToLinearEquiv' m) (((obj' f).ρ M) ((PiTensorProduct.tprod ℂ) x)) =
+      ((obj' g).ρ M) ((mapToLinearEquiv' m) ((PiTensorProduct.tprod ℂ) x))
+    rw [mapToLinearEquiv'_tprod, obj'_ρ_tprod]
+    erw [mapToLinearEquiv'_tprod, obj'_ρ_tprod]
+    apply congrArg
+    funext i
+    rw [colorToRepCongr_comm_ρ]
+
+end colorFun
+
+/-- The functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors
+  to the corresponding tensor product representation. -/
+def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where
+  obj := colorFun.obj'
+  map := colorFun.map'
+  map_id f := by
+    simp only
+    ext x
+    refine PiTensorProduct.induction_on' x ?_ (by
+      intro x y hx hy
+      simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
+        Function.comp_apply, hy])
+    intro r x
+    simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
+      _root_.map_smul, Action.id_hom, ModuleCat.id_apply]
+    apply congrArg
+    rw [colorFun.map']
+    erw [colorFun.mapToLinearEquiv'_tprod]
+    apply congrArg
+    funext i
+    rfl
+  map_comp {X Y Z} f g := by
+    simp only
+    ext x
+    refine PiTensorProduct.induction_on' x ?_ (by
+      intro x y hx hy
+      simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
+        Function.comp_apply, hy])
+    intro r x
+    simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul,
+      Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply]
+    apply congrArg
+    rw [colorFun.map', colorFun.map', colorFun.map']
+    simp only
+    change (colorFun.mapToLinearEquiv' (CategoryTheory.CategoryStruct.comp f g))
+      ((PiTensorProduct.tprod ℂ) x) =
+      (colorFun.mapToLinearEquiv' g) ((colorFun.mapToLinearEquiv' f) ((PiTensorProduct.tprod ℂ) x))
+    rw [colorFun.mapToLinearEquiv'_tprod, colorFun.mapToLinearEquiv'_tprod]
+    erw [colorFun.mapToLinearEquiv'_tprod]
+    apply congrArg
+    funext i
+    simp only [colorToRepCongr, Function.comp_apply, Equiv.cast_symm, LinearEquiv.coe_mk,
+      Equiv.cast_apply, cast_cast, cast_inj]
+    rfl
+
+end
+end Fermion