Merge pull request #194 from HEPLean/Weyl

feat: Add Pauli-matrices as tensor.
2024-10-16 11:18:40 +00:00 · 2024-10-16 11:18:40 +00:00 · 1f40cb332b
commit 1f40cb332b
parent 8e359c290f aea1e88561
14 changed files with 1085 additions and 154 deletions
--- a/HepLean.lean
+++ b/HepLean.lean
@ -93,6 +93,9 @@ import HepLean.SpaceTime.LorentzVector.LorentzAction
 import HepLean.SpaceTime.LorentzVector.Modules
 import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.MinkowskiMetric
+import HepLean.SpaceTime.PauliMatrices.AsTensor
+import HepLean.SpaceTime.PauliMatrices.Basic
+import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
 import HepLean.SpaceTime.SL2C.Basic
 import HepLean.SpaceTime.WeylFermion.Basic
 import HepLean.SpaceTime.WeylFermion.Contraction
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@ -36,7 +36,7 @@ open minkowskiMetric in
 /-- The Lorentz group is the subset of matrices which preserve the minkowski metric. -/
 def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :=
    {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ |
-      ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}
+    ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}

 namespace LorentzGroup
 /-- Notation for the Lorentz group. -/
@ -326,7 +326,7 @@ lemma toComplex_inv (Λ : LorentzGroup d) : (toComplex Λ)⁻¹ = toComplex Λ
@[simp]
 lemma toComplex_mul_minkowskiMatrix_mul_transpose (Λ : LorentzGroup d) :
    toComplex Λ * minkowskiMatrix.map ofReal * (toComplex Λ)ᵀ = minkowskiMatrix.map ofReal := by
-  simp [toComplex]
+  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]
  have h1 : ((Λ.1).map ⇑ofReal)ᵀ = (Λ.1ᵀ).map ofReal := rfl
  rw [h1]
  trans (Λ.1 * minkowskiMatrix * Λ.1ᵀ).map ofReal
@ -336,12 +336,19 @@ lemma toComplex_mul_minkowskiMatrix_mul_transpose (Λ : LorentzGroup d) :
@[simp]
 lemma toComplex_transpose_mul_minkowskiMatrix_mul_self (Λ : LorentzGroup d) :
    (toComplex Λ)ᵀ * minkowskiMatrix.map ofReal * toComplex Λ = minkowskiMatrix.map ofReal := by
-  simp [toComplex]
+  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]
  have h1 : ((Λ.1).map ⇑ofReal)ᵀ = (Λ.1ᵀ).map ofReal := rfl
  rw [h1]
  trans (Λ.1ᵀ * minkowskiMatrix * Λ.1).map ofReal
  · simp only [Matrix.map_mul]
  simp only [transpose_mul_minkowskiMatrix_mul_self]

+lemma toComplex_mulVec_ofReal (v : Fin 1 ⊕ Fin d → ℝ) (Λ : LorentzGroup d) :
+    toComplex Λ *ᵥ (ofReal ∘ v) = ofReal ∘ (Λ *ᵥ v) := by
+  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]
+  funext i
+  rw [← RingHom.map_mulVec]
+  rfl
+
 end
 end LorentzGroup
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.MinkowskiMetric
+import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
+import Mathlib.Tactic.Polyrith
 /-!
 # Lorentz vector as a self-adjoint matrix

@ -20,150 +22,86 @@ namespace SpaceTime
 open Matrix
 open MatrixGroups
 open Complex
-
-/-- A 2×2-complex matrix formed from a Lorentz vector point. -/
-@[simp]
-def toMatrix (x : LorentzVector 3) : Matrix (Fin 2) (Fin 2) ℂ :=
-  !![x.time + x.space 2, x.space 0 - x.space 1 * I; x.space 0 + x.space 1 * I, x.time - x.space 2]
-
-/-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/
-lemma toMatrix_isSelfAdjoint (x : LorentzVector 3) : IsSelfAdjoint (toMatrix x) := by
-  rw [isSelfAdjoint_iff, star_eq_conjTranspose, ← Matrix.ext_iff]
-  intro i j
-  fin_cases i <;> fin_cases j <;>
-    simp only [toMatrix, LorentzVector.time, Fin.isValue, LorentzVector.space, Function.comp_apply,
-    Fin.zero_eta, conjTranspose_apply, of_apply, cons_val', cons_val_zero, empty_val',
-    cons_val_fin_one, star_add, RCLike.star_def, conj_ofReal, Fin.mk_one, cons_val_one,
-    head_fin_const, star_mul', conj_I, mul_neg, head_cons, star_sub, sub_neg_eq_add]
-  rfl
-
-/-- A self-adjoint matrix formed from a Lorentz vector point. -/
-@[simps!]
-def toSelfAdjointMatrix' (x : LorentzVector 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
-  ⟨toMatrix x, toMatrix_isSelfAdjoint x⟩
-
-/-- A self-adjoint matrix formed from a Lorentz vector point. -/
-@[simp]
-noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
-    LorentzVector 3 := fun i =>
-  match i with
-  | Sum.inl 0 => 1/2 * (x.1 0 0 + x.1 1 1).re
-  | Sum.inr 0 => (x.1 1 0).re
-  | Sum.inr 1 => (x.1 1 0).im
-  | Sum.inr 2 => 1/2 * (x.1 0 0 - x.1 1 1).re
+noncomputable section

 /-- The linear equivalence between the vector-space `spaceTime` and self-adjoint
-  2×2-complex matrices. -/
-noncomputable def toSelfAdjointMatrix :
-    LorentzVector 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
-  toFun := toSelfAdjointMatrix'
-  invFun := fromSelfAdjointMatrix'
-  left_inv x := by
-    funext i
-    match i with
-    | Sum.inl 0 =>
-      simp only [fromSelfAdjointMatrix', one_div, toSelfAdjointMatrix', toMatrix,
-        LorentzVector.time, Fin.isValue, LorentzVector.space, Function.comp_apply, of_apply,
-        cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons,
-        head_fin_const, add_add_sub_cancel, add_re, ofReal_re]
-      ring_nf
-    | Sum.inr 0 =>
-      simp [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, toMatrix_isSelfAdjoint]
-    | Sum.inr 1 =>
-      simp only [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, LorentzVector.time,
-        Fin.isValue, LorentzVector.space, Function.comp_apply, of_apply, cons_val', cons_val_zero,
-        empty_val', cons_val_fin_one, cons_val_one, head_fin_const, add_im, ofReal_im, mul_im,
-        ofReal_re, I_im, mul_one, I_re, mul_zero, add_zero, zero_add]
-    | Sum.inr 2 =>
-      simp only [fromSelfAdjointMatrix', one_div, toSelfAdjointMatrix', toMatrix,
-        LorentzVector.time, Fin.isValue, LorentzVector.space, Function.comp_apply, of_apply,
-        cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons,
-        head_fin_const, add_sub_sub_cancel, add_re, ofReal_re]
-      ring
-  right_inv x := by
-    simp only [toSelfAdjointMatrix', toMatrix, LorentzVector.time, fromSelfAdjointMatrix', one_div,
-      Fin.isValue, add_re, ofReal_mul, ofReal_inv, ofReal_ofNat, ofReal_add, LorentzVector.space,
-      Function.comp_apply, sub_re, ofReal_sub, re_add_im]
-    ext i j
-    fin_cases i <;> fin_cases j <;>
-      field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal]
-    · exact conj_eq_iff_re.mp (congrArg (fun M => M 0 0) $ selfAdjoint.mem_iff.mp x.2)
-    · have h01 := congrArg (fun M => M 0 1) $ selfAdjoint.mem_iff.mp x.2
-      simp only [Fin.isValue, star_apply, RCLike.star_def] at h01
-      rw [← h01, RCLike.conj_eq_re_sub_im]
-      rfl
-    · exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2)
-  map_add' x y := by
-    ext i j : 2
-    simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val',
-      cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply]
-    fin_cases i <;> fin_cases j
-    · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl]
-      rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl]
-      simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero]
-      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
-        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
-        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_zero, empty_val',
-        cons_val_fin_one]
-      ring
-    · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl]
-      rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl]
-      simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta,
-        cons_val_zero]
-      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
-        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
-        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_one, empty_val',
-        cons_val_fin_one, cons_val_zero]
-      ring
-    · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl]
-      rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl]
-      simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one,
-        head_fin_const]
-      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
-        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
-        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_zero, empty_val',
-        cons_val_fin_one, cons_val_one, head_fin_const]
-      ring
-    · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl]
-      rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl]
-      simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, head_fin_const]
-      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
-        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
-        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_one, empty_val',
-        cons_val_fin_one, head_fin_const]
-      ring
-  map_smul' r x := by
-    ext i j : 2
-    simp only [toSelfAdjointMatrix'_coe, Fin.isValue, of_apply, cons_val', empty_val',
-      cons_val_fin_one, RingHom.id_apply, selfAdjoint.val_smul, smul_apply, real_smul]
-    fin_cases i <;> fin_cases j
-    · rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
-      rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
-      simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero]
-      ring
-    · rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
-      rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
-      simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta,
-        cons_val_zero]
-      ring
-    · rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
-      rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
-      simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one,
-        head_fin_const]
-      ring
-    · rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
-      rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
-      simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, head_fin_const]
-      ring
+  `2×2`-complex matrices. -/
+def toSelfAdjointMatrix : LorentzVector 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
+  (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)).symm ≪≫ₗ PauliMatrix.σSAL.repr.symm
+
+lemma toSelfAdjointMatrix_apply (x : LorentzVector 3) : toSelfAdjointMatrix x =
+    x (Sum.inl 0) • ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩
+    - x (Sum.inr 0) • ⟨PauliMatrix.σ1, PauliMatrix.σ1_selfAdjoint⟩
+    - x (Sum.inr 1) • ⟨PauliMatrix.σ2, PauliMatrix.σ2_selfAdjoint⟩
+    - x (Sum.inr 2) • ⟨PauliMatrix.σ3, PauliMatrix.σ3_selfAdjoint⟩ := by
+  simp only [toSelfAdjointMatrix, PauliMatrix.σSAL, LinearEquiv.trans_apply, Basis.repr_symm_apply,
+    Basis.coe_mk, Fin.isValue]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
+  · change (∑ i : Fin 1 ⊕ Fin 3, x i • PauliMatrix.σSAL' i) = _
+    simp only [PauliMatrix.σSAL', Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
+      Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three]
+    apply Subtype.ext
+    simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg,
+      AddSubgroupClass.coe_sub]
+    simp only [neg_add, add_assoc, sub_eq_add_neg]
+  · simp_all only [Finset.coe_univ, Finsupp.supported_univ, Submodule.mem_top]
+
+lemma toSelfAdjointMatrix_apply_coe (x : LorentzVector 3) : (toSelfAdjointMatrix x).1 =
+    x (Sum.inl 0) • PauliMatrix.σ0
+    - x (Sum.inr 0) • PauliMatrix.σ1
+    - x (Sum.inr 1) • PauliMatrix.σ2
+    - x (Sum.inr 2) • PauliMatrix.σ3 := by
+  rw [toSelfAdjointMatrix_apply]
+  simp only [Fin.isValue, AddSubgroupClass.coe_sub, selfAdjoint.val_smul]
+
+lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) :
+    toSelfAdjointMatrix (LorentzVector.stdBasis i) = PauliMatrix.σSAL i := by
+  rw [toSelfAdjointMatrix_apply]
+  match i with
+  | Sum.inl 0 =>
+    simp only [LorentzVector.stdBasis, Fin.isValue]
+    erw [Pi.basisFun_apply]
+    simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
+  | Sum.inr 0 =>
+    simp only [LorentzVector.stdBasis, Fin.isValue]
+    erw [Pi.basisFun_apply]
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Pi.single_eq_same, one_smul, zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq,
+      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
+    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+  | Sum.inr 1 =>
+    simp only [LorentzVector.stdBasis, Fin.isValue]
+    erw [Pi.basisFun_apply]
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Sum.inr.injEq, zero_ne_one, sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq,
+      sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
+    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+  | Sum.inr 2 =>
+    simp only [LorentzVector.stdBasis, Fin.isValue]
+    erw [Pi.basisFun_apply]
+    simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
+      Sum.inr.injEq, Fin.reduceEq, sub_self, Pi.single_eq_same, one_smul, zero_sub,
+      PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
+    refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl)
+
+@[simp]
+lemma toSelfAdjointMatrix_symm_basis (i : Fin 1 ⊕ Fin 3) :
+    toSelfAdjointMatrix.symm (PauliMatrix.σSAL i) = (LorentzVector.stdBasis i) := by
+  refine (LinearEquiv.symm_apply_eq toSelfAdjointMatrix).mpr ?_
+  rw [toSelfAdjointMatrix_stdBasis]

 open minkowskiMetric in
 lemma det_eq_ηLin (x : LorentzVector 3) : det (toSelfAdjointMatrix x).1 = ⟪x, x⟫ₘ := by
-  simp only [toSelfAdjointMatrix, LinearEquiv.coe_mk, toSelfAdjointMatrix'_coe, Fin.isValue,
-    det_fin_two_of, eq_time_minus_inner_prod, LorentzVector.time, LorentzVector.space,
+  rw [toSelfAdjointMatrix_apply_coe]
+  simp only [Fin.isValue, eq_time_minus_inner_prod, LorentzVector.time, LorentzVector.space,
    PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three,
    ofReal_sub, ofReal_mul, ofReal_add]
+  simp only [Fin.isValue, PauliMatrix.σ0, smul_of, smul_cons, real_smul, mul_one, smul_zero,
+    smul_empty, PauliMatrix.σ1, of_sub_of, sub_cons, head_cons, sub_zero, tail_cons, zero_sub,
+    sub_self, zero_empty, PauliMatrix.σ2, smul_neg, sub_neg_eq_add, PauliMatrix.σ3, det_fin_two_of]
  ring_nf
  simp only [Fin.isValue, I_sq, mul_neg, mul_one]
  ring

+end
 end SpaceTime
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
@ -10,6 +10,7 @@ import HepLean.SpaceTime.LorentzVector.Modules
 import HepLean.Meta.Informal
 import Mathlib.RepresentationTheory.Rep
 import HepLean.Tensors.Basic
+import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
 /-!

 # Complex Lorentz vectors
@ -49,6 +50,11 @@ lemma complexContrBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
  change (((LorentzGroup.toComplex (SL2C.toLorentzGroup M))) *ᵥ (Pi.single j 1)) i = _
  simp only [mulVec_single, transpose_apply, mul_one]

+lemma complexContrBasis_ρ_val (M : SL(2,ℂ)) (v : complexContr) :
+    ((complexContr.ρ M) v).val =
+    LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ v.val := by
+  rfl
+
 /-- The standard basis of complex covariant Lorentz vectors. -/
 def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun
  (Equiv.linearEquiv ℂ CoℂModule.toFin13ℂFun)
@ -62,5 +68,65 @@ lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
  change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (Pi.single j 1)) i = _
  simp only [mulVec_single, transpose_apply, mul_one]

+/-!
+
+## Relation to real
+
+-/
+
+/-- The semilinear map including real Lorentz vectors into complex contravariant
+  lorentz vectors. -/
+def inclCongrRealLorentz : LorentzVector 3 →ₛₗ[Complex.ofReal] complexContr where
+  toFun v := {val := ofReal ∘ v}
+  map_add' x y := by
+    apply Lorentz.ContrℂModule.ext
+    rw [Lorentz.ContrℂModule.val_add]
+    funext i
+    simp only [Function.comp_apply, ofReal_eq_coe, Pi.add_apply]
+    change ofReal (x i + y i) = _
+    simp only [ofReal_eq_coe, ofReal_add]
+  map_smul' c x := by
+    apply Lorentz.ContrℂModule.ext
+    rw [Lorentz.ContrℂModule.val_smul]
+    funext i
+    simp only [Function.comp_apply, ofReal_eq_coe, Pi.smul_apply]
+    change ofReal (c • x i) = _
+    simp only [smul_eq_mul, ofReal_eq_coe, ofReal_mul]
+
+lemma inclCongrRealLorentz_val (v : LorentzVector 3) :
+    (inclCongrRealLorentz v).val = ofReal ∘ v := rfl
+
+lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
+    (complexContrBasis i) = inclCongrRealLorentz (LorentzVector.stdBasis i) := by
+  apply Lorentz.ContrℂModule.ext
+  simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz, LorentzVector.stdBasis,
+    LinearMap.coe_mk, AddHom.coe_mk]
+  ext j
+  simp only [Function.comp_apply, ofReal_eq_coe]
+  erw [Pi.basisFun_apply]
+  change (Pi.single i 1) j = _
+  exact Eq.symm (Pi.apply_single (fun _ => ofReal') (congrFun rfl) i 1 j)
+
+lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : LorentzVector 3) :
+    (complexContr.ρ M) (inclCongrRealLorentz v) =
+    inclCongrRealLorentz (SL2C.repLorentzVector M v) := by
+  apply Lorentz.ContrℂModule.ext
+  rw [complexContrBasis_ρ_val, inclCongrRealLorentz_val, inclCongrRealLorentz_val]
+  rw [LorentzGroup.toComplex_mulVec_ofReal]
+  apply congrArg
+  simp only [SL2C.toLorentzGroup_apply_coe]
+  rw [SL2C.repLorentzVector_apply_eq_mulVec]
+  rfl
+
+lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
+    (complexContr.ρ M) (complexContrBasis i) =
+    ∑ j, (SL2C.toLorentzGroup M).1 j i •
+    complexContrBasis j := by
+  rw [complexContrBasis_of_real, inclCongrRealLorentz_ρ, SL2C.repLorentzVector_stdBasis, map_sum]
+  apply congrArg
+  funext j
+  simp only [LinearMap.map_smulₛₗ, ofReal_eq_coe, coe_smul]
+  rw [complexContrBasis_of_real]
+
 end Lorentz
 end
--- a/HepLean/SpaceTime/LorentzVector/Modules.lean
+++ b/HepLean/SpaceTime/LorentzVector/Modules.lean
@ -51,6 +51,19 @@ instance : AddCommGroup ContrℂModule := Equiv.addCommGroup toFin13ℂFun
  with `Fin 1 ⊕ Fin 3 → ℂ`. -/
 instance : Module ℂ ContrℂModule := Equiv.module ℂ toFin13ℂFun

+@[ext]
+lemma ext (ψ ψ' : ContrℂModule) (h : ψ.val = ψ'.val) : ψ = ψ' := by
+  cases ψ
+  cases ψ'
+  subst h
+  simp_all only
+
+@[simp]
+lemma val_add (ψ ψ' : ContrℂModule) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
+
+@[simp]
+lemma val_smul (r : ℂ) (ψ : ContrℂModule) : (r • ψ).val = r • ψ.val := rfl
+
 /-- The linear equivalence between `ContrℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
@[simps!]
 def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) where
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@ -82,6 +82,14 @@ lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 :=
  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
  exact diagonal_apply_ne _ h

+lemma inl_0_inl_0 : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := by
+  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
+  rfl
+
+lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1 := by
+  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
+  simp_all only [diagonal_apply_eq, Sum.elim_inr]
+
 end minkowskiMatrix

 /-!
@ -269,6 +277,16 @@ lemma det_dual : (dual Λ).det = Λ.det := by
  norm_cast
  simp

+lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
+    dual Λ μ ν = η μ μ * Λ ν μ * η ν ν := by
+  simp only [dual, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
+    diagonal_mul, transpose_apply, diagonal_apply_eq]
+
+lemma dual_apply_minkowskiMatrix (μ ν : Fin 1 ⊕ Fin d) :
+    dual Λ μ ν * η ν ν = η μ μ * Λ ν μ := by
+  rw [dual_apply, mul_assoc]
+  simp
+
@[simp]
 lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by
  simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, dual, minkowskiLinearForm_apply,
--- a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
+++ b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
@ -0,0 +1,128 @@
+/-
+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.Mathematics.PiTensorProduct
+import HepLean.SpaceTime.LorentzVector.Complex.Basic
+import HepLean.SpaceTime.WeylFermion.Two
+import HepLean.SpaceTime.PauliMatrices.Basic
+/-!
+
+## Pauli matrices
+
+-/
+
+namespace PauliMatrix
+
+open Complex
+open Lorentz
+open Fermion
+open TensorProduct
+open CategoryTheory.MonoidalCategory
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+
+/-- The tensor `σ^μ^a^{dot a}` based on the Pauli-matrices as an element of
+  `complexContr ⊗ leftHanded ⊗ rightHanded`. -/
+def asTensor : (complexContr ⊗ leftHanded ⊗ rightHanded).V :=
+  ∑ i, complexContrBasis i ⊗ₜ leftRightToMatrix.symm (σSA i)
+
+/-- 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. -/
+def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded where
+  hom := {
+    toFun := fun a =>
+      let a' : ℂ := a
+      a' • asTensor,
+    map_add' := fun x y => by
+      simp only [add_smul],
+    map_smul' := fun m x => by
+      simp only [smul_smul]
+      rfl}
+  comm M := by
+    ext x : 2
+    simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Function.comp_apply]
+    let x' : ℂ := x
+    change x' • asTensor =
+      (TensorProduct.map (complexContr.ρ M) (
+        TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M))) (x' • asTensor)
+    simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
+    apply congrArg
+    nth_rewrite 2 [asTensor]
+    simp only [Action.instMonoidalCategory_tensorObj_V, CategoryTheory.Equivalence.symm_inverse,
+      Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+      map_sum, map_tmul]
+    symm
+    calc _ = ∑ x, ((complexContr.ρ M) (complexContrBasis x) ⊗ₜ[ℂ]
+      leftRightToMatrix.symm (SL2C.repSelfAdjointMatrix M (σSA x))) := by
+          refine Finset.sum_congr rfl (fun x _ => ?_)
+          rw [← leftRightToMatrix_ρ_symm_selfAdjoint]
+          rfl
+      _ = ∑ x, ((∑ i, (SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ]
+          ∑ j, leftRightToMatrix.symm ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j))) := by
+          refine Finset.sum_congr rfl (fun x _ => ?_)
+          rw [SL2CRep_ρ_basis, SL2C.repSelfAdjointMatrix_σSA]
+          simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe,
+            Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+            Finset.sum_singleton, map_inv, lorentzGroupIsGroup_inv, AddSubgroup.coe_add,
+            selfAdjoint.val_smul, AddSubgroup.val_finset_sum, map_add, map_sum]
+      _ = ∑ x, ∑ i, ∑ j, ((SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ]
+            leftRightToMatrix.symm.toLinearMap ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j)) := by
+          refine Finset.sum_congr rfl (fun x _ => ?_)
+          rw [sum_tmul]
+          refine Finset.sum_congr rfl (fun i _ => ?_)
+          rw [tmul_sum]
+          rfl
+      _ = ∑ x, ∑ i, ∑ j, ((SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ]
+            ((SL2C.toLorentzGroup M⁻¹).1 x j • leftRightToMatrix.symm ((σSA j))) := by
+          refine Finset.sum_congr rfl (fun x _ => (Finset.sum_congr rfl (fun i _ =>
+            (Finset.sum_congr rfl (fun j _ => ?_)))))
+          simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe,
+            map_inv, lorentzGroupIsGroup_inv, LinearMap.map_smul_of_tower, LinearEquiv.coe_coe,
+            tmul_smul]
+      _ = ∑ x, ∑ i, ∑ j, ((SL2C.toLorentzGroup M).1 i x * (SL2C.toLorentzGroup M⁻¹).1 x j)
+          • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA j)) := by
+          refine Finset.sum_congr rfl (fun x _ => (Finset.sum_congr rfl (fun i _ =>
+            (Finset.sum_congr rfl (fun j _ => ?_)))))
+          rw [smul_tmul, smul_smul, tmul_smul]
+      _ = ∑ i, ∑ x, ∑ j, ((SL2C.toLorentzGroup M).1 i x * (SL2C.toLorentzGroup M⁻¹).1 x j)
+          • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA j)) := Finset.sum_comm
+      _ = ∑ i, ∑ j, ∑ x, ((SL2C.toLorentzGroup M).1 i x * (SL2C.toLorentzGroup M⁻¹).1 x j)
+          • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA j)) :=
+            Finset.sum_congr rfl (fun x _ => Finset.sum_comm)
+      _ = ∑ i, ∑ j, (∑ x, (SL2C.toLorentzGroup M).1 i x * (SL2C.toLorentzGroup M⁻¹).1 x j)
+          • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA j)) := by
+          refine Finset.sum_congr rfl (fun i _ => (Finset.sum_congr rfl (fun j _ => ?_)))
+          rw [Finset.sum_smul]
+      _ = ∑ i, ∑ j, ((1 : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) i j)
+        • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA j)) := by
+          refine Finset.sum_congr rfl (fun i _ => (Finset.sum_congr rfl (fun j _ => ?_)))
+          congr
+          change ((SL2C.toLorentzGroup M) * (SL2C.toLorentzGroup M⁻¹)).1 i j = _
+          rw [← SL2C.toLorentzGroup.map_mul]
+          simp only [mul_inv_cancel, _root_.map_one, lorentzGroupIsGroup_one_coe]
+      _ = ∑ i, ((1 : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) i i)
+        • ((complexContrBasis i)) ⊗ₜ[ℂ] leftRightToMatrix.symm ((σSA i)) := by
+          refine Finset.sum_congr rfl (fun i _ => ?_)
+          refine Finset.sum_eq_single i (fun b _ hb => ?_) (fun hb => ?_)
+          · simp [one_apply_ne' hb]
+          · simp only [Finset.mem_univ, not_true_eq_false] at hb
+      _ = asTensor := by
+        refine Finset.sum_congr rfl (fun i _ => ?_)
+        simp only [Action.instMonoidalCategory_tensorObj_V, one_apply_eq, one_smul,
+          CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+          Action.FunctorCategoryEquivalence.functor_obj_obj]
+
+end
+end PauliMatrix
--- a/HepLean/SpaceTime/PauliMatrices/Basic.lean
+++ b/HepLean/SpaceTime/PauliMatrices/Basic.lean
@ -0,0 +1,136 @@
+/-
+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.Mathematics.PiTensorProduct
+import Mathlib.RepresentationTheory.Rep
+import HepLean.Tensors.Basic
+import Mathlib.Logic.Equiv.TransferInstance
+import HepLean.SpaceTime.LorentzGroup.Basic
+/-!
+
+## Pauli matrices
+
+-/
+
+namespace PauliMatrix
+
+open Complex
+open Matrix
+
+/-- The zeroth Pauli-matrix as a `2 x 2` complex matrix. -/
+def σ0 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, 1]
+
+/-- The first Pauli-matrix as a `2 x 2` complex matrix. -/
+def σ1 : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; 1, 0]
+
+/-- The second Pauli-matrix as a `2 x 2` complex matrix. -/
+def σ2 : Matrix (Fin 2) (Fin 2) ℂ := !![0, -I; I, 0]
+
+/-- The third Pauli-matrix as a `2 x 2` complex matrix. -/
+def σ3 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, -1]
+
+@[simp]
+lemma σ0_selfAdjoint : σ0ᴴ = σ0 := by
+  rw [eta_fin_two σ0ᴴ]
+  simp [σ0]
+
+@[simp]
+lemma σ1_selfAdjoint : σ1ᴴ = σ1 := by
+  rw [eta_fin_two σ1ᴴ]
+  simp [σ1]
+
+@[simp]
+lemma σ2_selfAdjoint : σ2ᴴ = σ2 := by
+  rw [eta_fin_two σ2ᴴ]
+  simp [σ2]
+
+@[simp]
+lemma σ3_selfAdjoint : σ3ᴴ = σ3 := by
+  rw [eta_fin_two σ3ᴴ]
+  simp [σ3]
+
+/-!
+
+## Traces
+
+-/
+
+@[simp]
+lemma σ0_σ0_trace : Matrix.trace (σ0 * σ0) = 2 := by
+  simp only [σ0, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
+    tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply,
+    trace_fin_two_of]
+  norm_num
+
+@[simp]
+lemma σ0_σ1_trace : Matrix.trace (σ0 * σ1) = 0 := by
+  simp [σ0, σ1]
+
+@[simp]
+lemma σ0_σ2_trace : Matrix.trace (σ0 * σ2) = 0 := by
+  simp [σ0, σ2]
+
+@[simp]
+lemma σ0_σ3_trace : Matrix.trace (σ0 * σ3) = 0 := by
+  simp [σ0, σ3]
+
+@[simp]
+lemma σ1_σ0_trace : Matrix.trace (σ1 * σ0) = 0 := by
+  simp [σ1, σ0]
+
+@[simp]
+lemma σ1_σ1_trace : Matrix.trace (σ1 * σ1) = 2 := by
+  simp only [σ1, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
+    tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply,
+    trace_fin_two_of]
+  norm_num
+
+@[simp]
+lemma σ1_σ2_trace : Matrix.trace (σ1 * σ2) = 0 := by
+  simp [σ1, σ2]
+
+@[simp]
+lemma σ1_σ3_trace : Matrix.trace (σ1 * σ3) = 0 := by
+  simp [σ1, σ3]
+
+@[simp]
+lemma σ2_σ0_trace : Matrix.trace (σ2 * σ0) = 0 := by
+  simp [σ2, σ0]
+
+@[simp]
+lemma σ2_σ1_trace : Matrix.trace (σ2 * σ1) = 0 := by
+  simp [σ2, σ1]
+
+@[simp]
+lemma σ2_σ2_trace : Matrix.trace (σ2 * σ2) = 2 := by
+  simp only [σ2, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
+    tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply,
+    trace_fin_two_of]
+  norm_num
+
+@[simp]
+lemma σ2_σ3_trace : Matrix.trace (σ2 * σ3) = 0 := by
+  simp [σ2, σ3]
+
+@[simp]
+lemma σ3_σ0_trace : Matrix.trace (σ3 * σ0) = 0 := by
+  simp [σ3, σ0]
+
+@[simp]
+lemma σ3_σ1_trace : Matrix.trace (σ3 * σ1) = 0 := by
+  simp [σ3, σ1]
+
+@[simp]
+lemma σ3_σ2_trace : Matrix.trace (σ3 * σ2) = 0 := by
+  simp [σ3, σ2]
+
+@[simp]
+lemma σ3_σ3_trace : Matrix.trace (σ3 * σ3) = 2 := by
+  simp only [σ3, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
+    tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply,
+    trace_fin_two_of]
+  norm_num
+
+end PauliMatrix
--- a/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/SpaceTime/PauliMatrices/SelfAdjoint.lean
@ -0,0 +1,424 @@
+/-
+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.Mathematics.PiTensorProduct
+import Mathlib.RepresentationTheory.Rep
+import HepLean.Tensors.Basic
+import Mathlib.Logic.Equiv.TransferInstance
+import HepLean.SpaceTime.LorentzGroup.Basic
+import HepLean.SpaceTime.PauliMatrices.Basic
+/-!
+
+## Interaction of Pauli matrices with self-adjoint matrices
+
+-/
+namespace PauliMatrix
+open Matrix
+
+lemma selfAdjoint_trace_σ0_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    (Matrix.trace (σ0 * A.1)).re = Matrix.trace (σ0 * A.1) := by
+  rw [eta_fin_two A.1]
+  simp only [σ0, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of, Complex.add_re, Complex.ofReal_add]
+  have hA : IsSelfAdjoint A.1 := A.2
+  rw [isSelfAdjoint_iff, star_eq_conjTranspose] at hA
+  rw [eta_fin_two (A.1)ᴴ] at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def, of_apply, cons_val', cons_val_zero,
+    empty_val', cons_val_fin_one, cons_val_one, head_cons, head_fin_const] at hA
+  have h00 := congrArg (fun f => f 0 0) hA
+  simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one] at h00
+  have hA00 : A.1 0 0 = (A.1 0 0).re := by
+    exact Eq.symm ((fun {z} => Complex.conj_eq_iff_re.mp) h00)
+  rw [hA00]
+  simp only [Fin.isValue, Complex.ofReal_re, add_right_inj]
+  have h11 := congrArg (fun f => f 1 1) hA
+  simp only [Fin.isValue, of_apply, cons_val', cons_val_one, head_cons, empty_val',
+    cons_val_fin_one, head_fin_const] at h11
+  exact Complex.conj_eq_iff_re.mp h11
+
+lemma selfAdjoint_trace_σ1_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    (Matrix.trace (σ1 * A.1)).re = Matrix.trace (σ1 * A.1) := by
+  rw [eta_fin_two A.1]
+  simp only [σ1, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of, Complex.add_re, Complex.ofReal_add]
+  have hA : IsSelfAdjoint A.1 := A.2
+  rw [isSelfAdjoint_iff, star_eq_conjTranspose] at hA
+  rw [eta_fin_two (A.1)ᴴ] at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def] at hA
+  have h01 := congrArg (fun f => f 0 1) hA
+  simp only [Fin.isValue, of_apply, cons_val', cons_val_one, head_cons, empty_val',
+    cons_val_fin_one, cons_val_zero] at h01
+  rw [← h01]
+  simp only [Fin.isValue, Complex.conj_re]
+  rw [Complex.add_conj]
+  simp only [Fin.isValue, Complex.ofReal_mul, Complex.ofReal_ofNat]
+  ring
+
+lemma selfAdjoint_trace_σ2_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    (Matrix.trace (σ2 * A.1)).re = Matrix.trace (σ2 * A.1) := by
+  rw [eta_fin_two A.1]
+  simp only [σ2, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of, Complex.add_re, Complex.ofReal_add]
+  have hA : IsSelfAdjoint A.1 := A.2
+  rw [isSelfAdjoint_iff, star_eq_conjTranspose, eta_fin_two (A.1)ᴴ] at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def] at hA
+  have h10 := congrArg (fun f => f 1 0) hA
+  simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
+    cons_val_one, head_fin_const] at h10
+  rw [← h10]
+  simp only [Fin.isValue, neg_smul, smul_cons, smul_eq_mul, smul_empty, neg_cons, neg_empty,
+    trace_fin_two_of, Complex.add_re, Complex.neg_re, Complex.mul_re, Complex.I_re, Complex.conj_re,
+    zero_mul, Complex.I_im, Complex.conj_im, mul_neg, one_mul, sub_neg_eq_add, zero_add, zero_sub,
+    Complex.ofReal_add, Complex.ofReal_neg]
+  trans Complex.I * (A.1 0 1 - (starRingEnd ℂ) (A.1 0 1))
+  · rw [Complex.sub_conj]
+    ring_nf
+    simp
+  · ring
+
+lemma selfAdjoint_trace_σ3_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    (Matrix.trace (σ3 * A.1)).re = Matrix.trace (σ3 * A.1) := by
+  rw [eta_fin_two A.1]
+  simp only [σ3, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of, Complex.add_re, Complex.ofReal_add]
+  have hA : IsSelfAdjoint A.1 := A.2
+  rw [isSelfAdjoint_iff, star_eq_conjTranspose, eta_fin_two (A.1)ᴴ] at hA
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def] at hA
+  have h00 := congrArg (fun f => f 0 0) hA
+  have h11 := congrArg (fun f => f 1 1) hA
+  have hA00 : A.1 0 0 = (A.1 0 0).re := Eq.symm ((fun {z} => Complex.conj_eq_iff_re.mp) h00)
+  have hA11 : A.1 1 1 = (A.1 1 1).re := Eq.symm ((fun {z} => Complex.conj_eq_iff_re.mp) h11)
+  simp only [Fin.isValue, neg_smul, one_smul, neg_cons, neg_empty, trace_fin_two_of, Complex.add_re,
+    Complex.neg_re, Complex.ofReal_add, Complex.ofReal_neg]
+  rw [hA00, hA11]
+  simp
+
+open Complex
+
+lemma selfAdjoint_ext_complex {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
+    (h0 : ((Matrix.trace (PauliMatrix.σ0 * A.1)) = (Matrix.trace (PauliMatrix.σ0 * B.1))))
+    (h1 : Matrix.trace (PauliMatrix.σ1 * A.1) = Matrix.trace (PauliMatrix.σ1 * B.1))
+    (h2 : Matrix.trace (PauliMatrix.σ2 * A.1) = Matrix.trace (PauliMatrix.σ2 * B.1))
+    (h3 : Matrix.trace (PauliMatrix.σ3 * A.1) = Matrix.trace (PauliMatrix.σ3 * B.1)) : A = B := by
+  ext i j
+  rw [eta_fin_two A.1, eta_fin_two B.1] at h0 h1 h2 h3
+  simp only [PauliMatrix.σ0, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons,
+    head_cons, one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of] at h0
+  simp only [σ1, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    zero_smul, tail_cons, one_smul, empty_vecMul, add_zero, zero_add, empty_mul,
+    Equiv.symm_apply_apply, trace_fin_two_of] at h1
+  simp only [σ2, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    zero_smul, tail_cons, neg_smul, smul_cons, smul_eq_mul, smul_empty, neg_cons, neg_empty,
+    empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply, trace_fin_two_of] at h2
+  simp only [σ3, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons,
+    one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, neg_smul, neg_cons, neg_empty, zero_add,
+    empty_mul, Equiv.symm_apply_apply, trace_fin_two_of] at h3
+  match i, j with
+  | 0, 0 =>
+    linear_combination (norm := ring_nf) (h0 + h3) / 2
+  | 0, 1 =>
+    linear_combination (norm := ring_nf) (h1 - I * h2) / 2
+    simp
+  | 1, 0 =>
+    linear_combination (norm := ring_nf) (h1 + I * h2) / 2
+    simp
+  | 1, 1 =>
+    linear_combination (norm := ring_nf) (h0 - h3) / 2
+
+lemma selfAdjoint_ext {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
+    (h0 : ((Matrix.trace (PauliMatrix.σ0 * A.1))).re = ((Matrix.trace (PauliMatrix.σ0 * B.1))).re)
+    (h1 : ((Matrix.trace (PauliMatrix.σ1 * A.1))).re = ((Matrix.trace (PauliMatrix.σ1 * B.1))).re)
+    (h2 : ((Matrix.trace (PauliMatrix.σ2 * A.1))).re = ((Matrix.trace (PauliMatrix.σ2 * B.1))).re)
+    (h3 : ((Matrix.trace (PauliMatrix.σ3 * A.1))).re = ((Matrix.trace (PauliMatrix.σ3 * B.1))).re) :
+    A = B := by
+  have h0' := congrArg ofReal h0
+  have h1' := congrArg ofReal h1
+  have h2' := congrArg ofReal h2
+  have h3' := congrArg ofReal h3
+  rw [ofReal_eq_coe, ofReal_eq_coe] at h0' h1' h2' h3'
+  rw [selfAdjoint_trace_σ0_real A, selfAdjoint_trace_σ0_real B] at h0'
+  rw [selfAdjoint_trace_σ1_real A, selfAdjoint_trace_σ1_real B] at h1'
+  rw [selfAdjoint_trace_σ2_real A, selfAdjoint_trace_σ2_real B] at h2'
+  rw [selfAdjoint_trace_σ3_real A, selfAdjoint_trace_σ3_real B] at h3'
+  exact selfAdjoint_ext_complex h0' h1' h2' h3'
+
+noncomputable section
+
+/-- An auxillary function which on `i : Fin 1 ⊕ Fin 3` returns the corresponding
+  Pauli-matrix as a self-adjoint matrix. -/
+def σSA' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
+  match i with
+  | Sum.inl 0 => ⟨σ0, σ0_selfAdjoint⟩
+  | Sum.inr 0 => ⟨σ1, σ1_selfAdjoint⟩
+  | Sum.inr 1 => ⟨σ2, σ2_selfAdjoint⟩
+  | Sum.inr 2 => ⟨σ3, σ3_selfAdjoint⟩
+
+lemma σSA_linearly_independent : LinearIndependent ℝ σSA' := by
+  apply Fintype.linearIndependent_iff.mpr
+  intro g hg
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton] at hg
+  rw [Fin.sum_univ_three] at hg
+  simp only [Fin.isValue, σSA'] at hg
+  intro i
+  match i with
+  | Sum.inl 0 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ0 * A.1))) hg
+  | Sum.inr 0 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ1 * A.1))) hg
+  | Sum.inr 1 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ2 * A.1))) hg
+  | Sum.inr 2 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ3 * A.1))) hg
+
+lemma σSA_span : ⊤ ≤ Submodule.span ℝ (Set.range σSA') := by
+  refine (top_le_span_range_iff_forall_exists_fun ℝ).mpr ?_
+  intro A
+  let c : Fin 1 ⊕ Fin 3 → ℝ := fun i =>
+    match i with
+    | Sum.inl 0 => 1/2 * (Matrix.trace (σ0 * A.1)).re
+    | Sum.inr 0 => 1/2 * (Matrix.trace (σ1 * A.1)).re
+    | Sum.inr 1 => 1/2 * (Matrix.trace (σ2 * A.1)).re
+    | Sum.inr 2 => 1/2 * (Matrix.trace (σ3 * A.1)).re
+  use c
+  simp only [one_div, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, c]
+  apply selfAdjoint_ext
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ0_σ0_trace, real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat,
+    σ0_σ1_trace, smul_zero, σ0_σ2_trace, add_zero, σ0_σ3_trace, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
+    ring
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ1_σ0_trace, smul_zero, σ1_σ1_trace, real_smul, ofReal_mul, ofReal_inv,
+    ofReal_ofNat, σ1_σ2_trace, add_zero, σ1_σ3_trace, zero_add, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
+    ring
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ2_σ0_trace, smul_zero, σ2_σ1_trace, σ2_σ2_trace, real_smul, ofReal_mul,
+    ofReal_inv, ofReal_ofNat, zero_add, σ2_σ3_trace, add_zero, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
+    ring
+  · simp only [σSA', AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add, Algebra.mul_smul_comm,
+    trace_add, trace_smul, σ3_σ0_trace, smul_zero, σ3_σ1_trace, σ3_σ2_trace, add_zero, σ3_σ3_trace,
+    real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, zero_add, mul_re, inv_re, re_ofNat,
+    normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div, ofReal_im,
+    mul_zero, sub_zero, mul_im, zero_mul]
+    ring
+
+/-- The basis of `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` formed by Pauli matrices. -/
+def σSA : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :=
+  Basis.mk σSA_linearly_independent σSA_span
+
+/-- An auxillary function which on `i : Fin 1 ⊕ Fin 3` returns the corresponding
+  Pauli-matrix as a self-adjoint matrix with a minus sign for `Sum.inr _`. -/
+def σSAL' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
+  match i with
+  | Sum.inl 0 => ⟨σ0, σ0_selfAdjoint⟩
+  | Sum.inr 0 => ⟨-σ1, by rw [neg_mem_iff]; exact σ1_selfAdjoint⟩
+  | Sum.inr 1 => ⟨-σ2, by rw [neg_mem_iff]; exact σ2_selfAdjoint⟩
+  | Sum.inr 2 => ⟨-σ3, by rw [neg_mem_iff]; exact σ3_selfAdjoint⟩
+
+lemma σSAL_linearly_independent : LinearIndependent ℝ σSAL' := by
+  apply Fintype.linearIndependent_iff.mpr
+  intro g hg
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton] at hg
+  rw [Fin.sum_univ_three] at hg
+  simp only [Fin.isValue, σSAL'] at hg
+  intro i
+  match i with
+  | Sum.inl 0 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ0 * A.1))) hg
+  | Sum.inr 0 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ1 * A.1))) hg
+  | Sum.inr 1 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ2 * A.1))) hg
+  | Sum.inr 2 =>
+    simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ3 * A.1))) hg
+
+lemma σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL') := by
+  refine (top_le_span_range_iff_forall_exists_fun ℝ).mpr ?_
+  intro A
+  let c : Fin 1 ⊕ Fin 3 → ℝ := fun i =>
+    match i with
+    | Sum.inl 0 => 1/2 * (Matrix.trace (σ0 * A.1)).re
+    | Sum.inr 0 => - 1/2 * (Matrix.trace (σ1 * A.1)).re
+    | Sum.inr 1 => - 1/2 * (Matrix.trace (σ2 * A.1)).re
+    | Sum.inr 2 => - 1/2 * (Matrix.trace (σ3 * A.1)).re
+  use c
+  simp only [one_div, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three, c]
+  apply selfAdjoint_ext
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ0_σ0_trace, real_smul, ofReal_mul,
+    ofReal_inv, ofReal_ofNat, trace_neg, σ0_σ1_trace, smul_zero, neg_zero, σ0_σ2_trace, add_zero,
+    σ0_σ3_trace, mul_re, inv_re, re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im,
+    im_ofNat, zero_div, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]
+    ring
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ1_σ0_trace, smul_zero, trace_neg,
+    σ1_σ1_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat,
+    σ1_σ2_trace, neg_zero, add_zero, σ1_σ3_trace, zero_add, neg_re, mul_re, div_ofNat_re, one_re,
+    ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat,
+    mul_im, zero_mul, im_ofNat]
+    ring
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ2_σ0_trace, smul_zero, trace_neg,
+    σ2_σ1_trace, neg_zero, σ2_σ2_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one,
+    ofReal_ofNat, zero_add, σ2_σ3_trace, add_zero, neg_re, mul_re, div_ofNat_re, one_re, ofReal_re,
+    div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat, mul_im,
+    zero_mul, im_ofNat]
+    ring
+  · simp only [σSAL', AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg, mul_add,
+    Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul, σ3_σ0_trace, smul_zero, trace_neg,
+    σ3_σ1_trace, neg_zero, σ3_σ2_trace, add_zero, σ3_σ3_trace, real_smul, ofReal_mul, ofReal_div,
+    ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, neg_re, mul_re, div_ofNat_re, one_re, ofReal_re,
+    div_ofNat_im, neg_im, one_im, zero_div, ofReal_im, mul_zero, sub_zero, re_ofNat, mul_im,
+    zero_mul, im_ofNat]
+    ring
+
+/-- The basis of `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` formed by Pauli matrices
+where the `1, 2, 3` pauli matrices are negated. -/
+def σSAL : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :=
+  Basis.mk σSAL_linearly_independent σSAL_span
+
+lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    M = (1/2 * (Matrix.trace (σ0 * M.1)).re) • σSAL (Sum.inl 0)
+    + (-1/2 * (Matrix.trace (σ1 * M.1)).re) • σSAL (Sum.inr 0)
+    + (-1/2 * (Matrix.trace (σ2 * M.1)).re) • σSAL (Sum.inr 1)
+    + (-1/2 * (Matrix.trace (σ3 * M.1)).re) • σSAL (Sum.inr 2) := by
+  apply selfAdjoint_ext
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ0_σ0_trace, real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, trace_neg, σ0_σ1_trace, smul_zero,
+    neg_zero, add_zero, σ0_σ2_trace, σ0_σ3_trace, mul_re, inv_re, re_ofNat, normSq_ofNat,
+    div_self_mul_self', ofReal_re, inv_im, im_ofNat, zero_div, ofReal_im, mul_zero, sub_zero,
+    mul_im, zero_mul]
+    ring
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ1_σ0_trace, smul_zero, trace_neg, σ1_σ1_trace, real_smul, ofReal_mul, ofReal_div, ofReal_neg,
+    ofReal_one, ofReal_ofNat, zero_add, σ1_σ2_trace, neg_zero, add_zero, σ1_σ3_trace, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
+    ring
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ2_σ0_trace, smul_zero, trace_neg, σ2_σ1_trace, neg_zero, add_zero, σ2_σ2_trace, real_smul,
+    ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, σ2_σ3_trace, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
+    ring
+  · simp only [one_div, σSAL, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ3_σ0_trace, smul_zero, trace_neg, σ3_σ1_trace, neg_zero, add_zero, σ3_σ2_trace, σ3_σ3_trace,
+    real_smul, ofReal_mul, ofReal_div, ofReal_neg, ofReal_one, ofReal_ofNat, zero_add, neg_re,
+    mul_re, div_ofNat_re, one_re, ofReal_re, div_ofNat_im, neg_im, one_im, zero_div, ofReal_im,
+    mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
+    ring
+
+@[simp]
+lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    σSAL.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := by
+  have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
+  have h0 := congrArg (fun A => Matrix.trace (σ0 * A.1)/ 2) hM
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ0_σ0_trace, real_smul, trace_neg, σ0_σ1_trace, smul_zero, neg_zero, σ0_σ2_trace, add_zero,
+    σ0_σ3_trace, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+    IsUnit.mul_div_cancel_right] at h0
+  linear_combination (norm := ring_nf) -h0
+  simp [σSAL]
+
+@[simp]
+lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    σSAL.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := by
+  have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
+  have h0 := congrArg (fun A => - Matrix.trace (σ1 * A.1)/ 2) hM
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ1_σ0_trace, smul_zero, trace_neg, σ1_σ1_trace, real_smul, σ1_σ2_trace, neg_zero, add_zero,
+    σ1_σ3_trace, zero_add, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero,
+    not_false_eq_true, IsUnit.mul_div_cancel_right] at h0
+  linear_combination (norm := ring_nf) -h0
+  simp [σSAL]
+
+@[simp]
+lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    σSAL.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := by
+  have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
+  have h0 := congrArg (fun A => - Matrix.trace (σ2 * A.1)/ 2) hM
+  simp only [σSAL, Basis.mk_repr, Fin.isValue, Basis.coe_mk, σSAL', AddSubgroup.coe_add,
+    selfAdjoint.val_smul, smul_neg, mul_add, Algebra.mul_smul_comm, mul_neg, trace_add, trace_smul,
+    σ2_σ0_trace, smul_zero, trace_neg, σ2_σ1_trace, neg_zero, σ2_σ2_trace, real_smul, zero_add,
+    σ2_σ3_trace, add_zero, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero,
+    not_false_eq_true, IsUnit.mul_div_cancel_right] at h0
+  linear_combination (norm := ring_nf) -h0
+  simp [σSAL]
+
+@[simp]
+lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
+    σSAL.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := by
+  have hM : M = ∑ i, σSAL.repr M i • σSAL i := (Basis.sum_repr σSAL M).symm
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, Fin.sum_univ_three] at hM
+  have h0 := congrArg (fun A => - Matrix.trace (σ3 * A.1)/ 2) hM
+  simp [σSAL, σSAL', mul_add] at h0
+  linear_combination (norm := ring_nf) -h0
+  simp [σSAL]
+
+lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
+    (σSA i) = minkowskiMatrix i i • (σSAL i) := by
+  match i with
+  | Sum.inl 0 =>
+    simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inl_0_inl_0]
+  | Sum.inr 0 =>
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
+    cases i with
+    | inl val =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+    | inr val_1 =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+  | Sum.inr 1 =>
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
+    cases i with
+    | inl val =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+    | inr val_1 =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+  | Sum.inr 2 =>
+    simp only [σSA, Fin.isValue, Basis.coe_mk, σSA', minkowskiMatrix.inr_i_inr_i, σSAL, σSAL',
+      neg_smul, one_smul]
+    cases i with
+    | inl val =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+    | inr val_1 =>
+      ext i j : 2
+      simp_all only [NegMemClass.coe_neg, neg_apply, neg_neg]
+
+end
+end PauliMatrix
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@ -43,6 +43,7 @@ lemma inverse_coe (M : SL(2, ℂ)) : M.1⁻¹ = (M⁻¹).1 := by
  · simp
  · simp

+lemma transpose_coe (M : SL(2, ℂ)) : M.1ᵀ = (M.transpose).1 := rfl
 /-!

 ## Representation of SL(2, ℂ) on spacetime
@ -133,6 +134,64 @@ def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
    simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul,
      lorentzGroupIsGroup_mul_coe]

+lemma toLorentzGroup_eq_σSAL (M : SL(2, ℂ)) :
+    toLorentzGroup M = LinearMap.toMatrix
+    PauliMatrix.σSAL PauliMatrix.σSAL (repSelfAdjointMatrix M) := by
+  rfl
+
+lemma toLorentzGroup_eq_stdBasis (M : SL(2, ℂ)) :
+    toLorentzGroup M = LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis
+    (repLorentzVector M) := by rfl
+
+lemma repLorentzVector_apply_eq_mulVec (v : LorentzVector 3) :
+    SL2C.repLorentzVector M v = (SL2C.toLorentzGroup M).1 *ᵥ v := by
+  simp only [toLorentzGroup, MonoidHom.coe_mk, OneHom.coe_mk, toLorentzGroupElem_coe]
+  have hv : v = (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3))
+    (LorentzVector.stdBasis.repr v) := by rfl
+  nth_rewrite 2 [hv]
+  change _ = toLorentzGroup M *ᵥ (LorentzVector.stdBasis.repr v)
+  rw [toLorentzGroup_eq_stdBasis, LinearMap.toMatrix_mulVec_repr]
+  rfl
+
+lemma repSelfAdjointMatrix_basis (i : Fin 1 ⊕ Fin 3) :
+    SL2C.repSelfAdjointMatrix M (PauliMatrix.σSAL i) =
+    ∑ j, (toLorentzGroup M).1 j i •
+    PauliMatrix.σSAL j := by
+  rw [toLorentzGroup_eq_σSAL]
+  simp only [LinearMap.toMatrix_apply, Finset.univ_unique,
+    Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton]
+  nth_rewrite 1 [← (Basis.sum_repr PauliMatrix.σSAL
+    ((repSelfAdjointMatrix M) (PauliMatrix.σSAL i)))]
+  congr
+
+lemma repSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) :
+    SL2C.repSelfAdjointMatrix M (PauliMatrix.σSA i) =
+    ∑ j, (toLorentzGroup M⁻¹).1 i j • PauliMatrix.σSA j := by
+  have h1 : (toLorentzGroup M⁻¹).1 = minkowskiMetric.dual (toLorentzGroup M).1 := by
+    simp
+  simp only [h1]
+  rw [PauliMatrix.σSA_minkowskiMetric_σSAL, _root_.map_smul]
+  rw [repSelfAdjointMatrix_basis]
+  rw [Finset.smul_sum]
+  apply congrArg
+  funext j
+  rw [smul_smul, PauliMatrix.σSA_minkowskiMetric_σSAL, smul_smul]
+  apply congrFun
+  apply congrArg
+  exact Eq.symm (minkowskiMetric.dual_apply_minkowskiMatrix ((toLorentzGroup M).1) i j)
+
+lemma repLorentzVector_stdBasis (i : Fin 1 ⊕ Fin 3) :
+    SL2C.repLorentzVector M (LorentzVector.stdBasis i) =
+    ∑ j, (toLorentzGroup M).1 j i • LorentzVector.stdBasis j := by
+  simp only [repLorentzVector, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.coe_comp,
+    LinearEquiv.coe_coe, Function.comp_apply]
+  rw [toSelfAdjointMatrix_stdBasis]
+  rw [repSelfAdjointMatrix_basis]
+  rw [map_sum]
+  apply congrArg
+  funext j
+  simp
+
 /-!

 ## Homomorphism to the restricted Lorentz group
--- a/HepLean/SpaceTime/WeylFermion/Basic.lean
+++ b/HepLean/SpaceTime/WeylFermion/Basic.lean
@ -27,7 +27,7 @@ open Complex
 open TensorProduct

 /-- The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
-  In index notation corresponds to a Weyl fermion with indices ψ_a. -/
+  In index notation corresponds to a Weyl fermion with indices ψ^a. -/
 def leftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
  toFun := fun M => {
    toFun := fun (ψ : LeftHandedModule) =>
@ -60,7 +60,7 @@ lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
  simp only [mulVec_single, mul_one]

 /-- 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. -/
+    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) =>
@ -95,7 +95,7 @@ lemma altLeftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
  simp only [mulVec_single, transpose_apply, mul_one]

 /-- The vector space ℂ^2 carrying the conjugate representation of SL(2,C).
-  In index notation corresponds to a Weyl fermion with indices ψ_{dot a}. -/
+  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) =>
@ -128,7 +128,7 @@ lemma rightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :

 /-- 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}`. -/
+    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) =>
--- a/HepLean/SpaceTime/WeylFermion/Contraction.lean
+++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean
@ -125,7 +125,7 @@ def altRightBi : altRightHanded →ₗ[ℂ] rightHanded →ₗ[ℂ] ℂ where
    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. -/
+    In index notation this is ψ^a φ_a. -/
 def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
  hom := TensorProduct.lift leftAltBi
  comm M := TensorProduct.ext' fun ψ φ => by
@ -143,7 +143,7 @@ lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
    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. -/
+    In index notation this is φ_a ψ^a. -/
 def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
  hom := TensorProduct.lift altLeftBi
  comm M := TensorProduct.ext' fun φ ψ => by
@ -162,7 +162,7 @@ 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}.
+    In index notation this is ψ^{dot a} φ_{dot a}.
 -/
 def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
  hom := TensorProduct.lift rightAltBi
@ -187,7 +187,7 @@ def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2
    summing over components of altRightHandedWeyl and rightHandedWeyl 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}.
+    In index notation this is φ_{dot a} ψ^{dot a}.
 -/
 def altRightContraction : altRightHanded ⊗ rightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
  hom := TensorProduct.lift altRightBi
--- a/HepLean/SpaceTime/WeylFermion/Two.lean
+++ b/HepLean/SpaceTime/WeylFermion/Two.lean
@ -75,6 +75,18 @@ def altRightRightToMatrix : (altRightHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matri
  Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
  LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

+/-- Equivalence of `altLeftHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
+def altLeftAltRightToMatrix : (altLeftHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
+  (Basis.tensorProduct altLeftBasis altRightBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
+
+/-- Equivalence of `leftHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
+def leftRightToMatrix : (leftHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
+  (Basis.tensorProduct leftBasis rightBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
+
 /-!

 ## Group actions
@ -413,6 +425,87 @@ lemma altRightRightToMatrix_ρ (v : (altRightHanded ⊗ rightHanded).V) (M : SL(
    Action.instMonoidalCategory_tensorObj_V]
  ring

+lemma altLeftAltRightToMatrix_ρ (v : (altLeftHanded ⊗ altRightHanded).V) (M : SL(2,ℂ)) :
+    altLeftAltRightToMatrix (TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) v) =
+    (M.1⁻¹)ᵀ * altLeftAltRightToMatrix v * ((M.1⁻¹).conjTranspose)ᵀ := by
+  nth_rewrite 1 [altLeftAltRightToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
+      (altLeftBasis.tensorProduct altRightBasis) (altLeftBasis.tensorProduct altRightBasis)
+      (TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M)))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
+      ((altLeftBasis.tensorProduct altRightBasis).repr (v))))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (altLeftBasis.tensorProduct altRightBasis)
+      (altLeftBasis.tensorProduct altRightBasis)
+      (TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
+        ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
+        * altLeftAltRightToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
+  have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftAltRightToMatrix v x1 x) *
+      (M.1)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
+      ((M.1)⁻¹ x1 i * altLeftAltRightToMatrix v x1 x) * (M.1)⁻¹ᴴ j x:= by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [altLeftBasis_ρ_apply, altRightBasis_ρ_apply, transpose_apply,
+    Action.instMonoidalCategory_tensorObj_V]
+  ring
+
+lemma leftRightToMatrix_ρ (v : (leftHanded ⊗ rightHanded).V) (M : SL(2,ℂ)) :
+    leftRightToMatrix (TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) v) =
+    M.1 * leftRightToMatrix v * (M.1)ᴴ := by
+  nth_rewrite 1 [leftRightToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
+      (leftBasis.tensorProduct rightBasis) (leftBasis.tensorProduct rightBasis)
+      (TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M)))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
+      ((leftBasis.tensorProduct rightBasis).repr (v))))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct rightBasis)
+      (leftBasis.tensorProduct rightBasis)
+      (TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
+        ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
+        * leftRightToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply]
+  have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j
+    = ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j := by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [leftBasis_ρ_apply, rightBasis_ρ_apply, transpose_apply,
+    Action.instMonoidalCategory_tensorObj_V]
+  rw [Matrix.conjTranspose]
+  simp only [RCLike.star_def, map_apply, transpose_apply]
+  ring
+
 /-!

 ## The symm version of the group actions.
@ -483,5 +576,51 @@ lemma altRightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,
  rw [← h1]
  simp

+lemma altLeftAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) (altLeftAltRightToMatrix.symm v) =
+    altLeftAltRightToMatrix.symm ((M.1⁻¹)ᵀ * v * ((M.1⁻¹).conjTranspose)ᵀ) := by
+  have h1 := altLeftAltRightToMatrix_ρ (altLeftAltRightToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+lemma leftRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) (leftRightToMatrix.symm v) =
+    leftRightToMatrix.symm (M.1 * v * (M.1)ᴴ) := by
+  have h1 := leftRightToMatrix_ρ (leftRightToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+open SpaceTime
+
+lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
+    (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
+    TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) (altLeftAltRightToMatrix.symm v) =
+    altLeftAltRightToMatrix.symm
+    (SL2C.repSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by
+  rw [altLeftAltRightToMatrix_ρ_symm]
+  apply congrArg
+  simp only [SL2C.repSelfAdjointMatrix, MonoidHom.coe_mk, OneHom.coe_mk,
+    SL2C.toLinearMapSelfAdjointMatrix_apply_coe, SpecialLinearGroup.coe_inv,
+    SpecialLinearGroup.coe_transpose]
+  congr
+  · rw [SL2C.inverse_coe]
+    simp only [SpecialLinearGroup.coe_inv]
+    rw [@adjugate_transpose]
+  · rw [SL2C.inverse_coe]
+    simp only [SpecialLinearGroup.coe_inv]
+    rw [← @adjugate_transpose]
+    rfl
+
+lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
+    (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
+    TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) (leftRightToMatrix.symm v) =
+    leftRightToMatrix.symm
+    (SL2C.repSelfAdjointMatrix M ⟨v, hv⟩) := by
+  rw [leftRightToMatrix_ρ_symm]
+  apply congrArg
+  simp [SpaceTime.SL2C.repSelfAdjointMatrix]
+
 end
 end Fermion
--- a/HepLean/SpaceTime/WeylFermion/Unit.lean
+++ b/HepLean/SpaceTime/WeylFermion/Unit.lean
@ -24,11 +24,11 @@ open Complex
 open TensorProduct
 open CategoryTheory.MonoidalCategory

-/-- The left-alt-left unit `δₐᵃ` as an element of `(leftHanded ⊗ altLeftHanded).V`. -/
+/-- The left-alt-left unit `δᵃₐ` as an element of `(leftHanded ⊗ altLeftHanded).V`. -/
 def leftAltLeftUnitVal : (leftHanded ⊗ altLeftHanded).V :=
  leftAltLeftToMatrix.symm 1

-/-- The left-alt-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded `,
+/-- The left-alt-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded `,
  manifesting the invariance under the `SL(2,ℂ)` action. -/
 def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded where
  hom := {
@ -55,11 +55,11 @@ def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded
    apply congrArg
    simp

-/-- The alt-left-left unit `δᵃₐ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/
+/-- The alt-left-left unit `δₐᵃ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/
 def altLeftLeftUnitVal : (altLeftHanded ⊗ leftHanded).V :=
  altLeftLeftToMatrix.symm 1

-/-- The alt-left-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded `,
+/-- The alt-left-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded `,
  manifesting the invariance under the `SL(2,ℂ)` action. -/
 def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded where
  hom := {
@ -87,12 +87,12 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded
    simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq,
      one_ne_zero, not_false_eq_true, mul_nonsing_inv, transpose_one]

-/-- The right-alt-right unit `δ_{dot a}^{dot a}` as an element of
+/-- The right-alt-right unit `δ^{dot a}_{dot a}` as an element of
  `(rightHanded ⊗ altRightHanded).V`. -/
 def rightAltRightUnitVal : (rightHanded ⊗ altRightHanded).V :=
  rightAltRightToMatrix.symm 1

-/-- The right-alt-right unit `δ_{dot a}^{dot a}` as a morphism
+/-- The right-alt-right unit `δ^{dot a}_{dot a}` as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded`, manifesting
  the invariance under the `SL(2,ℂ)` action. -/
 def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded where
@ -126,12 +126,12 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa
    rw [@conjTranspose_nonsing_inv]
    simp

-/-- The alt-right-right unit `δ^{dot a}_{dot a}` as an element of
+/-- The alt-right-right unit `δ_{dot a}^{dot a}` as an element of
  `(rightHanded ⊗ altRightHanded).V`. -/
 def altRightRightUnitVal : (altRightHanded ⊗ rightHanded).V :=
  altRightRightToMatrix.symm 1

-/-- The alt-right-right unit `δ^{dot a}_{dot a}` as a morphism
+/-- The alt-right-right unit `δ_{dot a}^{dot a}` as a morphism
  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded`, manifesting
  the invariance under the `SL(2,ℂ)` action. -/
 def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded where