refactor: Linting

HepLean.lean

@@ -23,7 +23,7 @@ import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
 import HepLean.AnomalyCancellation.PureU1.Odd.Parameterization
 import HepLean.AnomalyCancellation.PureU1.Permutations
-import HepLean.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.VectorLike
 import HepLean.AnomalyCancellation.SM.Basic
 import HepLean.AnomalyCancellation.SM.FamilyMaps
@@ -71,7 +71,7 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Restricted
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.LorentzTensor.Basic
-import HepLean.SpaceTime.LorentzTensor.Contractions
+import HepLean.SpaceTime.LorentzTensor.Contraction
 import HepLean.SpaceTime.LorentzTensor.Fin
 import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 import HepLean.SpaceTime.LorentzTensor.Notation

HepLean/AnomalyCancellation/PureU1/ConstAbs.lean

@@ -3,7 +3,7 @@ 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.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.VectorLike
 /-!
 # Charges assignments with constant abs

HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -3,7 +3,7 @@ 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.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
 import Mathlib.Logic.Equiv.Fin

HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -3,7 +3,7 @@ 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.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.Sorts
 import HepLean.AnomalyCancellation.PureU1.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.VectorLike
 import Mathlib.Logic.Equiv.Fin

HepLean/AnomalyCancellation/PureU1/VectorLike.lean

@@ -3,7 +3,7 @@ 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.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.Sorts
 import Mathlib.Logic.Equiv.Fin
 /-!
 # Vector like charges

HepLean/SpaceTime/LorentzTensor/Basic.lean

@@ -34,6 +34,7 @@ open TensorProduct
 
 variable {R : Type} [CommSemiring R]
 
+/-- An auxillary function to contract the vector space `V1` and `V2` in  `V1 ⊗[R] V2 ⊗[R] V3`. -/
 def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
     [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
     V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 :=
@@ -41,9 +42,11 @@ def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [Ad
   TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap
   ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap
 
+/-- An auxillary function to contract the vector space `V1` and `V2` in
+  `V4 ⊗[R] V1 ⊗[R] V2 ⊗[R] V3`. -/
 def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
-    [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] (f : V1 ⊗[R] V2 →ₗ[R] R) :
-    (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 :=
+    [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4]
+    (f : V1 ⊗[R] V2 →ₗ[R] R) : (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 :=
   (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ
   (TensorProduct.assoc R _ _ _).toLinearMap
 

HepLean/SpaceTime/LorentzTensor/Contraction.lean

@@ -51,25 +51,12 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
 
 -/
 
-def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
-    [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
-    V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 :=
-  (TensorProduct.lid R _).toLinearMap ∘ₗ
-  TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap
-  ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap
-
 /-- The contraction of a vector in `𝓣.ColorModule ν` with a vector in
   `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in `𝓣.ColorModule η`. -/
 def contrDualLeft {ν η : 𝓣.Color} :
     𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η →ₗ[R] 𝓣.ColorModule η :=
   contrDualLeftAux (𝓣.contrDual ν)
 
-def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
-    [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] (f : V1 ⊗[R] V2 →ₗ[R] R) :
-    (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 :=
-  (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ
-  (TensorProduct.assoc R _ _ _).toLinearMap
-
 /-- The contraction of a vector in `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν` with a vector in
   `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in
   `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule η`. -/

HepLean/SpaceTime/LorentzTensor/Fin.lean

@@ -35,10 +35,13 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
   {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
   {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
 
+/-- Casting a tensor defined on `Fin n` to `Fin m` where `n = m`. -/
 @[simp]
 def finCast (h : n = m) (hc : cn = cm ∘ Fin.castOrderIso h) : 𝓣.Tensor cn ≃ₗ[R] 𝓣.Tensor cm :=
   𝓣.mapIso (Fin.castOrderIso h) hc
 
+/-- An equivalence between `𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm` indexed by `Fin n` and `Fin m`,
+  and `𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm)` indexed by `Fin (n + m)`. -/
 @[simp]
 def finSumEquiv : 𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm ≃ₗ[R]
     𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm) :=

HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean

@@ -3,7 +3,7 @@ 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.SpaceTime.LorentzTensor.Contractions
+import HepLean.SpaceTime.LorentzTensor.Contraction
 import Mathlib.RepresentationTheory.Basic
 /-!
 
@@ -19,6 +19,8 @@ variable {R : Type} [CommSemiring R]
 
 /-! TODO: Add preservation of the unit, and the metric. -/
 
+/-- A multiplicative action on a tensor structure (e.g. the action of the Lorentz
+  group on real Lorentz tensors). -/
 class MulActionTensor (G : Type) [Monoid G] (𝓣 : TensorStructure R) where
   /-- For each color `μ` a representation of `G` on `ColorModule μ`. -/
   repColorModule : (μ : 𝓣.Color) → Representation R G (𝓣.ColorModule μ)
@@ -42,12 +44,14 @@ variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [De
 
 -/
 
+/-- The `MulActionTensor` defined by restriction along a group homomorphism. -/
 def compHom (f : H →* G) : MulActionTensor H 𝓣 where
   repColorModule μ := MonoidHom.comp (repColorModule μ) f
   contrDual_inv μ h := by
     simp only [MonoidHom.coe_comp, Function.comp_apply]
     rw [contrDual_inv]
 
+/-- The trivial `MulActionTensor` defined via trivial representations. -/
 def trivial : MulActionTensor G 𝓣 where
   repColorModule μ := Representation.trivial R
   contrDual_inv μ g := by

HepLean/SpaceTime/LorentzTensor/Real/Basic.lean

@@ -23,6 +23,8 @@ variable {d : ℕ}
 ## Definitions and lemmas needed to define a `LorentzTensorStructure`
 
 -/
+
+/-- The type colors for real Lorentz tensors. -/
 inductive ColorType
   | up
   | down
@@ -34,57 +36,57 @@ open realTensor
 /-! TODO: Set up the notation `𝓛𝓣ℝ` or similar. -/
 /-- The `LorentzTensorStructure` associated with real Lorentz tensors. -/
 def realLorentzTensor (d : ℕ) : TensorStructure ℝ where
-    Color := ColorType
-    ColorModule μ :=
-      match μ with
-      | .up => LorentzVector d
-      | .down => CovariantLorentzVector d
-    τ μ :=
-      match μ with
-      | .up => .down
-      | .down => .up
-    τ_involutive μ :=
-      match μ with
-      | .up => rfl
-      | .down => rfl
-    colorModule_addCommMonoid μ :=
-      match μ with
-      | .up => instAddCommMonoidLorentzVector d
-      | .down => instAddCommMonoidCovariantLorentzVector d
-    colorModule_module μ :=
-      match μ with
-      | .up => instModuleRealLorentzVector d
-      | .down => instModuleRealCovariantLorentzVector d
-    contrDual μ :=
-      match μ with
-      | .up => LorentzVector.contrUpDown
-      | .down => LorentzVector.contrDownUp
-    contrDual_symm μ :=
-      match μ with
-      | .up => by
-        intro x y
-        simp only [LorentzVector.contrDownUp, Equiv.cast_refl, Equiv.refl_apply, LinearMap.coe_comp,
-          LinearEquiv.coe_coe, Function.comp_apply, comm_tmul]
-      | .down => by
-        intro x y
-        simp only [LorentzVector.contrDownUp, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
-          comm_tmul, Equiv.cast_refl, Equiv.refl_apply]
-    unit μ :=
-      match μ with
-      | .up => LorentzVector.unitUp
-      | .down => LorentzVector.unitDown
-    unit_lid μ :=
-      match μ with
-      | .up => LorentzVector.unitUp_lid
-      | .down => LorentzVector.unitDown_lid
-    metric μ :=
-      match μ with
-      | realTensor.ColorType.up => asProdLorentzVector
-      | realTensor.ColorType.down => asProdCovariantLorentzVector
-    metric_dual μ :=
-      match μ with
-      | realTensor.ColorType.up => asProdLorentzVector_contr_asCovariantProdLorentzVector
-      | realTensor.ColorType.down => asProdCovariantLorentzVector_contr_asProdLorentzVector
+  Color := ColorType
+  ColorModule μ :=
+    match μ with
+    | .up => LorentzVector d
+    | .down => CovariantLorentzVector d
+  τ μ :=
+    match μ with
+    | .up => .down
+    | .down => .up
+  τ_involutive μ :=
+    match μ with
+    | .up => rfl
+    | .down => rfl
+  colorModule_addCommMonoid μ :=
+    match μ with
+    | .up => instAddCommMonoidLorentzVector d
+    | .down => instAddCommMonoidCovariantLorentzVector d
+  colorModule_module μ :=
+    match μ with
+    | .up => instModuleRealLorentzVector d
+    | .down => instModuleRealCovariantLorentzVector d
+  contrDual μ :=
+    match μ with
+    | .up => LorentzVector.contrUpDown
+    | .down => LorentzVector.contrDownUp
+  contrDual_symm μ :=
+    match μ with
+    | .up => by
+      intro x y
+      simp only [LorentzVector.contrDownUp, Equiv.cast_refl, Equiv.refl_apply, LinearMap.coe_comp,
+        LinearEquiv.coe_coe, Function.comp_apply, comm_tmul]
+    | .down => by
+      intro x y
+      simp only [LorentzVector.contrDownUp, LinearMap.coe_comp, LinearEquiv.coe_coe,
+        Function.comp_apply, comm_tmul, Equiv.cast_refl, Equiv.refl_apply]
+  unit μ :=
+    match μ with
+    | .up => LorentzVector.unitUp
+    | .down => LorentzVector.unitDown
+  unit_lid μ :=
+    match μ with
+    | .up => LorentzVector.unitUp_lid
+    | .down => LorentzVector.unitDown_lid
+  metric μ :=
+    match μ with
+    | realTensor.ColorType.up => asProdLorentzVector
+    | realTensor.ColorType.down => asProdCovariantLorentzVector
+  metric_dual μ :=
+    match μ with
+    | realTensor.ColorType.up => asProdLorentzVector_contr_asCovariantProdLorentzVector
+    | realTensor.ColorType.down => asProdCovariantLorentzVector_contr_asProdLorentzVector
 
 /-- The action of the Lorentz group on real Lorentz tensors. -/
 instance : MulActionTensor (LorentzGroup d) (realLorentzTensor d) where

HepLean/SpaceTime/LorentzVector/Contraction.lean

@@ -27,6 +27,8 @@ namespace LorentzVector
 open Matrix
 variable {d : ℕ} (v : LorentzVector d)
 
+/-- The bi-linear map defining the contraction of a contravariant Lorentz vector
+  and a covariant Lorentz vector. -/
 def contrUpDownBi : LorentzVector d →ₗ[ℝ] CovariantLorentzVector d →ₗ[ℝ] ℝ where
   toFun v := {
     toFun := fun w => ∑ i, v i * w i,
@@ -57,6 +59,8 @@ def contrUpDownBi : LorentzVector d →ₗ[ℝ] CovariantLorentzVector d →ₗ[
     simp only [RingHom.id, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, id_eq]
     ring
 
+/-- The linear map defining the contraction of a contravariant Lorentz vector
+  and a covariant Lorentz vector. -/
 def contrUpDown : LorentzVector d ⊗[ℝ] CovariantLorentzVector d →ₗ[ℝ] ℝ :=
   TensorProduct.lift contrUpDownBi
 
@@ -93,6 +97,8 @@ lemma contrUpDown_stdBasis_right (x : CovariantLorentzVector d) (i : Fin 1 ⊕ F
   simp only [LinearMap.stdBasis_apply', ite_eq_right_iff, one_ne_zero, imp_false]
   exact Or.intro_left (x b = 0) (id (Ne.symm hbi))
 
+/-- The linear map defining the contraction of a covariant Lorentz vector
+  and a contravariant Lorentz vector. -/
 def contrDownUp : CovariantLorentzVector d ⊗[ℝ] LorentzVector d →ₗ[ℝ] ℝ :=
   contrUpDown ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap
 
@@ -107,6 +113,8 @@ lemma contrDownUp_tmul_eq_dotProduct {x : CovariantLorentzVector d} {y : Lorentz
 
 -/
 
+/-- The unit of the contraction of contravariant Lorentz vector and a
+  covariant Lorentz vector. -/
 def unitUp : LorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
   ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i
 
@@ -122,6 +130,8 @@ lemma unitUp_lid (x : LorentzVector d) :
     LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul,
     contrUpDown_stdBasis_left, rid_tmul, decomp_stdBasis']
 
+/-- The unit of the contraction of covariant Lorentz vector and a
+  contravariant Lorentz vector. -/
 def unitDown : CovariantLorentzVector d ⊗[ℝ] LorentzVector d :=
   ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i
 
@@ -168,9 +178,11 @@ open LorentzVector
 open scoped minkowskiMatrix
 variable {d : ℕ}
 
+/-- The metric tensor as an element of `LorentzVector d ⊗[ℝ] LorentzVector d`. -/
 def asProdLorentzVector : LorentzVector d ⊗[ℝ] LorentzVector d :=
   ∑ μ, η μ μ • (LorentzVector.stdBasis μ ⊗ₜ[ℝ] LorentzVector.stdBasis μ)
 
+/-- The metric tensor as an element of `CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d`. -/
 def asProdCovariantLorentzVector : CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
   ∑ μ, η μ μ • (CovariantLorentzVector.stdBasis μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis μ)
 

HepLean/SpaceTime/LorentzVector/Covariant.lean

@@ -61,7 +61,8 @@ lemma decomp_stdBasis (v : CovariantLorentzVector d) : ∑ i, v i • stdBasis i
 
 @[simp]
 lemma decomp_stdBasis' (v : CovariantLorentzVector d) :
-    v (Sum.inl 0) • stdBasis (Sum.inl 0) + ∑ a₂ : Fin d, v (Sum.inr a₂) • stdBasis (Sum.inr a₂) = v := by
+    v (Sum.inl 0) • stdBasis (Sum.inl 0)
+    + ∑ a₂ : Fin d, v (Sum.inr a₂) • stdBasis (Sum.inr a₂) = v := by
   trans ∑ i, v i • stdBasis i
   simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
     Finset.sum_singleton]
@@ -83,7 +84,7 @@ def rep : Representation ℝ (LorentzGroup d) (CovariantLorentzVector d) where
       lorentzGroupIsGroup_mul_coe, map_mul]
 
 open Matrix in
-@[simp]
+
 lemma rep_apply (g : LorentzGroup d) : rep g v = (g.1⁻¹)ᵀ *ᵥ v := by
   trans (LorentzGroup.transpose g⁻¹) *ᵥ v
   rfl

HepLean/SpaceTime/LorentzVector/LorentzAction.lean

@@ -26,7 +26,6 @@ def rep : Representation ℝ (LorentzGroup d) (LorentzVector d) where
     simp only [lorentzGroupIsGroup_mul_coe, map_mul]
 
 open Matrix in
-@[simp]
 lemma rep_apply (g : LorentzGroup d) : rep g v = g *ᵥ v := rfl
 
 end LorentzVector