refactor: Docs

HepLean/SpaceTime/WeylFermion/Contraction.lean

@@ -135,8 +135,6 @@ def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,
 
 lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
     leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
-  rw [leftAltContraction]
-  erw [TensorProduct.lift.tmul]
   rfl
 
 /-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
@@ -153,8 +151,6 @@ def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,
 
 lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
     altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
-  rw [altLeftContraction]
-  erw [TensorProduct.lift.tmul]
   rfl
 
 /--
@@ -162,7 +158,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

HepLean/SpaceTime/WeylFermion/Two.lean

@@ -619,8 +619,7 @@ lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
     leftRightToMatrix.symm
     (SL2C.repSelfAdjointMatrix M ⟨v, hv⟩) := by
   rw [leftRightToMatrix_ρ_symm]
-  apply congrArg
-  simp [SpaceTime.SL2C.repSelfAdjointMatrix]
+  rfl
 
 end
 end Fermion

HepLean/Tensors/Tree/Elab.lean

@@ -418,6 +418,7 @@ def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ))
     (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x))
   return l2''.map fun x => x.1
 
+/-- Takes two maps `Fin n → Fin n` and returns the equivelance they form. -/
 def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by decide)
   (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin n where
   toFun := f1
@@ -425,6 +426,7 @@ def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by deci
   left_inv := h'
   right_inv := h
 
+/-- Given two lists of indices returns the permutation between them based on `finMapToEquiv`. -/
 def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term := do
   let lPerm ← getPermutation l1 l2
   let l2Perm ← getPermutation l1 l2
@@ -435,6 +437,7 @@ def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term :=
   let stx := Syntax.mkApp (mkIdent ``finMapToEquiv) #[P1, P2]
   return stx
 
+/-- The syntax for a equality of tensor trees. -/
 def equalSyntax (permSyntax : Term) (T1 T2 : Term) : TermElabM Term := do
   let X1 := Syntax.mkApp (mkIdent ``TensorTree.tensor) #[T1]
   let P := Syntax.mkApp (mkIdent ``OverColor.equivToHomEq) #[permSyntax]

HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean

@@ -22,27 +22,43 @@ namespace TensorTree
 
 variable {S : TensorStruct}
 
+/-- A structure containing two pairs of indices (i, j) and (k, l) to be sequentially
+  contracted in a tensor.-/
 structure ContrQuartet {n : ℕ} (c : Fin n.succ.succ.succ.succ → S.C) where
+  /-- The first index of the first pair to be contracted. -/
   i : Fin n.succ.succ.succ.succ
+  /-- The second index of the first pair to be contracted. -/
   j : Fin n.succ.succ.succ
+  /-- The first index of the second pair to be contracted. -/
   k : Fin n.succ.succ
+  /-- The second index of the second pair to be contracted. -/
   l : Fin n.succ
+  /-- The condition on the first pair of indices permitting their contraction. -/
   hij : c (i.succAbove j) = S.τ (c i)
+  /-- The condition on the second pair of indices permitting their contraction. -/
   hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) = S.τ ((c ∘ i.succAbove ∘ j.succAbove) k)
 
 namespace ContrQuartet
 variable {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} (q : ContrQuartet c)
 
+/-- On swapping the order of contraction (notionally `(i, j) - (k, l)` vs `(k, l) - (i, j)`), this
+  is the new `i` index. -/
 def swapI : Fin n.succ.succ.succ.succ := q.i.succAbove (q.j.succAbove q.k)
 
+/-- On swapping the order of contraction (notionally `(i, j) - (k, l)` vs `(k, l) - (i, j)`), this
+  is the new `j` index. -/
 def swapJ : Fin n.succ.succ.succ := (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
   ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
 
+/-- On swapping the order of contraction (notionally `(i, j) - (k, l)` vs `(k, l) - (i, j)`), this
+  is the new `k` index. -/
 def swapK : Fin n.succ.succ := predAboveI
     ((predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
       ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l))
     (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)
 
+/-- On swapping the order of contraction (notionally `(i, j) - (k, l)` vs `(k, l) - (i, j)`), this
+  is the new `l` index. -/
 def swapL : Fin n.succ := predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
   (predAboveI (q.j.succAbove q.k) q.j)
 
@@ -113,6 +129,8 @@ lemma swapL_swapK_swapJ_swapI_succAbove :
   exact Fin.succAbove_ne q.j q.k
   exact Fin.succAbove_ne (predAboveI (q.j.succAbove q.k) q.j) q.l
 
+/-- The `ContrQuartet` corresponding to swapping the order of contraction
+  (notionally `(i, j) - (k, l)` vs `(k, l) - (i, j)`). -/
 def swap : ContrQuartet c where
   i := q.swapI
   j := q.swapJ
@@ -126,10 +144,13 @@ def swap : ContrQuartet c where
 
 noncomputable section
 
+/-- The contraction map for the first pair of indices. -/
 def contrMapFst := S.contrMap c q.i q.j q.hij
 
+/-- The contractoin map for the second pair of indices. -/
 def contrMapSnd := S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l q.hkl
 
+/-- The homomorphism one must apply on swapping the order of contractions. -/
 def contrSwapHom : (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘
     q.swap.k.succAbove ∘ q.swap.l.succAbove)) ⟶
     (OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))) :=