Merge pull request #245 from HEPLean/FeynmanDiagrams

docs: Add some docs and create file

HepLean.lean

@@ -56,6 +56,7 @@ import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
 import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FeynmanDiagrams.Wick.Contract
+import HepLean.FeynmanDiagrams.Wick.Ring
 import HepLean.FeynmanDiagrams.Wick.String
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants

HepLean/FeynmanDiagrams/Wick/Ring.lean

@@ -0,0 +1,24 @@
+/-
+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.FeynmanDiagrams.Basic
+/-!
+# Operator ring
+
+Currently this file is only for an example of Wick strings, correpsonding to a
+theory with two complex scalar fields. The concepts will however generalize.
+
+This file is currently a stub.
+
+We will formally define the operator ring, in terms of the fields present in the theory.
+
+-/
+
+namespace TwoComplexScalar
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+end TwoComplexScalar

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -94,6 +94,7 @@ inductive WickStringLast where
 
 open WickStringLast
 
+/-! TODO: This definition should be adapted to include the in and out going fields as inputs. -/
 /-- A wick string is a representation of a string of fields from a theory.
   E.g. `φ(x1) φ(x2) φ(y) φ(y) φ(y) φ(x3)`. The use of vertices in the Wick string
   allows us to identify which fields have the same space-time coordinate. -/