From 1384239f71b4782d62b2a6bb0b41e4a7d577f451 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 14 Jun 2024 15:38:16 -0400 Subject: [PATCH] feat: symmetry factor and connectedness --- HepLean/FeynmanDiagrams/PhiFour/Basic.lean | 362 ++++++++++++++++++++- README.md | 6 +- 2 files changed, 361 insertions(+), 7 deletions(-) diff --git a/HepLean/FeynmanDiagrams/PhiFour/Basic.lean b/HepLean/FeynmanDiagrams/PhiFour/Basic.lean index b894dc6..6291b2c 100644 --- a/HepLean/FeynmanDiagrams/PhiFour/Basic.lean +++ b/HepLean/FeynmanDiagrams/PhiFour/Basic.lean @@ -8,6 +8,11 @@ import Mathlib.Tactic.FinCases import Mathlib.Data.Finset.Card import Mathlib.CategoryTheory.IsomorphismClasses import Mathlib.Data.Fintype.Pi +import Mathlib.CategoryTheory.Limits.Shapes.Terminal +import Mathlib.Data.Fintype.Prod +import Mathlib.Data.Fintype.Perm +import Mathlib.Combinatorics.SimpleGraph.Basic +import Mathlib.Combinatorics.SimpleGraph.Connectivity /-! # Feynman diagrams in Phi^4 theory @@ -24,8 +29,10 @@ factors of Feynman diagrams? , URL (version: 2010-06-03): https://mathoverflow.n ## TODO - Develop a way to display Feynman diagrams. -- Define the symmetry factor and compute for examples of Feynman diagrams. +- Define a connected diagram. - Define the Feynman rules, and perform an example calculation. +- Determine an efficent way to calculate symmetry factors. Currently there is a method, but +it will not work for large diagrams as it scales factorially with the number of half-edges. -/ @@ -155,6 +162,300 @@ instance {𝓱π“₯ π“₯ : Type} [Fintype 𝓱π“₯] [DecidableEq 𝓱π“₯] [Deci end Decidability +section Finiteness +/-! +## Finiteness + +As defined above our Feynman diagrams can have non-finite Types of half-edges etc. +We define the class of those Feynman diagrams which are `finite` in the appropriate sense. +In practice, every Feynman diagram considered in the physics literature is `finite`. + +-/ + +/-- A Feynman diagram is said to be finite if its type of half-edges, edges and vertices +are finite and decidable. -/ +class IsFiniteDiagram (F : FeynmanDiagram) where + /-- The type `𝓔` is finite. -/ + 𝓔Fintype : Fintype F.𝓔 + /-- The type `𝓔` is decidable. -/ + 𝓔DecidableEq : DecidableEq F.𝓔 + /-- The type `π“₯` is finite. -/ + π“₯Fintype : Fintype F.π“₯ + /-- The type `π“₯` is decidable. -/ + π“₯DecidableEq : DecidableEq F.π“₯ + /-- The type `𝓱𝓔` is finite. -/ + 𝓱𝓔Fintype : Fintype F.𝓱𝓔 + /-- The type `𝓱𝓔` is decidable. -/ + 𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔 + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.𝓔 := + IsFiniteDiagram.𝓔Fintype + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.𝓔 := + IsFiniteDiagram.𝓔DecidableEq + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.π“₯ := + IsFiniteDiagram.π“₯Fintype + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.π“₯ := + IsFiniteDiagram.π“₯DecidableEq + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 := + IsFiniteDiagram.𝓱𝓔Fintype + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 := + IsFiniteDiagram.𝓱𝓔DecidableEq + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Decidable (Nonempty F.π“₯) := + decidable_of_iff _ Finset.univ_nonempty_iff + +end Finiteness + +section categoryOfFeynmanDiagrams +/-! + +## The category of Feynman diagrams + +Feynman diagrams, as defined above, form a category. +We will be able to use this category to define the symmetry factor of a Feynman diagram, +and the condition on whether a diagram is connected. + +-/ +/-- A morphism between two `FeynmanDiagram`. -/ +structure Hom (F1 F2 : FeynmanDiagram) where + /-- A morphism between half-edges. -/ + 𝓱𝓔 : F1.𝓱𝓔 ⟢ F2.𝓱𝓔 + /-- A morphism between edges. -/ + 𝓔 : F1.𝓔 ⟢ F2.𝓔 + /-- A morphism between vertices. -/ + π“₯ : F1.π“₯ ⟢ F2.π“₯ + /-- The morphism between edges must respect the labels. -/ + 𝓔Label : F1.𝓔Label = F2.𝓔Label ∘ 𝓔 + /-- The morphism between vertices must respect the labels. -/ + π“₯Label : F1.π“₯Label = F2.π“₯Label ∘ π“₯ + /-- The morphism between edges and half-edges must commute with `𝓱𝓔To𝓔`. -/ + 𝓱𝓔To𝓔 : 𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ 𝓱𝓔 + /-- The morphism between vertices and half-edges must commute with `𝓱𝓔Toπ“₯`. -/ + 𝓱𝓔Toπ“₯ : π“₯ ∘ F1.𝓱𝓔Toπ“₯ = F2.𝓱𝓔Toπ“₯ ∘ 𝓱𝓔 + +namespace Hom + +lemma ext {F1 F2 : FeynmanDiagram} {f g : Hom F1 F2} (h1 : f.𝓱𝓔 = g.𝓱𝓔) + (h2 : f.𝓔 = g.𝓔) (h3 : f.π“₯ = g.π“₯) : f = g := by + cases f; cases g + simp_all only + +/-- The identity morphism from a Feynman diagram to itself. -/ +@[simps!] +def id (F : FeynmanDiagram) : Hom F F where + 𝓱𝓔 := πŸ™ F.𝓱𝓔 + 𝓔 := πŸ™ F.𝓔 + π“₯ := πŸ™ F.π“₯ + 𝓔Label := rfl + π“₯Label := rfl + 𝓱𝓔To𝓔 := rfl + 𝓱𝓔Toπ“₯ := rfl + +/-- Composition of morphisms between Feynman diagrams. -/ +@[simps!] +def comp {F1 F2 F3 : FeynmanDiagram} (f : Hom F1 F2) (g : Hom F2 F3) : Hom F1 F3 where + 𝓱𝓔 := f.𝓱𝓔 ≫ g.𝓱𝓔 + 𝓔 := f.𝓔 ≫ g.𝓔 + π“₯ := f.π“₯ ≫ g.π“₯ + 𝓔Label := by + ext + simp [f.𝓔Label, g.𝓔Label] + π“₯Label := by + ext x + simp [f.π“₯Label, g.π“₯Label] + 𝓱𝓔To𝓔 := by + rw [types_comp, types_comp, Function.comp.assoc] + rw [f.𝓱𝓔To𝓔, ← Function.comp.assoc, g.𝓱𝓔To𝓔] + rfl + 𝓱𝓔Toπ“₯ := by + rw [types_comp, types_comp, Function.comp.assoc] + rw [f.𝓱𝓔Toπ“₯, ← Function.comp.assoc, g.𝓱𝓔Toπ“₯] + rfl + +/-- The condition on a triplet of maps for them to form a morphism of Feynman diagrams. -/ +def Cond {F1 F2 : FeynmanDiagram} (f𝓱𝓔 : F1.𝓱𝓔 β†’ F2.𝓱𝓔) (f𝓔 : F1.𝓔 β†’ F2.𝓔) + (fπ“₯ : F1.π“₯ β†’ F2.π“₯) : Prop := + F1.𝓔Label = F2.𝓔Label ∘ f𝓔 ∧ F1.π“₯Label = F2.π“₯Label ∘ fπ“₯ ∧ + f𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ f𝓱𝓔 ∧ fπ“₯ ∘ F1.𝓱𝓔Toπ“₯ = F2.𝓱𝓔Toπ“₯ ∘ f𝓱𝓔 + +instance {F1 F2 : FeynmanDiagram} [IsFiniteDiagram F1] [IsFiniteDiagram F2] + (f𝓱𝓔 : F1.𝓱𝓔 β†’ F2.𝓱𝓔) (f𝓔 : F1.𝓔 β†’ F2.𝓔) (fπ“₯ : F1.π“₯ β†’ F2.π“₯) : + Decidable (Cond f𝓱𝓔 f𝓔 fπ“₯) := + @And.decidable _ _ _ $ + @And.decidable _ _ _ $ + @And.decidable _ _ _ _ + +end Hom + +@[simps!] +instance : Category FeynmanDiagram where + Hom := Hom + id := Hom.id + comp := Hom.comp + + +/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram + to its set of half-edges. -/ +def toHalfEdges : FeynmanDiagram β₯€ Type where + obj F := F.𝓱𝓔 + map f := f.𝓱𝓔 + +/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram + to its set of edges. -/ +def toEdges : FeynmanDiagram β₯€ Type where + obj F := F.𝓔 + map f := f.𝓔 + +/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram + to its set of vertices. -/ +def toVertices : FeynmanDiagram β₯€ Type where + obj F := F.π“₯ + map f := f.π“₯ + +lemma 𝓱𝓔_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟢ F2) [IsIso f] : + f.𝓱𝓔.Bijective := + (isIso_iff_bijective f.𝓱𝓔).mp $ Functor.map_isIso toHalfEdges f + +lemma 𝓔_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟢ F2) [IsIso f] : + f.𝓔.Bijective := + (isIso_iff_bijective f.𝓔).mp $ Functor.map_isIso toEdges f + +lemma π“₯_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟢ F2) [IsIso f] : + f.π“₯.Bijective := + (isIso_iff_bijective f.π“₯).mp $ Functor.map_isIso toVertices f + +/-- An isomorphism formed from an equivalence between the types of half-edges, edges and vertices + satisfying the appropriate conditions. -/ +def mkIso {F1 F2 : FeynmanDiagram} (f𝓱𝓔 : F1.𝓱𝓔 ≃ F2.𝓱𝓔) + (f𝓔 : F1.𝓔 ≃ F2.𝓔) (fπ“₯ : F1.π“₯ ≃ F2.π“₯) + (h𝓔Label : F1.𝓔Label = F2.𝓔Label ∘ f𝓔) + (hπ“₯Label : F1.π“₯Label = F2.π“₯Label ∘ fπ“₯) + (h𝓱𝓔To𝓔 : f𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ f𝓱𝓔) + (h𝓱𝓔Toπ“₯ : fπ“₯ ∘ F1.𝓱𝓔Toπ“₯ = F2.𝓱𝓔Toπ“₯ ∘ f𝓱𝓔) : F1 β‰… F2 where + hom := Hom.mk f𝓱𝓔 f𝓔 fπ“₯ h𝓔Label hπ“₯Label h𝓱𝓔To𝓔 h𝓱𝓔Toπ“₯ + inv := Hom.mk f𝓱𝓔.symm f𝓔.symm fπ“₯.symm + (((Iso.eq_inv_comp f𝓔.toIso).mpr h𝓔Label.symm).trans (types_comp _ _)) + (((Iso.eq_inv_comp fπ“₯.toIso).mpr hπ“₯Label.symm).trans (types_comp _ _)) + ((Iso.comp_inv_eq f𝓔.toIso).mpr $ (Iso.eq_inv_comp f𝓱𝓔.toIso).mpr $ + (types_comp _ _).symm.trans (Eq.trans h𝓱𝓔To𝓔.symm (types_comp _ _))) + ((Iso.comp_inv_eq fπ“₯.toIso).mpr $ (Iso.eq_inv_comp f𝓱𝓔.toIso).mpr $ + (types_comp _ _).symm.trans (Eq.trans h𝓱𝓔Toπ“₯.symm (types_comp _ _))) + hom_inv_id := by + apply Hom.ext + ext a + simp only [instCategory_comp_𝓱𝓔, Equiv.symm_apply_apply, instCategory_id_𝓱𝓔] + ext a + simp only [instCategory_comp_𝓔, Equiv.symm_apply_apply, instCategory_id_𝓔] + ext a + simp only [instCategory_comp_π“₯, Equiv.symm_apply_apply, instCategory_id_π“₯] + inv_hom_id := by + apply Hom.ext + ext a + simp only [instCategory_comp_𝓱𝓔, Equiv.apply_symm_apply, instCategory_id_𝓱𝓔] + ext a + simp only [instCategory_comp_𝓔, Equiv.apply_symm_apply, instCategory_id_𝓔] + ext a + simp only [instCategory_comp_π“₯, Equiv.apply_symm_apply, instCategory_id_π“₯] + +lemma isIso_of_bijections {F1 F2 : FeynmanDiagram} (f : F1 ⟢ F2) + (h𝓱𝓔 : f.𝓱𝓔.Bijective) (h𝓔 : f.𝓔.Bijective) (hπ“₯ : f.π“₯.Bijective) : + IsIso f := + Iso.isIso_hom $ mkIso (Equiv.ofBijective f.𝓱𝓔 h𝓱𝓔) (Equiv.ofBijective f.𝓔 h𝓔) + (Equiv.ofBijective f.π“₯ hπ“₯) f.𝓔Label f.π“₯Label f.𝓱𝓔To𝓔 f.𝓱𝓔Toπ“₯ + + +lemma isIso_iff_all_bijective {F1 F2 : FeynmanDiagram} (f : F1 ⟢ F2) : + IsIso f ↔ f.𝓱𝓔.Bijective ∧ f.𝓔.Bijective ∧ f.π“₯.Bijective := + Iff.intro + (fun _ ↦ βŸ¨π“±π“”_bijective_of_isIso f, 𝓔_bijective_of_isIso f, π“₯_bijective_of_isIso f⟩) + (fun ⟨h𝓱𝓔, h𝓔, hπ“₯⟩ ↦ isIso_of_bijections f h𝓱𝓔 h𝓔 hπ“₯) + +/-- An equivalence between the isomorphism class of a Feynman diagram an + permutations of the half-edges, edges and vertices satisfying the `Hom.cond`. -/ +def isoEquivBijec {F : FeynmanDiagram} : + (F β‰… F) ≃ {S : Equiv.Perm F.𝓱𝓔 Γ— Equiv.Perm F.𝓔 Γ— Equiv.Perm F.π“₯ // + Hom.Cond S.1 S.2.1 S.2.2} where + toFun f := ⟨⟨(toHalfEdges.mapIso f).toEquiv, + (toEdges.mapIso f).toEquiv , (toVertices.mapIso f).toEquiv⟩, + f.hom.𝓔Label, f.hom.π“₯Label, f.hom.𝓱𝓔To𝓔, f.hom.𝓱𝓔Toπ“₯⟩ + invFun S := mkIso S.1.1 S.1.2.1 S.1.2.2 S.2.1 S.2.2.1 S.2.2.2.1 S.2.2.2.2 + left_inv _ := rfl + right_inv _ := rfl + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : + Fintype (F β‰… F) := + Fintype.ofEquiv _ isoEquivBijec.symm + +end categoryOfFeynmanDiagrams + +section symmetryFactors +/-! +## Symmetry factors + +The symmetry factor of a Feynman diagram is the cardinality of the group of automorphisms of that +diagram. In this section we define symmetry factors for Feynman diagrams which are +finite. + +-/ + +/-- The symmetry factor is the cardinality of the set of isomorphisms of the Feynman diagram. -/ +def symmetryFactor (F : FeynmanDiagram) [IsFiniteDiagram F] : β„• := + Fintype.card (F β‰… F) + +end symmetryFactors + +section connectedness +/-! + +## Connectedness + +Given a Feynman diagram we can create a simple graph based on the obvious adjacency relation. +A feynman diagram is connected if its simple graph is connected. + +-/ + +/-- A relation on the vertices of Feynman diagrams. The proposition is true if the two + vertices are not equal and are connected by a single edge. -/ +@[simp] +def adjRelation (F : FeynmanDiagram) : F.π“₯ β†’ F.π“₯ β†’ Prop := fun x y => + x β‰  y ∧ + βˆƒ (a b : F.𝓱𝓔), F.𝓱𝓔To𝓔 a = F.𝓱𝓔To𝓔 b ∧ F.𝓱𝓔Toπ“₯ a = x ∧ F.𝓱𝓔Toπ“₯ b = y + +/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/ +def toSimpleGraph (F : FeynmanDiagram) : SimpleGraph F.π“₯ where + Adj := adjRelation F + symm := by + intro x y h + apply And.intro (Ne.symm h.1) + obtain ⟨a, b, hab⟩ := h.2 + exact ⟨b, a, ⟨hab.1.symm, hab.2.2, hab.2.1⟩⟩ + loopless := by + intro x h + simp at h + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj := fun _ _ => + And.decidable + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : + Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.π“₯) := + @And.decidable _ _ _ _ + +instance {F : FeynmanDiagram} [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. -/ +def Connected (F : FeynmanDiagram) : Prop := F.toSimpleGraph.Connected + +instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Decidable (Connected F) := + PhiFour.FeynmanDiagram.instDecidableConnectedπ“₯ToSimpleGraphOfIsFiniteDiagram + +end connectedness + section examples /-! @@ -162,8 +463,10 @@ section examples In this section we give examples of Feynman diagrams in Phi^4 theory. +Symmetry factors can be compared with e.g. those in +- https://arxiv.org/abs/0907.0859 ---/ +-/ /-- The propagator - - - - - - @@ -180,6 +483,17 @@ def propagator : FeynmanDiagram where 𝓱𝓔Toπ“₯ := ![0, 1] π“₯Fiber := by decide +instance : IsFiniteDiagram propagator where + 𝓔Fintype := Fin.fintype 1 + 𝓔DecidableEq := instDecidableEqFin 1 + π“₯Fintype := Fin.fintype 2 + π“₯DecidableEq := instDecidableEqFin 2 + 𝓱𝓔Fintype := Fin.fintype 2 + 𝓱𝓔DecidableEq := instDecidableEqFin 2 + +lemma propagator_symmetryFactor : symmetryFactor propagator = 2 := by + decide + /-- The figure 8 Feynman diagram _ / \ @@ -191,6 +505,7 @@ def propagator : FeynmanDiagram where / \ \ / \ __ / -/ +@[simps!] def figureEight : FeynmanDiagram where 𝓱𝓔 := Fin 4 𝓔 := Fin 2 @@ -202,15 +517,30 @@ def figureEight : FeynmanDiagram where 𝓱𝓔Toπ“₯ := ![0, 0, 0, 0] π“₯Fiber := by decide +instance : IsFiniteDiagram figureEight where + 𝓔Fintype := Fin.fintype 2 + 𝓔DecidableEq := instDecidableEqFin 2 + π“₯Fintype := Fin.fintype 1 + π“₯DecidableEq := instDecidableEqFin 1 + 𝓱𝓔Fintype := Fin.fintype 4 + 𝓱𝓔DecidableEq := instDecidableEqFin 4 + + +lemma figureEight_connected : Connected figureEight := by + decide + +lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by + decide + /-- The feynman diagram _ _ _ _ _ / \ / \ - - - - - - - - - - - - \ / - \ _ _ _ _ _/ + \ _ _ _ _ _/ -/ -def propagtor1 : FeynmanDiagram where +def diagram1 : FeynmanDiagram where 𝓱𝓔 := Fin 10 𝓔 := Fin 5 𝓔Label := ![0, 0, 0, 0, 0] @@ -221,6 +551,30 @@ def propagtor1 : FeynmanDiagram where 𝓱𝓔Toπ“₯ := ![0, 1, 1, 2, 1, 2, 1, 2, 2, 3] π“₯Fiber := by decide +/-- An example of a disconnected Feynman diagram. -/ +def diagram2 : FeynmanDiagram where + 𝓱𝓔 := Fin 14 + 𝓔 := Fin 7 + 𝓔Label := ![0, 0, 0, 0, 0, 0, 0] + 𝓱𝓔To𝓔 := ![0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6] + 𝓔Fiber := by decide + π“₯ := Fin 5 + π“₯Label := ![0, 0, 1, 1, 1] + 𝓱𝓔Toπ“₯ := ![0, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4] + π“₯Fiber := by decide + +instance : IsFiniteDiagram diagram2 where + 𝓔Fintype := Fin.fintype _ + 𝓔DecidableEq := instDecidableEqFin _ + π“₯Fintype := Fin.fintype _ + π“₯DecidableEq := instDecidableEqFin _ + 𝓱𝓔Fintype := Fin.fintype _ + 𝓱𝓔DecidableEq := instDecidableEqFin _ + +lemma diagram2_not_connected : Β¬ Connected diagram2 := by + decide + + end examples diff --git a/README.md b/README.md index f37e81a..56922cd 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ A project to digitalize high energy physics. - Keep the database up-to date with developments in MathLib4. - Create gitHub workflows of relevance to the high energy physics community. -## Areas of high energy physics currently covered +## Areas of high energy physics with some coverage in HepLean [![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/HepLean/FlavorPhysics/CKMMatrix/Basic.html) @@ -22,7 +22,7 @@ A project to digitalize high energy physics. [![](https://img.shields.io/badge/2HDM-blue)](https://heplean.github.io/HepLean/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html) [![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/HepLean/SpaceTime/LorentzGroup/Basic.html) [![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/HepLean/AnomalyCancellation/Basic.html) - +[![](https://img.shields.io/badge/Feynman_diagrams-blue)](https://heplean.github.io/HepLean/HepLean/FeynmanDiagrams/PhiFour/Basic.html) ## Where to learn more - Read the associated paper: @@ -71,4 +71,4 @@ The installation instructions for Lean 4 are given here: https://leanprover-comm ### Optional extras - [Lean Copilot](https://github.com/lean-dojo/LeanCopilot) allows the use of large language models in Lean. -- [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) allows one to apply a tactic, e.g. `exact?` at each step of a each lemma in a file to see if it completes the goal. This is useful for golfing proofs. +- [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) allows one to apply a tactic, e.g. `exact?` at each step of a lemma in a file to see if it completes the goal. This is useful for golfing proofs.