refactor:Lint

HepLean.lean

@@ -99,6 +99,11 @@ import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
 import HepLean.StandardModel.HiggsBoson.Potential
 import HepLean.StandardModel.Representations
 import HepLean.Tensors.Basic
+import HepLean.Tensors.ComplexLorentz.Basic
+import HepLean.Tensors.ComplexLorentz.ColorFun
+import HepLean.Tensors.ComplexLorentz.ContrNatTransform
+import HepLean.Tensors.ComplexLorentz.Examples
+import HepLean.Tensors.ComplexLorentz.TensorStruct
 import HepLean.Tensors.Contraction
 import HepLean.Tensors.EinsteinNotation.Basic
 import HepLean.Tensors.EinsteinNotation.IndexNotation
@@ -121,6 +126,9 @@ import HepLean.Tensors.IndexNotation.IndexList.Subperm
 import HepLean.Tensors.IndexNotation.IndexString
 import HepLean.Tensors.IndexNotation.TensorIndex
 import HepLean.Tensors.MulActionTensor
+import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Functors
+import HepLean.Tensors.OverColor.Iso
 import HepLean.Tensors.RisingLowering
 import HepLean.Tensors.Tree.Basic
 import HepLean.Tensors.Tree.Dot

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -30,6 +30,7 @@ inductive Color
   | up : Color
   | down : Color
 
+/-- The involution taking a colour to its dual. -/
 def τ : Color → Color
   | Color.upL => Color.downL
   | Color.downL => Color.upL
@@ -38,6 +39,7 @@ def τ : Color → Color
   | Color.up => Color.down
   | Color.down => Color.up
 
+/-- The function taking a color to the dimension of the basis of vectors. -/
 def evalNo : Color → ℕ
   | Color.upL => 2
   | Color.downL => 2

HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean

@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Basic
 import HepLean.Tensors.OverColor.Functors
-import HepLean.Tensors.COmplexLorentz.ColorFun
+import HepLean.Tensors.ComplexLorentz.ColorFun
 import HepLean.Mathematics.PiTensorProduct
 /-!
 
@@ -25,12 +25,10 @@ open IndexNotation
 open CategoryTheory
 open MonoidalCategory
 
-def tensorateContrPair (c : OverColor Color) : (OverColor.contrPair Color τ ⊗⋙ colorFunMon).obj c ≅
-    (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) :=
-  (colorFunMon.μIso c ((OverColor.map τ).obj c)).symm
-
 namespace pairwiseRepFun
 
+/-- Given an object `c : OverColor Color` the representation defined by
+  `⨂[R] x, colorToRep (c.hom x) ⊗[R] colorToRep (τ (c.hom x))`. -/
 def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
   toFun := fun M => PiTensorProduct.map (fun x =>
     TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M)),
@@ -42,7 +40,7 @@ def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
     simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
     apply congrArg
     funext i
-    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _ ) (x' i)
+    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _) (x' i)
     rw [← TensorProduct.map_comp]
     rfl}
 
@@ -59,34 +57,20 @@ lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
     (x : (i : f.left) → (colorToRep (f.hom i)).V ⊗[ℂ] (colorToRep (τ (f.hom i))).V) :
     mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
     PiTensorProduct.tprod ℂ fun i =>
-    (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i ))
-    (colorToRepCongr (mapToLinearEquiv'.proof_4 m i ))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
+    (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
+    (colorToRepCongr (mapToLinearEquiv'.proof_4 m i))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
   simp [mapToLinearEquiv']
-  change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _) (colorToRepCongr _))
-    ((PiTensorProduct.reindex ℂ (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
-        (OverColor.Hom.toEquiv m))
-      ((PiTensorProduct.tprod ℂ) x)) = _
+  change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _)
+    (colorToRepCongr _)) ((PiTensorProduct.reindex ℂ
+    (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
+    (OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _
   rw [PiTensorProduct.reindex_tprod]
   erw [PiTensorProduct.congr_tprod]
   rfl
 
-
 end pairwiseRepFun
 
-def pairwiseRep (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
-  toFun := fun M => PiTensorProduct.map (fun x =>
-    TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M )),
-  map_one' := by
-    simp
-  map_mul' := fun x y => by
-    simp only [Functor.id_obj, _root_.map_mul]
-    ext x' : 2
-    simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
-    apply congrArg
-    funext i
-    change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _ ) (x' i)
-    rw [← TensorProduct.map_comp]
-    rfl}
+/-
 
 def contrPairPairwiseRep (c : OverColor Color) :
     (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) ⟶
@@ -100,8 +84,9 @@ def contrPairPairwiseRep (c : OverColor Color) :
       Action.FunctorCategoryEquivalence.functor_obj_obj, Action.tensor_ρ', LinearMap.coe_comp,
       Function.comp_apply]
     change (TensorProduct.lift
-      (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V ↑(colorToRep (τ (c.hom x))).V))
-      ((TensorProduct.map  _ _)
+      (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
+      ↑(colorToRep (τ (c.hom x))).V))
+      ((TensorProduct.map _ _)
       ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) = _
     rw [TensorProduct.map_tmul]
     erw [colorFun.obj_ρ_tprod, colorFun.obj_ρ_tprod]
@@ -109,7 +94,8 @@ def contrPairPairwiseRep (c : OverColor Color) :
     erw [PiTensorProduct.map₂_tprod_tprod]
     change _ = ((pairwiseRep c).ρ M)
       ((TensorProduct.lift
-        (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V ↑(colorToRep (τ (c.hom x))).V))
+        (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
+        ↑(colorToRep (τ (c.hom x))).V))
       ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y))
     simp only [mk_apply, Functor.id_obj, lift.tmul]
     rw [PiTensorProduct.map₂_tprod_tprod]
@@ -117,7 +103,6 @@ def contrPairPairwiseRep (c : OverColor Color) :
       mk_apply]
     erw [PiTensorProduct.map_tprod]
     rfl
-
-
+-/
 end
 end Fermion

HepLean/Tensors/ComplexLorentz/Examples.lean

@@ -21,11 +21,11 @@ open TensorProduct
 open IndexNotation
 open CategoryTheory
 
-
 noncomputable section
 
 namespace complexLorentzTensor
 
+/-- The color map for a 2d tensor with the first index up and the second index down. -/
 def upDown : Fin 2 → complexLorentzTensor.C
   | 0 => Fermion.Color.up
   | 1 => Fermion.Color.down

HepLean/Tensors/ComplexLorentz/TensorStruct.lean

@@ -20,9 +20,9 @@ open TensorProduct
 open IndexNotation
 open CategoryTheory
 
-
 noncomputable section
 
+/-- The tensor structure for complex Lorentz tensors. -/
 def complexLorentzTensor : TensorStruct where
   C := Fermion.Color
   G := SL(2, ℂ)

HepLean/Tensors/OverColor/Basic.lean

@@ -65,6 +65,7 @@ lemma toEquiv_comp_inv_apply (m : f ⟶ g) (i : g.left) :
     f.hom ((OverColor.Hom.toEquiv m).symm i) = g.hom i := by
   simpa [toEquiv, types_comp] using congrFun m.inv.w i
 
+/-- Given a morphism in `OverColor C`, the corresponding isomorphism. -/
 def toIso (m : f ⟶ g) : f ≅ g := {
   hom := m,
   inv := m.symm,

HepLean/Tensors/OverColor/Functors.lean

@@ -14,7 +14,6 @@ namespace OverColor
 open CategoryTheory
 open MonoidalCategory
 
-
 /-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map
   `f : C → D`. -/
 def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where
@@ -50,7 +49,7 @@ def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D)
     | Sum.inr x => rfl
 
 /-- The tensor product on `OverColor C` as a monoidal functor. -/
-def tensor (C : Type)  : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
+def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
   toFunctor := MonoidalCategory.tensor (OverColor C)
   ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
     ext x
@@ -93,13 +92,16 @@ def tensor (C : Type)  : MonoidalFunctor (OverColor C × OverColor C) (OverColor
     | Sum.inl (Sum.inr x) => rfl
     | Sum.inr x => exact Empty.elim x
 
+/-- The monoidal functor from `OverColor C` to `OverColor C × OverColor C` landing on the
+  diagonal. -/
 def diag (C : Type) : MonoidalFunctor (OverColor C) (OverColor C × OverColor C) :=
   MonoidalFunctor.diag (OverColor C)
 
+/-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/
 def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where
   toFunctor := (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
   ε := 𝟙 (𝟙_ (OverColor C))
-  μ _ _:= (λ_  (𝟙_ (OverColor C))).hom
+  μ _ _:= (λ_ (𝟙_ (OverColor C))).hom
   μ_natural_left _ _ := by
     simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
       Category.id_comp, Iso.hom_inv_id, Category.comp_id]
@@ -120,9 +122,11 @@ def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where
     | Sum.inl i => exact Empty.elim i
     | Sum.inr i => exact Empty.elim i
 
+/-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/
 def contrPair (C : Type) (τ : C → C) : MonoidalFunctor (OverColor C) (OverColor C) :=
   OverColor.diag C
   ⊗⋙ (MonoidalFunctor.prod (MonoidalFunctor.id (OverColor C)) (OverColor.map τ))
   ⊗⋙ OverColor.tensor C
+
 end OverColor
 end IndexNotation

HepLean/Tensors/OverColor/Iso.lean

@@ -25,6 +25,7 @@ open MonoidalCategory
 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))
 
+/-- Given a map `X ⊕ Y → C`, the isomorphism `mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr)`. -/
 def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr) :=
   Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
     ext x
@@ -32,6 +33,7 @@ def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.in
     | Sum.inl x => rfl
     | Sum.inr x => 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
@@ -53,11 +55,13 @@ lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
   simp only [Nat.succ_eq_add_one, finExtractOne, Function.comp_apply, Equiv.symm_trans_apply,
     finCongr_symm, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply,
     Equiv.coe_refl, Sum.map_inr, finCongr_apply, Fin.coe_cast]
-  change (finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
-        ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
+  change (finSumFinEquiv
+    (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
+    ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm
+    (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
   by_cases hi : x.1 < i.1
   · have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
-        Sum.inl ⟨x, hi⟩  := by
+        Sum.inl ⟨x, hi⟩ := by
       rw [← finSumFinEquiv_symm_apply_castAdd]
       apply congrArg
       ext
@@ -78,7 +82,7 @@ lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
       rw [← finSumFinEquiv_symm_apply_natAdd]
       apply congrArg
       ext
-      simp
+      simp only [Nat.succ_eq_add_one, Fin.coe_cast, Fin.natAdd_mk]
       omega
     rw [h1, Fin.succAbove]
     split
@@ -91,8 +95,8 @@ lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
 @[simp]
 lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
     (finExtractOne i).symm (Sum.inr x) = i.succAbove x := calc
-  _ = ((finExtractOne i).symm ∘ Sum.inr) x  := rfl
-  _ = i.succAbove x  := by rw [finExtractOne_symm_inr]
+  _ = ((finExtractOne i).symm ∘ Sum.inr) x := rfl
+  _ = i.succAbove x := by rw [finExtractOne_symm_inr]
 
 @[simp]
 lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
@@ -104,6 +108,8 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
   ext
   rfl
 
+/-- The equivalence of types `Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n` extracting
+  the `i` and `(i.succAbove j)`. -/
 def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
     Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n :=
   (finExtractOne i).trans <|
@@ -129,11 +135,14 @@ lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin
   simp
 
 @[simp]
-lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)  :
+lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
     (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := by
   rw [finExtractTwo]
   simp
 
+/-- The isomorphism between a `Fin 1 ⊕ Fin 1 → C` satisfying the condition
+  `c (Sum.inr 0) = τ (c (Sum.inl 0))`
+  and an object in the image of `contrPair`. -/
 def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
     (h : c (Sum.inr 0) = τ (c (Sum.inl 0))) :
     OverColor.mk c ≅ (contrPair C τ).obj (OverColor.mk (fun (_ : Fin 1) => c (Sum.inl 0))) :=
@@ -149,6 +158,8 @@ def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
       rw [h]
       rfl))
 
+/-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the
+  image of `contrPair` based on the given values. -/
 def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ)
     (j : Fin n.succ) (h : c (i.succAbove j) = τ (c i)) :
     OverColor.mk c ≅ ((contrPair C τ).obj (Over.mk (fun (_ : Fin 1) => c i))) ⊗

HepLean/Tensors/Tree/Basic.lean

@@ -64,7 +64,8 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
     (i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 →
     TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm)
   | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
-    (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
+    (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
+    TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
   | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
     TensorTree S (Function.update c i (S.τ (c i)))
   | eval {n : ℕ} {c : Fin n.succ → S.C} :