docs: Add some docs and create file

This commit is contained in:
jstoobysmith 2024-11-25 05:41:46 +00:00
parent dc12a3ead3
commit d8b6aa0cbb
3 changed files with 26 additions and 0 deletions

View file

@ -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

View file

@ -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. -/