chore: Add doc strings

HepLean/Mathematics/Fin.lean

@@ -21,6 +21,8 @@ namespace HepLean.Fin
 open Fin
 variable {n : Nat}
 
+/-- Given a `i` and `x` in `Fin n.succ.succ` returns an element of `Fin n.succ`
+  subtracting 1 if `i.val ≤ x.val` else casting x. -/
 def predAboveI (i x : Fin n.succ.succ) : Fin n.succ :=
   if h : x.val < i.val then
     ⟨x.val, by omega⟩
@@ -245,6 +247,8 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
   ext
   rfl
 
+/-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
+  the map  `Fin n.succ → Fin n.succ` obtained by dropping `i` and it's image. -/
 def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
     Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
 

HepLean/Tensors/OverColor/Discrete.lean

@@ -48,6 +48,8 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
     fin_cases x
     rfl
 
+/-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
+  `(lift.obj F).obj (OverColor.mk ![c1,c2])` fored by the tensorate.  -/
 def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
     (lift.obj F).obj (OverColor.mk ![c1,c2]) := by
   symm

HepLean/Tensors/OverColor/Iso.lean

@@ -27,6 +27,8 @@ open HepLean.Fin
 def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) :=
   Hom.toIso (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl))
 
+/-- The homomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
+  equivalence `e`. -/
 def equivToHom {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ e.symm) :=
   (equivToIso e).hom
 
@@ -47,12 +49,15 @@ lemma mkSum_homToEquiv {c : X ⊕ Y → C}:
 lemma mkSum_inv_homToEquiv {c : X ⊕ Y → C}:
     Hom.toEquiv (mkSum c).inv = (Equiv.refl _) := by
   rfl
+
 /-- The isomorphism between objects in `OverColor C` given equality of maps. -/
 def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
   Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
     subst h
     rfl))
 
+/-- The homorophism from `mk c` to `mk c1` obtaied by an equivalence and
+  an equality lemma. -/
 def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y)
     (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : mk c ⟶ mk c1 :=
   (equivToHom e).trans (mkIso (funext fun x => (h x).symm)).hom
@@ -71,6 +76,7 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
     fin_cases x
     rfl
 
+/-- Removes a given `i : Fin n.succ.succ` from a morphism in `OverColor C`. -/
 def extractOne {n : ℕ} (i : Fin n.succ.succ)
     {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
     mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
@@ -96,6 +102,7 @@ lemma extractOne_homToEquiv {n : ℕ} (i : Fin n.succ.succ)
     (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)) := by
   rfl
 
+/-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`. -/
 def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     {c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
     mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
@@ -107,6 +114,8 @@ def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
     equivToHomEq (Equiv.refl _) (by simp)
 
+/-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`.
+  This is from and to different (by equivalent) objects to `extractTwo`. -/
 def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     {c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) :
     mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i)
@@ -114,6 +123,8 @@ def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inr) :=
   equivToHomEq (Equiv.refl _) (by simp) ≫ extractTwo i j σ ≫ equivToHomEq (Equiv.refl _) (by simp)
 
+/-- Given a morphism ` mk c ⟶ mk c1` the corresponding morphism on the `Fin 1 ⊕ Fin 1` maps
+  obtained by extracting `i` and `j`. -/
 def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     {c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) :
   mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i)

HepLean/Tensors/Tree/Basic.lean

@@ -234,6 +234,7 @@ def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
   (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
   (MonoidalCategory.leftUnitor _).hom
 
+/-- Casts an element of the monoidal unit of `Rep S.k S.G` to the field `S.k`. -/
 def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
 
 lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)

HepLean/Tensors/Tree/Elab.lean

@@ -263,12 +263,17 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
   return ind.filter (fun x => indFilt.count x ≤ 1)
 
+/-- Takes a list and puts conseutive  elements into pairs.
+  e.g. [0, 1, 2, 3] becomes [(0, 1), (2, 3)]. -/
 def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
   match l with
   | x1 :: x2 :: xs => (x1, x2) :: toPairs xs
   | [] => []
   | [x] => [(x, 0)]
 
+/-- Adjusts a list `List (ℕ × ℕ)` by subtracting from each natrual number the number
+  of elements before it in the list which are less then itself. This is used
+  to form a list of pairs which can be used for contracting indices. -/
 def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ) :=
   let l' := l.bind (fun p => [p.1, p.2])
   let l'' := List.mapAccumr
@@ -367,6 +372,7 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
 
 end ProdNode
 
+/-- Returns the full list of indices after contraction. TODO: Include evaluation. -/
 partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   match stx with
   | `(tensorExpr| $_:term | $[$args]*) => do
@@ -402,6 +408,8 @@ partial def getIndicesRight (stx : Syntax) : TermElabM (List (TSyntax `indexExpr
   | _ =>
     throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
 
+/-- Given two lists of indices returns the `List (ℕ)` representing the how one list
+  permutes into the other. -/
 def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ)) := do
   let l1' ← l1.mapM (fun x => indexToIdent x)
   let l2' ← l2.mapM (fun x => indexToIdent x)

HepLean/Tensors/Tree/NodeIdentities/PermContr.lean

@@ -150,6 +150,7 @@ lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     rfl
   exact congrArg (λ f => Action.Hom.hom f) h1
 
+/-- A helper function used to proof the relation between perm and contr. -/
 def contrIsoComm {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :=
   (((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i) :