Merge pull request #62 from HEPLean/Feynman_Diagrams

feat: number of loops of a Feynman diagram

HepLean.lean

@@ -51,6 +51,7 @@ import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
+import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom

HepLean/FeynmanDiagrams/Basic.lean

@@ -204,6 +204,36 @@ instance preimageEdgeMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
 
 /-!
 
+## External and internal Vertices
+
+We say a vertex Label is `external` if it has only one half-edge associated with it.
+Otherwise, we say it is `internal`.
+
+We will show that for `IsFinitePreFeynmanRule` the condition of been external is decidable.
+-/
+
+/-- A vertex is external if it has a single half-edge associated to it. -/
+def External {P : PreFeynmanRule} (v : P.VertexLabel) : Prop :=
+  IsIsomorphic (P.vertexLabelMap v).left (Fin 1)
+
+lemma external_iff_exists_bijection {P : PreFeynmanRule}  (v : P.VertexLabel) :
+    External v ↔ ∃ (κ : (P.vertexLabelMap v).left → Fin 1), Function.Bijective κ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  obtain ⟨κ, κm1, h1, h2⟩ := h
+  let f : (P.vertexLabelMap v).left ≅ (Fin 1) :=  ⟨κ, κm1, h1, h2⟩
+  exact ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f⟩
+  obtain ⟨κ, h1⟩ := h
+  let f : (P.vertexLabelMap v).left ⟶ (Fin 1) := κ
+  have ft : IsIso f := (isIso_iff_bijective κ).mpr h1
+  obtain ⟨fm, hf1, hf2⟩ := ft
+  exact ⟨f, fm, hf1, hf2⟩
+
+instance externalDecidable [IsFinitePreFeynmanRule P] (v : P.VertexLabel) :
+    Decidable (External v) :=
+  decidable_of_decidable_of_iff (external_iff_exists_bijection v).symm
+
+/-!
+
 ## Conditions to form a diagram.
 
 -/
@@ -317,6 +347,12 @@ def 𝓱𝓔 : Type := F.𝓱𝓔To𝓔𝓥.left
 /-- The object in Over P.HalfEdgeLabel generated by a Feynman diagram. -/
 def 𝓱𝓔𝓞 : Over P.HalfEdgeLabel := P.toHalfEdge.obj F.𝓱𝓔To𝓔𝓥
 
+/-- The map `F.𝓱𝓔 → F.𝓔` as an object in `Over F.𝓔 `. -/
+def 𝓱𝓔To𝓔 : Over F.𝓔 := P.toEdge.obj F.𝓱𝓔To𝓔𝓥
+
+/-- The map `F.𝓱𝓔 → F.𝓥` as an object in `Over F.𝓥 `. -/
+def 𝓱𝓔To𝓥 : Over F.𝓥 := P.toVertex.obj F.𝓱𝓔To𝓔𝓥
+
 /-!
 
 ## Making a Feynman diagram
@@ -383,6 +419,13 @@ class IsFiniteDiagram (F : FeynmanDiagram P) where
   /-- The type of half-edges is decidable. -/
   𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
 
+instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
+    [h3 : Fintype 𝓥] [h4 : DecidableEq 𝓥] [h5 : Fintype 𝓱𝓔] [h6 : DecidableEq 𝓱𝓔]
+    (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :
+    IsFiniteDiagram (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C) :=
+  ⟨h1, h2, h3, h4, h5, h6⟩
+
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
   IsFiniteDiagram.𝓔Fintype
 
@@ -401,6 +444,9 @@ instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
   IsFiniteDiagram.𝓱𝓔DecidableEq
 
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] (i : F.𝓱𝓔) (j : F.𝓔) :
+    Decidable (F.𝓱𝓔To𝓔.hom i = j) :=  IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j
+
 instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
     [IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
   instDecidableEqProd
@@ -706,7 +752,7 @@ instance [IsFiniteDiagram F] :
 instance [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
   decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
 
-/-- We say a Feynman diagram is connected if its simple graph is connected. -/
+/-- A Feynman diagram is connected if its simple graph is connected. -/
 def Connected : Prop := F.toSimpleGraph.Connected
 
 instance [IsFiniteDiagram F] : Decidable (Connected F) :=

HepLean/FeynmanDiagrams/Instances/Phi4.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.FeynmanDiagrams.Momentum
 /-!
 # Feynman diagrams in Phi^4 theory
 
@@ -65,6 +65,32 @@ instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
     match v with
     | 0 => instDecidableEqFin _
 
+/-!
+
+## The figure eight diagram
+
+This section provides an example of the use of Feynman diagrams in HepLean.
+
+-/
+section Example
+
+/-- The figure eight Feynman diagram. -/
+abbrev figureEight : FeynmanDiagram phi4PreFeynmanRules :=
+  mk'
+    ![0, 0] -- edges
+    ![1] -- one internal vertex
+    ![⟨0, 0, 0⟩, ⟨0, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 1, 0⟩] -- four half-edges
+    (by decide) -- the condition to form a Feynman diagram.
+
+/-- `figureEight` is connected. We can get this from
+  `#eval Connected figureEight`. -/
+lemma figureEight_connected : Connected figureEight := by decide
+
+/-- The symmetry factor of `figureEight` is 8. We can get this from
+  `#eval symmetryFactor figureEight`. -/
+lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
+
+end Example
 
 
 end PhiFour

HepLean/FeynmanDiagrams/Momentum.lean

@@ -0,0 +1,219 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.LinearAlgebra.StdBasis
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.Data.Matrix.Rank
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.SesquilinearForm
+/-!
+# Momentum in Feynman diagrams
+
+The aim of this file is to associate with each half-edge of a Feynman diagram a momentum,
+and constrain the momentums based conservation at each vertex and edge.
+
+The number of loops of a Feynman diagram is related to the dimension of the resulting
+vector space.
+
+## TODO
+
+- Prove lemmas that make the calcuation of the number of loops of a Feynman diagram easier.
+
+## Note
+
+This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
+-/
+
+
+namespace FeynmanDiagram
+
+open CategoryTheory
+open PreFeynmanRule
+
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P) [IsFiniteDiagram F]
+
+/-!
+
+## Vector spaces associated with momenta in Feynman diagrams.
+
+We define the vector space associated with momenta carried by half-edges,
+outflowing momenta of edges, and inflowing momenta of vertices.
+
+We define the direct sum of the edge and vertex momentum spaces.
+
+-/
+
+/-- The type which assocaites to each half-edge a `1`-dimensional vector space.
+ Corresponding to that spanned by its momentum.  -/
+def HalfEdgeMomenta : Type :=  F.𝓱𝓔 → ℝ
+
+instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
+
+/-- An auxillary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInnerAux (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun y := ∑ i,  (x i) * (y i)
+  map_add' z y :=
+    show (∑ i, (x i) * (z i + y i)) = (∑ i, x i * z i) + ∑ i, x i * (y i) by
+      simp only [mul_add, Finset.sum_add_distrib]
+  map_smul' c y :=
+    show (∑ i, x i * (c * y i)) = c * ∑ i, x i * y i by
+      rw [Finset.mul_sum]
+      refine Finset.sum_congr rfl (fun _ _  => by ring)
+
+lemma euclidInnerAux_symm (x y : F.HalfEdgeMomenta) :
+    F.euclidInnerAux x y = F.euclidInnerAux y x := Finset.sum_congr rfl (fun _ _ => by ring)
+
+/-- The Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun x := F.euclidInnerAux x
+  map_add' x y := by
+    refine LinearMap.ext (fun z  => ?_)
+    simp only [euclidInnerAux_symm, map_add, LinearMap.add_apply]
+  map_smul' c x := by
+    refine LinearMap.ext (fun z  => ?_)
+    simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
+      LinearMap.smul_apply]
+
+
+/-- The type which assocaites to each ege a `1`-dimensional vector space.
+ Corresponding to that spanned by its total outflowing momentum.  -/
+def EdgeMomenta : Type := F.𝓔 → ℝ
+
+instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
+
+
+/-- The type which assocaites to each ege a `1`-dimensional vector space.
+ Corresponding to that spanned by its total inflowing momentum.  -/
+def VertexMomenta : Type := F.𝓥 → ℝ
+
+instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.VertexMomenta := Pi.module _ _ _
+
+/-- The map from `Fin 2` to `Type` landing on `EdgeMomenta` and `VertexMomenta`. -/
+def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
+  match i with
+  | 0 =>  F.EdgeMomenta
+  | 1 =>  F.VertexMomenta
+
+instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instAddCommGroupEdgeMomenta F
+  | 1 => instAddCommGroupVertexMomenta F
+
+instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instModuleRealEdgeMomenta F
+  | 1 => instModuleRealVertexMomenta F
+
+/-- The direct sum of `EdgeMomenta` and `VertexMomenta`.-/
+def EdgeVertexMomenta : Type := DirectSum (Fin 2) (EdgeVertexMomentaMap F)
+
+instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
+
+instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
+
+
+/-!
+
+## Linear maps between the vector spaces.
+
+We define various maps into `F.HalfEdgeMomenta`.
+
+In particular, we define a map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta`. This
+map represents the space orthogonal (with respect to the standard Euclidean inner product)
+to the allowed momenta of half-edges (up-to an offset determined by the
+ external momenta).
+
+The number of loops of a diagram is defined as the number of half-edges minus
+the rank of this matrix.
+
+-/
+
+/-- The linear map from `F.EdgeMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓔.hom`. -/
+def edgeToHalfEdgeMomenta : F.EdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓔.hom
+  map_add' _ _ := by rfl
+  map_smul' _ _ := by rfl
+
+/-- The linear map from `F.VertexMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓥.hom`. -/
+def vertexToHalfEdgeMomenta : F.VertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓥.hom
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/-- The linear map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta` induced by
+   `F.edgeToHalfEdgeMomenta` and `F.vertexToHalfEdgeMomenta`. -/
+def edgeVertexToHalfEdgeMomenta : F.EdgeVertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta :=
+  DirectSum.toModule ℝ (Fin 2) F.HalfEdgeMomenta
+    (fun i => match i with | 0 => F.edgeToHalfEdgeMomenta | 1 => F.vertexToHalfEdgeMomenta)
+
+/-!
+
+## Submodules
+
+We define submodules of `F.HalfEdgeMomenta` which correspond to
+the orthogonal space to allowed momenta (up-to an offset), and the space of
+allowed momenta.
+
+-/
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the range of
+ `F.edgeVertexToHalfEdgeMomenta`. -/
+def orthogHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  LinearMap.range F.edgeVertexToHalfEdgeMomenta
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the allowed momenta. -/
+def allowedHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  Submodule.orthogonalBilin F.orthogHalfEdgeMomenta F.euclidInner
+
+/-!
+
+## Number of loops
+
+We define the number of loops of a Feynman diagram as the dimension of the
+allowed space of half-edge momenta.
+
+-/
+
+/-- The number of loops of a Feynman diagram. Defined as the dimension
+  of the space of allowed Half-loop momenta. -/
+noncomputable def numberOfLoops : ℕ := FiniteDimensional.finrank ℝ F.allowedHalfEdgeMomenta
+
+/-!
+
+## Lemmas regarding `numberOfLoops`
+
+We now give a series of lemmas which be used to help calculate the number of loops
+for specific Feynman diagrams.
+
+### TODO
+
+- Complete this section.
+
+
+-/
+
+/-!
+
+## Category theory
+
+### TODO
+
+- Complete this section.
+
+
+-/
+
+end FeynmanDiagram