Merge pull request #262 from HEPLean/NotesEdit
feat: Update to note constructors
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
f71180f641
4 changed files with 64 additions and 14 deletions
|
|
@ -126,6 +126,22 @@ def codeButton : String := "
|
|||
</style>
|
||||
"
|
||||
|
||||
/-- HTML allowing the use of mathjax. -/
|
||||
def mathJaxScript : String := "
|
||||
<!-- MathJax code -->
|
||||
<script type=\"text/javascript\">
|
||||
window.MathJax = {
|
||||
tex: {
|
||||
inlineMath: [['$', '$']], // Use $...$ for inline math
|
||||
displayMath: [['$$', '$$']] // Use $$...$$ for block math
|
||||
}
|
||||
};
|
||||
</script>
|
||||
<script type=\"text/javascript\" id=\"MathJax-script\" async
|
||||
src=\"https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js\">
|
||||
</script>
|
||||
"
|
||||
|
||||
/-- The header to the html code. -/
|
||||
def headerHTML : String :=
|
||||
"---
|
||||
|
|
@ -133,7 +149,7 @@ layout: default
|
|||
---
|
||||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>" ++ codeBlockHTML ++ informalDefStyle ++ codeButton ++ "</head>
|
||||
<head>" ++ codeBlockHTML ++ mathJaxScript ++ informalDefStyle ++ codeButton ++ "</head>
|
||||
</head>
|
||||
<body>"
|
||||
|
||||
|
|
@ -147,11 +163,11 @@ def titleHTML : String :=
|
|||
def leanNote : String := "
|
||||
<br>
|
||||
<div style=\"border: 1px solid black; padding: 10px;\">
|
||||
<p>Note: These are are not ordinary notes. They are created using an interactive theorem
|
||||
<p>Note: These are not ordinary notes. They are created using an interactive theorem
|
||||
prover called <a href=\"https://lean-lang.org\">Lean</a>.
|
||||
Lean formally checks definitions, theorems and proofs for correctness.
|
||||
These notes are part of a much larger project called
|
||||
<a href=\"https://github.com/HEPLean/HepLean\">HepLean</a>., which aims to digitalize
|
||||
<a href=\"https://github.com/HEPLean/HepLean\">HepLean</a>, which aims to digitalize
|
||||
high energy physics into Lean. Please consider contributing to this project.
|
||||
<br><br>
|
||||
Please provide feedback or suggestions for improvements by creating a GitHub issue
|
||||
|
|
|
|||
|
|
@ -24,12 +24,42 @@ We will formally define the operator ring, in terms of the fields present in the
|
|||
- Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
|
||||
-/
|
||||
|
||||
note "
|
||||
<h1>Operator algebra</h1>
|
||||
This is a test note."
|
||||
|
||||
namespace Wick
|
||||
|
||||
note r"
|
||||
<h2>Operator algebra</h2>
|
||||
Given a Wick Species $S$, we can define the operator algebra of that theory.
|
||||
The operator algebra is a super-algebra over the complex numbers, which acts on
|
||||
the Hilbert space of the theory. A super-algebra is an algebra with a $\mathbb{Z}/2$ grading.
|
||||
To do pertubation theory in a QFT we need a need some basic properties of the operator algebra,
|
||||
$A$.
|
||||
<br><br>
|
||||
For every field $f ∈ \mathcal{f}$, we have a number of families of operators. For every
|
||||
space-time point $x ∈ \mathbb{R}^4$, we have the operators $ψ(f, x)$ which we decomponse into
|
||||
a creation and destruction part, $ψ_c(f, x)$ and $ψ_d(f, x)$ respectively. Thus
|
||||
$ψ(f, x) = ψ_c(f, x) + ψ_d(f, x)$.
|
||||
For each momentum $p$ we also have the asymptotic states $φ_c(f, p)$ and $φ_d(f, p)$.
|
||||
<br><br>
|
||||
If the field $f$ corresponds to a fermion, then all of these operators are homogeneous elements
|
||||
in the non-identity part of $A$. Conversely, if the field $f$ corresponds to a boson, then all
|
||||
of these operators are homogeneous elements in the module of $A$ corresponding to
|
||||
$0 ∈ \mathbb{Z}/2$.
|
||||
<br><br>
|
||||
The super-commutator of any of the operators above is in the center of the algebra. Moreover,
|
||||
the following super-commutators are zero:
|
||||
<ul>
|
||||
<li>$[ψ_c(f, x), ψ_c(g, y)] = 0$</li>
|
||||
<li>$[ψ_d(f, x), ψ_d(g, y)] = 0$</li>
|
||||
<li>$[φ_c(f, p), φ_c(g, q)] = 0$</li>
|
||||
<li>$[φ_d(f, p), φ_d(g, q)] = 0$</li>
|
||||
<li>$[φ_c(f, p), φ_d(g, q)] = 0$ for $f \neq \xi g$</li>
|
||||
<li>$[φ_d(f, p), ψ_c(g, y)] = 0$ for $f \neq \xi g$</li>
|
||||
<li>$[φ_c(f, p), ψ_d(g, y)] = 0$ for $f \neq \xi g$</li>
|
||||
</ul>
|
||||
<br>
|
||||
This basic structure constitutes what we call a Wick Algebra:
|
||||
"
|
||||
|
||||
informal_definition_note WickAlgebra where
|
||||
math :≈ "
|
||||
Modifications of this may be needed.
|
||||
|
|
@ -45,8 +75,8 @@ informal_definition_note WickAlgebra where
|
|||
- The super-commutator of two fields is always in the
|
||||
center of the algebra.
|
||||
Asympotic states:
|
||||
- `φc : S.𝓯 × SpaceTime → A`. The creation asympotic state (incoming).
|
||||
- `φd : S.𝓯 × SpaceTime → A`. The destruction asympotic state (outgoing).
|
||||
- `φc : S.𝓯 × MomentumSpace → A`. The creation asympotic state (incoming).
|
||||
- `φd : S.𝓯 × MomentumSpace → A`. The destruction asympotic state (outgoing).
|
||||
Subject to the conditions:
|
||||
...
|
||||
"
|
||||
|
|
@ -55,7 +85,7 @@ informal_definition_note WickAlgebra where
|
|||
ref :≈ "https://physics.stackexchange.com/questions/24157/"
|
||||
deps :≈ [``SuperAlgebra, ``SuperAlgebra.superCommuator]
|
||||
|
||||
informal_definition_note WickMonomial where
|
||||
informal_definition WickMonomial where
|
||||
math :≈ "The type of elements of the Wick algebra which is a product of fields."
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
|
|
@ -66,7 +96,11 @@ informal_definition toWickAlgebra where
|
|||
returns the product of the fields in the monomial."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
|
||||
informal_definition timeOrder where
|
||||
note r"
|
||||
<h2>Order</h2>
|
||||
"
|
||||
|
||||
informal_definition_note timeOrder where
|
||||
math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
|
||||
returns the monomial with the fields time ordered, with the correct sign
|
||||
determined by the Koszul sign factor.
|
||||
|
|
@ -81,7 +115,7 @@ informal_definition timeOrder where
|
|||
"
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
|
||||
informal_definition normalOrder where
|
||||
informal_definition_note normalOrder where
|
||||
math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
|
||||
returns the element in `WickAlgebra` defined as follows
|
||||
- The ψd fields are move to the right.
|
||||
|
|
|
|||
|
|
@ -41,7 +41,6 @@ inductive WickContract : {ni : ℕ} → {i : Fin ni → S.𝓯} → {n : ℕ}
|
|||
namespace WickContract
|
||||
|
||||
/-- The number of nodes of a Wick contraction. -/
|
||||
@[note_attr]
|
||||
def size {ni : ℕ} {i : Fin ni → S.𝓯} {n : ℕ} {c : Fin n → S.𝓯}
|
||||
{no : ℕ} {o : Fin no → S.𝓯} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
|
||||
WickContract str b1 b2 → ℕ := fun
|
||||
|
|
|
|||
|
|
@ -29,7 +29,8 @@ The first bit of data we need is a type of fields `𝓯`. We also need to know w
|
|||
are dual to what other fields, for example in a complex scalar theory `φ` is dual to `φ†`.
|
||||
We can encode this information in an involution `ξ : 𝓯 → 𝓯`.
|
||||
<br><br>
|
||||
...
|
||||
The second bit of data we need is how the fields interact with each other. In other words,
|
||||
a list of interaction vertices `𝓘`, and the type of fields associated to each vertex.
|
||||
<br><br>
|
||||
This necessary information to do perturbation theory is encoded in a `Wick Species`, which
|
||||
we define as:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue