DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #60 from HEPLean/Feynman_Diagrams

Browse source 
feat: General definition of Feynman diagram
This commit is contained in:
Joseph Tooby-Smith 2024-06-18 13:19:15 -04:00 • committed by GitHub
commit 9d4d81f9f4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 861 additions and 584 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean.lean
View file

@ -48,7 +48,9 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
import HepLean.BeyondTheStandardModel.TwoHDM.Basic
import HepLean.FeynmanDiagrams.PhiFour.Basic
import HepLean.FeynmanDiagrams.Basic
import HepLean.FeynmanDiagrams.Instances.ComplexScalar
import HepLean.FeynmanDiagrams.Instances.Phi4
import HepLean.FlavorPhysics.CKMMatrix.Basic
import HepLean.FlavorPhysics.CKMMatrix.Invariants
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom

717
HepLean/FeynmanDiagrams/Basic.lean Normal file
View file

@ -0,0 +1,717 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Mathlib.Logic.Equiv.Fin
import Mathlib.Tactic.FinCases
import Mathlib.Data.Finset.Card
import Mathlib.CategoryTheory.IsomorphismClasses
import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Comma.Over
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
import Mathlib.SetTheory.Cardinal.Basic
/-!
# Feynman diagrams
Feynman diagrams are a graphical representation of the terms in the perturbation expansion of
a quantum field theory.
-/
open CategoryTheory
/-!
## The definition of Pre Feynman rules
We define the notion of a pre-Feynman rule, which specifies the possible
half-edges, edges and vertices in a diagram. It does not specify how to turn a diagram
into an algebraic expression.
## TODO
Prove that the `halfEdgeLimit` functor lands on limits of functors.
-/
/-- A `PreFeynmanRule` is a set of rules specifying the allowed half-edges,
edges and vertices in a diagram. (It does not specify how to turn the diagram
into an algebraic expression.) -/
structure PreFeynmanRule where
/-- The type labelling the different half-edges. -/
HalfEdgeLabel : Type
/-- A type labelling the different types of edges. -/
EdgeLabel : Type
/-- A type labelling the different types of vertices. -/
VertexLabel : Type
/-- A function taking `EdgeLabels` to the half edges it contains. -/
edgeLabelMap : EdgeLabel → CategoryTheory.Over HalfEdgeLabel
/-- A function taking `VertexLabels` to the half edges it contains. -/
vertexLabelMap : VertexLabel → CategoryTheory.Over HalfEdgeLabel
namespace PreFeynmanRule
variable (P : PreFeynmanRule)
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
to `Over (P.VertexLabel)` induced by projections on products. -/
@[simps!]
def toVertex {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓥 :=
Over.map <| Prod.snd ∘ Prod.snd
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
to `Over (P.EdgeLabel)` induced by projections on products. -/
@[simps!]
def toEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓔 :=
Over.map <| Prod.fst ∘ Prod.snd
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
to `Over (P.HalfEdgeLabel)` induced by projections on products. -/
@[simps!]
def toHalfEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel :=
Over.map Prod.fst
/-- The functor from `Over P.VertexLabel` to `Type` induced by pull-back along insertion of
`v : P.VertexLabel`. -/
@[simps!]
def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where
obj := fun f => f.hom ⁻¹' {v}
map {f g} F := fun x =>
⟨F.left x.1, by
have h := congrFun F.w x
simp only [Functor.const_obj_obj, Functor.id_obj, Functor.id_map, types_comp_apply,
CostructuredArrow.right_eq_id, Functor.const_obj_map, types_id_apply] at h
simpa [h] using x.2⟩
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`. -/
def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) :
Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
(P.toVertex ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
map {f g} F := Over.homMk ((P.toVertex ⋙ preimageType' v).map F)
(funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
`Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.EdgeLabel`. -/
def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
(P.toEdge ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
(funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
/-!
## Finitness of pre-Feynman rules
We define a class of `PreFeynmanRule` which have nice properties with regard to
decidablity and finitness.
In practice, every pre-Feynman rule considered in the physics literature satisfies these
properties.
-/
/-- A set of conditions on `PreFeynmanRule` for it to be considered finite. -/
class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
/-- The type of edge labels is decidable. -/
edgeLabelDecidable : DecidableEq P.EdgeLabel
/-- The type of vertex labels is decidable. -/
vertexLabelDecidable : DecidableEq P.VertexLabel
/-- The type of half-edge labels is decidable. -/
halfEdgeLabelDecidable : DecidableEq P.HalfEdgeLabel
/-- The type of half-edges associated with a vertex is finite. -/
vertexMapFintype : ∀ v : P.VertexLabel, Fintype (P.vertexLabelMap v).left
/-- The type of half-edges associated with a vertex is decidable. -/
vertexMapDecidable : ∀ v : P.VertexLabel, DecidableEq (P.vertexLabelMap v).left
/-- The type of half-edges associated with an edge is finite. -/
edgeMapFintype : ∀ v : P.EdgeLabel, Fintype (P.edgeLabelMap v).left
/-- The type of half-edges associated with an edge is decidable. -/
edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
DecidableEq P.EdgeLabel :=
IsFinitePreFeynmanRule.edgeLabelDecidable
instance preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
DecidableEq P.VertexLabel :=
IsFinitePreFeynmanRule.vertexLabelDecidable
instance preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
DecidableEq P.HalfEdgeLabel :=
IsFinitePreFeynmanRule.halfEdgeLabelDecidable
instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : Fintype (P.vertexLabelMap v).left :=
IsFinitePreFeynmanRule.vertexMapFintype v
instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : DecidableEq (P.vertexLabelMap v).left :=
IsFinitePreFeynmanRule.vertexMapDecidable v
instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : Fintype (P.edgeLabelMap v).left :=
IsFinitePreFeynmanRule.edgeMapFintype v
instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left :=
IsFinitePreFeynmanRule.edgeMapDecidable v
instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥)
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
DecidablePred fun x => x ∈ (P.toVertex.obj F).hom ⁻¹' {v} := fun y =>
match decEq ((P.toVertex.obj F).hom y) v with
| isTrue h => isTrue h
| isFalse h => isFalse h
instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔)
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
DecidablePred fun x => x ∈ (P.toEdge.obj F).hom ⁻¹' {v} := fun y =>
match decEq ((P.toEdge.obj F).hom y) v with
| isTrue h => isTrue h
| isFalse h => isFalse h
instance preimageVertexDecidable {𝓔 𝓥 : Type} (v : 𝓥)
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq
instance preimageEdgeDecidable {𝓔 𝓥 : Type} (v : 𝓔)
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq
instance preimageVertexFintype {𝓔 𝓥 : Type} [DecidableEq 𝓥]
(v : 𝓥) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
Fintype ((P.preimageVertex v).obj F).left := @Subtype.fintype _ _ _ h
instance preimageEdgeFintype {𝓔 𝓥 : Type} [DecidableEq 𝓔]
(v : 𝓔) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
Fintype ((P.preimageEdge v).obj F).left := @Subtype.fintype _ _ _ h
instance preimageVertexMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
[DecidableEq 𝓥] (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
[Fintype F.left] :
Fintype ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left) :=
Pi.fintype
instance preimageEdgeMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
[DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
[Fintype F.left] :
Fintype ((P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left) :=
Pi.fintype
/-!
## Conditions to form a diagram.
-/
/-- The proposition on vertices which must be satisfied by an object
`F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram.
This condition corresponds to the vertices of `F` having the correct half-edges associated
with them. -/
def diagramVertexProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
(f : 𝓥 ⟶ P.VertexLabel) :=
∀ v, IsIsomorphic (P.vertexLabelMap (f v)) ((P.preimageVertex v).obj F)
/-- The proposition on edges which must be satisfied by an object
`F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram.
This condition corresponds to the edges of `F` having the correct half-edges associated
with them. -/
def diagramEdgeProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
(f : 𝓔 ⟶ P.EdgeLabel) :=
∀ v, IsIsomorphic (P.edgeLabelMap (f v)) ((P.preimageEdge v).obj F)
lemma diagramVertexProp_iff {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
(f : 𝓥 ⟶ P.VertexLabel) : P.diagramVertexProp F f ↔
∀ v, ∃ (κ : (P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left),
Function.Bijective κ
∧ ((P.preimageVertex v).obj F).hom ∘ κ = (P.vertexLabelMap (f v)).hom := by
refine Iff.intro (fun h v => ?_) (fun h v => ?_)
obtain ⟨κ, κm1, h1, h2⟩ := h v
let f := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
refine ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
obtain ⟨κ, h1, h2⟩ := h v
let f : (P.vertexLabelMap (f v)) ⟶ ((P.preimageVertex v).obj F) := Over.homMk κ h2
have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
exact ⟨f, fm, hf1, hf2⟩
lemma diagramEdgeProp_iff {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
(f : 𝓔 ⟶ P.EdgeLabel) : P.diagramEdgeProp F f ↔
∀ v, ∃ (κ : (P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left),
Function.Bijective κ
∧ ((P.preimageEdge v).obj F).hom ∘ κ = (P.edgeLabelMap (f v)).hom := by
refine Iff.intro (fun h v => ?_) (fun h v => ?_)
obtain ⟨κ, κm1, h1, h2⟩ := h v
let f := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
refine ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
obtain ⟨κ, h1, h2⟩ := h v
let f : (P.edgeLabelMap (f v)) ⟶ ((P.preimageEdge v).obj F) := Over.homMk κ h2
have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
exact ⟨f, fm, hf1, hf2⟩
instance diagramVertexPropDecidable
[IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥] [DecidableEq 𝓥]
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
(f : 𝓥 ⟶ P.VertexLabel) : Decidable (P.diagramVertexProp F f) :=
@decidable_of_decidable_of_iff _ _
(@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
(fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
(fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
(P.diagramVertexProp_iff F f).symm
instance diagramEdgePropDecidable
[IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔] [DecidableEq 𝓔]
(F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
(f : 𝓔 ⟶ P.EdgeLabel) : Decidable (P.diagramEdgeProp F f) :=
@decidable_of_decidable_of_iff _ _
(@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
(fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
(fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
(P.diagramEdgeProp_iff F f).symm
end PreFeynmanRule
/-!
## The definition of Feynman diagrams
We now define the type of Feynman diagrams for a given pre-Feynman rule.
-/
open PreFeynmanRule
/-- The type of Feynman diagrams given a `PreFeynmanRule`. -/
structure FeynmanDiagram (P : PreFeynmanRule) where
/-- The type of edges in the Feynman diagram, labelled by their type. -/
𝓔𝓞 : Over P.EdgeLabel
/-- The type of vertices in the Feynman diagram, labelled by their type. -/
𝓥𝓞 : Over P.VertexLabel
/-- The type of half-edges in the Feynman diagram, labelled by their type, the edge it
belongs to, and the vertex they belong to. -/
𝓱𝓔To𝓔𝓥 : Over (P.HalfEdgeLabel × 𝓔𝓞.left × 𝓥𝓞.left)
/-- Each edge has the correct type of half edges. -/
𝓔Cond : P.diagramEdgeProp 𝓱𝓔To𝓔𝓥 𝓔𝓞.hom
/-- Each vertex has the correct sort of half edges. -/
𝓥Cond : P.diagramVertexProp 𝓱𝓔To𝓔𝓥 𝓥𝓞.hom
namespace FeynmanDiagram
variable {P : PreFeynmanRule} (F : FeynmanDiagram P)
/-- The type of edges. -/
def 𝓔 : Type := F.𝓔𝓞.left
/-- The type of vertices. -/
def 𝓥 : Type := F.𝓥𝓞.left
/-- The type of half-edges. -/
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𝓔𝓥
/-!
## Making a Feynman diagram
-/
/-- The condition which must be satisfied by maps to form a Feynman diagram. -/
def Cond {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
(𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) : Prop :=
P.diagramEdgeProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓔𝓞 ∧
P.diagramVertexProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓥𝓞
lemma cond_self : Cond F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom :=
⟨F.𝓔Cond, F.𝓥Cond⟩
/-- `Cond` is decidable. -/
instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel)
(𝓥𝓞 : 𝓥 → P.VertexLabel)
(𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
[Fintype 𝓥] [DecidableEq 𝓥] [Fintype 𝓔] [DecidableEq 𝓔] [h : Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] :
Decidable (Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :=
@And.decidable _ _
(@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
(@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
(𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
(C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥): FeynmanDiagram P where
𝓔𝓞 := Over.mk 𝓔𝓞
𝓥𝓞 := Over.mk 𝓥𝓞
𝓱𝓔To𝓔𝓥 := Over.mk 𝓱𝓔To𝓔𝓥
𝓔Cond := C.1
𝓥Cond := C.2
lemma mk'_self : mk' F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom F.cond_self = F := rfl
/-!
## Finitness of Feynman diagrams
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`.
This finiteness condition will be used to prove certain `Types` are `Fintype`, and prove
that certain propositions are decidable.
-/
/-- A set of conditions on a Feynman diagram for it to be considered finite. -/
class IsFiniteDiagram (F : FeynmanDiagram P) where
/-- The type of edges is finite. -/
𝓔Fintype : Fintype F.𝓔
/-- The type of edges is decidable. -/
𝓔DecidableEq : DecidableEq F.𝓔
/-- The type of vertices is finite. -/
𝓥Fintype : Fintype F.𝓥
/-- The type of vertices is decidable. -/
𝓥DecidableEq : DecidableEq F.𝓥
/-- The type of half-edges is finite. -/
𝓱𝓔Fintype : Fintype F.𝓱𝓔
/-- The type of half-edges is decidable. -/
𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
IsFiniteDiagram.𝓔Fintype
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
IsFiniteDiagram.𝓔DecidableEq
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓥 :=
IsFiniteDiagram.𝓥Fintype
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
IsFiniteDiagram.𝓥DecidableEq
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
IsFiniteDiagram.𝓱𝓔Fintype
instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
IsFiniteDiagram.𝓱𝓔DecidableEq
instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
[IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
instDecidableEqProd
/-!
## Morphisms of Feynman diagrams
We define a morphism between Feynman diagrams, and properties thereof.
This will be used to define the category of Feynman diagrams.
-/
/-- Given two maps `F.𝓔 ⟶ G.𝓔` and `F.𝓥 ⟶ G.𝓥` the corresponding map
`P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥`. -/
@[simps!]
def edgeVertexMap {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥 :=
fun x => ⟨x.1, 𝓔 x.2.1, 𝓥 x.2.2⟩
/-- Given equivalences `F.𝓔 ≃ G.𝓔` and `F.𝓥 ≃ G.𝓥`, the induced equivalence between
`P.HalfEdgeLabel × F.𝓔 × F.𝓥` and `P.HalfEdgeLabel × G.𝓔 × G.𝓥 ` -/
def edgeVertexEquiv {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) :
P.HalfEdgeLabel × F.𝓔 × F.𝓥 ≃ P.HalfEdgeLabel × G.𝓔 × G.𝓥 where
toFun := edgeVertexMap 𝓔.toFun 𝓥.toFun
invFun := edgeVertexMap 𝓔.invFun 𝓥.invFun
left_inv := by aesop_cat
right_inv := by aesop_cat
/-- The functor of over-categories generated by `edgeVertexMap`. -/
@[simps!]
def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
Over.map <| edgeVertexMap 𝓔 𝓥
/-- A morphism of Feynman diagrams. -/
structure Hom (F G : FeynmanDiagram P) where
/-- The morphism of edge objects. -/
𝓔𝓞 : F.𝓔𝓞 ⟶ G.𝓔𝓞
/-- The morphism of vertex objects. -/
𝓥𝓞 : F.𝓥𝓞 ⟶ G.𝓥𝓞
/-- The morphism of half-edge objects. -/
𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
namespace Hom
variable {F G : FeynmanDiagram P}
variable (f : Hom F G)
/-- The map `F.𝓔 → G.𝓔` induced by a homomorphism of Feynman diagrams. -/
@[simp]
def 𝓔 : F.𝓔 → G.𝓔 := f.𝓔𝓞.left
/-- The map `F.𝓥 → G.𝓥` induced by a homomorphism of Feynman diagrams. -/
@[simp]
def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
/-- The map `F.𝓱𝓔 → G.𝓱𝓔` induced by a homomorphism of Feynman diagrams. -/
@[simp]
def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
/-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
@[simp]
def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
/-- The identity morphism for a Feynman diagram. -/
def id (F : FeynmanDiagram P) : Hom F F where
𝓔𝓞 := 𝟙 F.𝓔𝓞
𝓥𝓞 := 𝟙 F.𝓥𝓞
𝓱𝓔To𝓔𝓥 := 𝟙 F.𝓱𝓔To𝓔𝓥
/-- The composition of two morphisms of Feynman diagrams. -/
@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
def comp {F G H : FeynmanDiagram P} (f : Hom F G) (g : Hom G H) : Hom F H where
𝓔𝓞 := f.𝓔𝓞 ≫ g.𝓔𝓞
𝓥𝓞 := f.𝓥𝓞 ≫ g.𝓥𝓞
𝓱𝓔To𝓔𝓥 := (edgeVertexFunc g.𝓔 g.𝓥).map f.𝓱𝓔To𝓔𝓥 ≫ g.𝓱𝓔To𝓔𝓥
lemma ext' {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔𝓞 = g.𝓔𝓞)
(h𝓥 : f.𝓥𝓞 = g.𝓥𝓞) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g := by
cases f
cases g
subst h𝓔 h𝓥
simp_all only [mk.injEq, heq_eq_eq, true_and]
ext a : 2
simp only [𝓱𝓔] at h𝓱𝓔
exact congrFun h𝓱𝓔 a
lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
(h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g :=
ext' (Over.OverMorphism.ext h𝓔) (Over.OverMorphism.ext h𝓥) h𝓱𝓔
/-- The condition on maps of edges, vertices and half-edges for it to be lifted to a
morphism of Feynman diagrams. -/
def Cond {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Prop :=
(∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) ∧
(∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) ∧
(∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x))
lemma cond_satisfied {F G : FeynmanDiagram P} (f : Hom F G) :
Cond f.𝓔 f.𝓥 f.𝓱𝓔 :=
⟨fun x => congrFun f.𝓔𝓞.w x, fun x => congrFun f.𝓥𝓞.w x, fun x => congrFun f.𝓱𝓔To𝓔𝓥.w x ⟩
lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
(h : Cond 𝓔 𝓥 𝓱𝓔) : Cond 𝓔.symm 𝓥.symm 𝓱𝓔.symm := by
refine ⟨?_, ?_, ?_⟩
simpa using fun x => (h.1 (𝓔.symm x)).symm
simpa using fun x => (h.2.1 (𝓥.symm x)).symm
intro x
have h1 := h.2.2 (𝓱𝓔.symm x)
simp at h1
exact (edgeVertexEquiv 𝓔 𝓥).apply_eq_iff_eq_symm_apply.mp (h1).symm
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
(𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) :=
@Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓔 P _ _) _
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
(𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
@Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) :
Decidable (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x)) :=
@Fintype.decidableForallFintype _ _ (fun _ => fintypeProdHalfEdgeLabel𝓔𝓥 _ _) _
instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
And.decidable
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
(C : Cond 𝓔 𝓥 𝓱𝓔) : Hom F G where
𝓔𝓞 := Over.homMk 𝓔 $ funext C.1
𝓥𝓞 := Over.homMk 𝓥 $ funext C.2.1
𝓱𝓔To𝓔𝓥 := Over.homMk 𝓱𝓔 $ funext C.2.2
lemma mk'_self {F G : FeynmanDiagram P} (f : Hom F G) :
mk' f.𝓔 f.𝓥 f.𝓱𝓔 f.cond_satisfied = f := rfl
end Hom
/-!
## 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.
-/
/-- Feynman diagrams form a category. -/
@[simps! id_𝓔𝓞_left id_𝓥𝓞_left id_𝓱𝓔To𝓔𝓥_left comp_𝓔𝓞_left comp_𝓥𝓞_left comp_𝓱𝓔To𝓔𝓥_left]
instance : Category (FeynmanDiagram P) where
Hom := Hom
id := Hom.id
comp := Hom.comp
/-- An isomorphism of Feynman diagrams from isomorphisms of edges, vertices and half-edges. -/
def mkIso {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
(C : Hom.Cond 𝓔 𝓥 𝓱𝓔) : F ≅ G where
hom := Hom.mk' 𝓔 𝓥 𝓱𝓔 C
inv := Hom.mk' 𝓔.symm 𝓥.symm 𝓱𝓔.symm (Hom.cond_symm 𝓔 𝓥 𝓱𝓔 C)
hom_inv_id := by
apply Hom.ext
all_goals
aesop_cat
inv_hom_id := by
apply Hom.ext
all_goals
aesop_cat
/-- The functor from Feynman diagrams to category over edge labels. -/
def func𝓔𝓞 : FeynmanDiagram P ⥤ Over P.EdgeLabel where
obj F := F.𝓔𝓞
map f := f.𝓔𝓞
/-- The functor from Feynman diagrams to category over vertex labels. -/
def func𝓥𝓞 : FeynmanDiagram P ⥤ Over P.VertexLabel where
obj F := F.𝓥𝓞
map f := f.𝓥𝓞
/-- The functor from Feynman diagrams to category over half-edge labels. -/
def func𝓱𝓔𝓞 : FeynmanDiagram P ⥤ Over P.HalfEdgeLabel where
obj F := F.𝓱𝓔𝓞
map f := f.𝓱𝓔𝓞
/-- The functor from Feynman diagrams to `Type` landing on edges. -/
def func𝓔 : FeynmanDiagram P ⥤ Type where
obj F := F.𝓔
map f := f.𝓔
/-- The functor from Feynman diagrams to `Type` landing on vertices. -/
def func𝓥 : FeynmanDiagram P ⥤ Type where
obj F := F.𝓥
map f := f.𝓥
/-- The functor from Feynman diagrams to `Type` landing on half-edges. -/
def func𝓱𝓔 : FeynmanDiagram P ⥤ Type where
obj F := F.𝓱𝓔
map f := f.𝓱𝓔
section symmetryFactor
/-!
## Symmetry factors
The symmetry factor of a Feynman diagram is the cardinality of the group of automorphisms of that
diagram.
We show that the symmetry factor for a finite Feynman diagram is finite.
-/
/-- The type of isomorphisms of a Feynman diagram. -/
def SymmetryType : Type := F ≅ F
/-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
satisfying `Hom.Cond`. -/
def symmetryTypeEquiv :
F.SymmetryType ≃ {S : Equiv.Perm F.𝓔 × Equiv.Perm F.𝓥 × Equiv.Perm F.𝓱𝓔 //
Hom.Cond S.1 S.2.1 S.2.2} where
toFun f := ⟨⟨(func𝓔.mapIso f).toEquiv, (func𝓥.mapIso f).toEquiv,
(func𝓱𝓔.mapIso f).toEquiv⟩, f.1.cond_satisfied⟩
invFun S := mkIso S.1.1 S.1.2.1 S.1.2.2 S.2
left_inv _ := rfl
right_inv _ := rfl
instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType :=
Fintype.ofEquiv _ F.symmetryTypeEquiv.symm
/-- The symmetry factor can be defined as the cardinal of the symmetry type.
In general this is not a finite number. -/
@[simp]
def cardSymmetryFactor : Cardinal := Cardinal.mk (F.SymmetryType)
/-- The symmetry factor of a Finite Feynman diagram, as a natural number. -/
@[simp]
def symmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : ℕ :=
(Fintype.card F.SymmetryType)
@[simp]
lemma symmetryFactor_eq_cardSymmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] :
F.symmetryFactor = F.cardSymmetryFactor := by
simp only [symmetryFactor, cardSymmetryFactor, Cardinal.mk_fintype]
end symmetryFactor
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.
## TODO
- Complete this section.
-/
/-- 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.𝓥 → F.𝓥 → Prop := fun x y =>
x ≠ y ∧
∃ (a b : F.𝓱𝓔), ((F.𝓱𝓔To𝓔𝓥.hom a).2.1 = (F.𝓱𝓔To𝓔𝓥.hom b).2.1
∧ (F.𝓱𝓔To𝓔𝓥.hom a).2.2 = x ∧ (F.𝓱𝓔To𝓔𝓥.hom b).2.2 = y)
instance [IsFiniteDiagram F] : DecidableRel F.adjRelation := fun _ _ =>
@And.decidable _ _ _ $
@Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _ (
fun _ => @And.decidable _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
@And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
(instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _
/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
def toSimpleGraph : 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
use b, a
simp_all only [adjRelation, ne_eq, and_self]
loopless := by
intro x h
simp at h
instance [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
instDecidableRel𝓥AdjRelationOfIsFiniteDiagram F
instance [IsFiniteDiagram F] :
Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
@And.decidable _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
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. -/
def Connected : Prop := F.toSimpleGraph.Connected
instance [IsFiniteDiagram F] : Decidable (Connected F) :=
instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram F
end connectedness
end FeynmanDiagram

71
HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean Normal file
View file

@ -0,0 +1,71 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.FeynmanDiagrams.Basic
/-!
# Feynman diagrams in a complex scalar field theory
-/
namespace PhiFour
open CategoryTheory
open FeynmanDiagram
open PreFeynmanRule
/-- The pre-Feynman rules for a complex scalar theory. -/
@[simps!]
def complexScalarFeynmanRules : PreFeynmanRule where
/- There is 2 types of `half-edge`. -/
HalfEdgeLabel := Fin 2
/- There is only 1 type of `edge`. -/
EdgeLabel := Fin 1
/- There are two types of `vertex`, two external `0` and internal `1`. -/
VertexLabel := Fin 3
edgeLabelMap x :=
match x with
| 0 => Over.mk ![0, 1]
vertexLabelMap x :=
match x with
| 0 => Over.mk ![0]
| 1 => Over.mk ![1]
| 2 => Over.mk ![0, 0, 1, 1]
instance (a : ℕ) : OfNat complexScalarFeynmanRules.EdgeLabel a where
ofNat := (a : Fin _)
instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
ofNat := (a : Fin _)
instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
ofNat := (a : Fin _)
instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
edgeLabelDecidable := instDecidableEqFin _
vertexLabelDecidable := instDecidableEqFin _
halfEdgeLabelDecidable := instDecidableEqFin _
vertexMapFintype := fun v =>
match v with
| 0 => Fin.fintype _
| 1 => Fin.fintype _
| 2 => Fin.fintype _
edgeMapFintype := fun v =>
match v with
| 0 => Fin.fintype _
vertexMapDecidable := fun v =>
match v with
| 0 => instDecidableEqFin _
| 1 => instDecidableEqFin _
| 2 => instDecidableEqFin _
edgeMapDecidable := fun v =>
match v with
| 0 => instDecidableEqFin _
end PhiFour

70
HepLean/FeynmanDiagrams/Instances/Phi4.lean Normal file
View file

@ -0,0 +1,70 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.FeynmanDiagrams.Basic
/-!
# Feynman diagrams in Phi^4 theory
The aim of this file is to start building up the theory of Feynman diagrams in the context of
Phi^4 theory.
-/
namespace PhiFour
open CategoryTheory
open FeynmanDiagram
open PreFeynmanRule
/-- The pre-Feynman rules for `Phi^4` theory. -/
@[simps!]
def phi4PreFeynmanRules : PreFeynmanRule where
/- There is only 1 type of `half-edge`. -/
HalfEdgeLabel := Fin 1
/- There is only 1 type of `edge`. -/
EdgeLabel := Fin 1
/- There are two types of `vertex`, external `0` and internal `1`. -/
VertexLabel := Fin 2
edgeLabelMap x :=
match x with
| 0 => Over.mk ![0, 0]
vertexLabelMap x :=
match x with
| 0 => Over.mk ![0]
| 1 => Over.mk ![0, 0, 0, 0]
instance (a : ℕ) : OfNat phi4PreFeynmanRules.EdgeLabel a where
ofNat := (a : Fin _)
instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
ofNat := (a : Fin _)
instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
ofNat := (a : Fin _)
instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
edgeLabelDecidable := instDecidableEqFin _
vertexLabelDecidable := instDecidableEqFin _
halfEdgeLabelDecidable := instDecidableEqFin _
vertexMapFintype := fun v =>
match v with
| 0 => Fin.fintype _
| 1 => Fin.fintype _
edgeMapFintype := fun v =>
match v with
| 0 => Fin.fintype _
vertexMapDecidable := fun v =>
match v with
| 0 => instDecidableEqFin _
| 1 => instDecidableEqFin _
edgeMapDecidable := fun v =>
match v with
| 0 => instDecidableEqFin _
end PhiFour

583
HepLean/FeynmanDiagrams/PhiFour/Basic.lean
View file

@ -1,583 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Mathlib.Logic.Equiv.Fin
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
The aim of this file is to start building up the theory of Feynman diagrams in the context of
Phi^4 theory.
## References
- The approach taking to defining Feynman diagrams is based on:
Theo Johnson-Freyd (https://mathoverflow.net/users/78/theo-johnson-freyd), How to count symmetry
factors of Feynman diagrams? , URL (version: 2010-06-03): https://mathoverflow.net/q/26938
## TODO
- Develop a way to display 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.
-/
namespace PhiFour
open CategoryTheory
/-- Edges in Φ^4 internal `0`.
Here `Type` is the category in which half-edges live. In general `Type` will be e.g.
`Type × Type` with more fields. -/
def edgeType : Fin 1 → Type
| 0 => Fin 2
/-- Vertices in Φ^4, can either be `external` corresponding to `0`, or a `phi^4` interaction
corresponding to `1`. -/
def vertexType : Fin 2 → Type
| 0 => Fin 1
| 1 => Fin 4
/-- The type of vacuum Feynman diagrams for Phi-4 theory. -/
structure FeynmanDiagram where
/-- The type of half edges in the Feynman diagram. Sometimes also called `flags`. -/
𝓱𝓔 : Type
/-- The type of edges in the Feynman diagram. -/
𝓔 : Type
/-- Maps each edge to a label. Labels `0` if it is an external edge,
and labels `1` if an internal edge. -/
𝓔Label : 𝓔 → Fin 1
/-- Maps half-edges to edges. -/
𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔
/-- Requires that the fiber of the map `𝓱𝓔To𝓔` at `x ∈ 𝓔` agrees with the corresponding
`edgeType`. -/
𝓔Fiber : ∀ x, CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x
/-- The type of vertices in the Feynman diagram. -/
𝓥 : Type
/-- Maps each vertex to a label. In this case this map contains no information since
there is only one type of vertex.. -/
𝓥Label : 𝓥 → Fin 2
/-- Maps half-edges to vertices. -/
𝓱𝓔To𝓥 : 𝓱𝓔 → 𝓥
/-- Requires that the fiber of the map `𝓱𝓔To𝓥` at `x ∈ 𝓥` agrees with the corresponding
`vertexType`. -/
𝓥Fiber : ∀ x, CategoryTheory.IsIsomorphic (𝓱𝓔To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x
namespace FeynmanDiagram
variable (F : FeynmanDiagram)
section Decidability
/-!
## Decidability
The aim of this section is to make it easy to prove the `𝓔Fiber` and `𝓥Fiber` conditions by
showing that they are decidable in cases when everything is finite and nice
(which in practice is always).
--/
lemma fiber_cond_edge_iff_exists {𝓱𝓔 𝓔 : Type} (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
(CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x)
↔ ∃ (f : 𝓱𝓔To𝓔 ⁻¹' {x} → (edgeType ∘ 𝓔Label) x), Function.Bijective f :=
Iff.intro
(fun h ↦ match h with
| ⟨f1, f2, h1, h2⟩ => ⟨f1, (isIso_iff_bijective f1).mp ⟨f2, h1, h2⟩⟩)
(fun ⟨f1, hb⟩ ↦ match (isIso_iff_bijective f1).mpr hb with
| ⟨f2, h1, h2⟩ => ⟨f1, f2, h1, h2⟩)
lemma fiber_cond_vertex_iff_exists {𝓱𝓥 𝓥 : Type} (𝓱𝓥To𝓥 : 𝓱𝓥 → 𝓥) (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
(CategoryTheory.IsIsomorphic (𝓱𝓥To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x)
↔ ∃ (f : 𝓱𝓥To𝓥 ⁻¹' {x} → (vertexType ∘ 𝓥Label) x), Function.Bijective f :=
Iff.intro
(fun h ↦ match h with
| ⟨f1, f2, h1, h2⟩ => ⟨f1, (isIso_iff_bijective f1).mp ⟨f2, h1, h2⟩⟩)
(fun ⟨f1, hb⟩ ↦ match (isIso_iff_bijective f1).mpr hb with
| ⟨f2, h1, h2⟩ => ⟨f1, f2, h1, h2⟩)
instance {𝓱𝓔 𝓔 : Type} [DecidableEq 𝓔] (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (x : 𝓔):
DecidablePred (fun y => y ∈ 𝓱𝓔To𝓔 ⁻¹' {x}) := fun y =>
match decEq (𝓱𝓔To𝓔 y) x with
| isTrue h => isTrue h
| isFalse h => isFalse h
instance {𝓱𝓔 𝓔 : Type} [DecidableEq 𝓱𝓔] (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (x : 𝓔) :
DecidableEq $ (𝓱𝓔To𝓔 ⁻¹' {x}) := Subtype.instDecidableEq
instance edgeTypeFintype (x : Fin 1) : Fintype (edgeType x) :=
match x with
| 0 => Fin.fintype 2
instance edgeTypeDecidableEq (x : Fin 1) : DecidableEq (edgeType x) :=
match x with
| 0 => instDecidableEqFin 2
instance vertexTypeFintype (x : Fin 2) : Fintype (vertexType x) :=
match x with
| 0 => Fin.fintype 1
| 1 => Fin.fintype 4
instance vertexTypeDecidableEq (x : Fin 2) : DecidableEq (vertexType x) :=
match x with
| 0 => instDecidableEqFin 1
| 1 => instDecidableEqFin 4
instance {𝓔 : Type} (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
DecidableEq ((edgeType ∘ 𝓔Label) x) := edgeTypeDecidableEq (𝓔Label x)
instance {𝓔 : Type} (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
Fintype ((edgeType ∘ 𝓔Label) x) := edgeTypeFintype (𝓔Label x)
instance {𝓥 : Type} (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
DecidableEq ((vertexType ∘ 𝓥Label) x) := vertexTypeDecidableEq (𝓥Label x)
instance {𝓥 : Type} (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
Fintype ((vertexType ∘ 𝓥Label) x) := vertexTypeFintype (𝓥Label x)
instance {𝓱𝓔 𝓔 : Type} [Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] [DecidableEq 𝓔]
(𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
Decidable (CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x) :=
decidable_of_decidable_of_iff (fiber_cond_edge_iff_exists 𝓱𝓔To𝓔 𝓔Label x).symm
instance {𝓱𝓥 𝓥 : Type} [Fintype 𝓱𝓥] [DecidableEq 𝓱𝓥] [DecidableEq 𝓥]
(𝓱𝓥To𝓥 : 𝓱𝓥 → 𝓥) (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
Decidable (CategoryTheory.IsIsomorphic (𝓱𝓥To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x) :=
decidable_of_decidable_of_iff (fiber_cond_vertex_iff_exists 𝓱𝓥To𝓥 𝓥Label x).symm
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
/-!
## 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
- - - - - -
-/
def propagator : FeynmanDiagram where
𝓱𝓔 := Fin 2
𝓔 := Fin 1
𝓔Label := ![0]
𝓱𝓔To𝓔 := ![0, 0]
𝓔Fiber := by decide
𝓥 := Fin 2
𝓥Label := ![0, 0]
𝓱𝓔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
_
/ \
/ \
\ /
\ /
\ /
/ \
/ \
\ /
\ __ / -/
@[simps!]
def figureEight : FeynmanDiagram where
𝓱𝓔 := Fin 4
𝓔 := Fin 2
𝓔Label := ![0, 0]
𝓱𝓔To𝓔 := ![0, 0, 1, 1]
𝓔Fiber := by decide
𝓥 := Fin 1
𝓥Label := ![1]
𝓱𝓔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 diagram1 : FeynmanDiagram where
𝓱𝓔 := Fin 10
𝓔 := Fin 5
𝓔Label := ![0, 0, 0, 0, 0]
𝓱𝓔To𝓔 := ![0, 0, 1, 1, 2, 2, 3, 3, 4, 4]
𝓔Fiber := by decide
𝓥 := Fin 4
𝓥Label := ![0, 1, 1, 0]
𝓱𝓔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
end FeynmanDiagram
end PhiFour