Feynman diagrams in a complex scalar field theory #
@[simp]
theorem
PhiFour.complexScalarFeynmanRules_VertexLabel :
PhiFour.complexScalarFeynmanRules.VertexLabel = Fin 3
@[simp]
theorem
PhiFour.complexScalarFeynmanRules_vertexLabelMap
(x : Fin 3)
:
PhiFour.complexScalarFeynmanRules.vertexLabelMap x = match x with
| 0 => CategoryTheory.Over.mk ![0]
| 1 => CategoryTheory.Over.mk ![1]
| 2 => CategoryTheory.Over.mk ![0, 0, 1, 1]
@[simp]
theorem
PhiFour.complexScalarFeynmanRules_EdgeLabel :
PhiFour.complexScalarFeynmanRules.EdgeLabel = Fin 1
@[simp]
theorem
PhiFour.complexScalarFeynmanRules_edgeLabelMap
(x : Fin 1)
:
PhiFour.complexScalarFeynmanRules.edgeLabelMap x = match x with
| 0 => CategoryTheory.Over.mk ![0, 1]
@[simp]
theorem
PhiFour.complexScalarFeynmanRules_HalfEdgeLabel :
PhiFour.complexScalarFeynmanRules.HalfEdgeLabel = Fin 2
The pre-Feynman rules for a complex scalar theory.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
PhiFour.instOfNatEdgeLabelComplexScalarFeynmanRules
(a : ℕ)
:
OfNat PhiFour.complexScalarFeynmanRules.EdgeLabel a
Equations
- PhiFour.instOfNatEdgeLabelComplexScalarFeynmanRules a = { ofNat := ↑a }
instance
PhiFour.instOfNatHalfEdgeLabelComplexScalarFeynmanRules
(a : ℕ)
:
OfNat PhiFour.complexScalarFeynmanRules.HalfEdgeLabel a
Equations
- PhiFour.instOfNatHalfEdgeLabelComplexScalarFeynmanRules a = { ofNat := ↑a }
instance
PhiFour.instOfNatVertexLabelComplexScalarFeynmanRules
(a : ℕ)
:
OfNat PhiFour.complexScalarFeynmanRules.VertexLabel a
Equations
- PhiFour.instOfNatVertexLabelComplexScalarFeynmanRules a = { ofNat := ↑a }
instance
PhiFour.instIsFinitePreFeynmanRuleComplexScalarFeynmanRules :
PhiFour.complexScalarFeynmanRules.IsFinitePreFeynmanRule
Equations
- One or more equations did not get rendered due to their size.