From c81d6ce2469e29dded111aea78b931a65ab1336b Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 6 Feb 2025 13:06:51 +0000
Subject: [PATCH] docs: Docs for FieldOpAlgebra

---
 .../FieldOpAlgebra/Basic.lean                 | 37 +++++++++++++++----
 .../FieldOpAlgebra/Grading.lean               |  5 ++-
 .../FieldOpAlgebra/SuperCommute.lean          | 11 +++++-
 .../FieldOpFreeAlgebra/Grading.lean           |  7 ++--
 scripts/MetaPrograms/notes.lean               | 25 +++++++------
 5 files changed, 60 insertions(+), 25 deletions(-)

diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
index 193e226..7f36022 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
@@ -67,7 +67,11 @@ lemma equiv_iff_exists_add (x y : FieldOpFreeAlgebra 𝓕) :
     rw [equiv_iff_sub_mem_ideal]
     simp [ha]
 
-/-- The projection of `FieldOpFreeAlgebra` down to `FieldOpAlgebra` as an algebra map. -/
+/-- For a field specification `𝓕`, the projection
+
+`𝓕.FieldOpFreeAlgebra →ₐ[ℂ] FieldOpAlgebra 𝓕`
+
+taking each element of `𝓕.FieldOpFreeAlgebra` to its equivalence class in `FieldOpAlgebra 𝓕`. -/
 def ι : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.mk'
   map_one' := by rfl
@@ -453,12 +457,14 @@ lemma ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero (x : FieldOpFreeAlgebra 
 
 -/
 
-/-- An element of `FieldOpAlgebra` from a `FieldOp`. -/
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.FieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpF φ)`. -/
 def ofFieldOp (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpF φ)
 
 lemma ofFieldOp_eq_ι_ofFieldOpF (φ : 𝓕.FieldOp) : ofFieldOp φ = ι (ofFieldOpF φ) := rfl
 
-/-- An element of `FieldOpAlgebra` from a list of `FieldOp`. -/
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.FieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpListF φ)`. -/
 def ofFieldOpList (φs : List 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpListF φs)
 
 lemma ofFieldOpList_eq_ι_ofFieldOpListF (φs : List 𝓕.FieldOp) :
@@ -481,7 +487,8 @@ lemma ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     ofFieldOpList [φ] = ofFieldOp φ := by
   simp only [ofFieldOpList, ofFieldOp, ofFieldOpListF_singleton]
 
-/-- An element of `FieldOpAlgebra` from a `CrAnFieldOp`. -/
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.CrAnFieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofCrAnOpF φ)`. -/
 def ofCrAnOp (φ : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnOpF φ)
 
 lemma ofCrAnOp_eq_ι_ofCrAnOpF (φ : 𝓕.CrAnFieldOp) :
@@ -493,7 +500,8 @@ lemma ofFieldOp_eq_sum (φ : 𝓕.FieldOp) :
   simp only [map_sum]
   rfl
 
-/-- An element of `FieldOpAlgebra` from a list of `CrAnFieldOp`. -/
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.CrAnFieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofCrAnListF φ)`. -/
 def ofCrAnList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
 
 lemma ofCrAnList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
@@ -515,7 +523,13 @@ lemma ofFieldOpList_eq_sum (φs : List 𝓕.FieldOp) :
   simp only [map_sum]
   rfl
 
-/-- The annihilation part of a state. -/
+remark notation_drop := "In doc-strings we will often drop explicit applications of `ofCrAnOp`,
+`ofCrAnList`, `ofFieldOp`, and `ofFieldOpList`"
+
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, the
+  annihilation part of `𝓕.FieldOp` as an element of `𝓕.FieldOpAlgebra`.
+  If `φ` is an incoming asymptotic state this is zero by definition, otherwise
+  it is of the form `ofCrAnOp _`. -/
 def anPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (anPartF φ)
 
 lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl
@@ -536,7 +550,10 @@ lemma anPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPart, ofCrAnOp]
 
-/-- The creation part of a state. -/
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, the
+  creation part of `𝓕.FieldOp` as an element of `𝓕.FieldOpAlgebra`.
+  If `φ` is an outgoing asymptotic state this is zero by definition, otherwise
+  it is of the form `ofCrAnOp _`. -/
 def crPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (crPartF φ)
 
 lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl
@@ -557,6 +574,12 @@ lemma crPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPart (FieldOp.outAsymp φ) = 0 := by
   simp [crPart]
 
+/-- For field specification `𝓕`, and an element `φ` of `𝓕.FieldOp` the following relation holds:
+
+`ofFieldOp φ = crPart φ + anPart φ`
+
+That is, every field operator splits into its creation part plus its annihilation part.
+-/
 lemma ofFieldOp_eq_crPart_add_anPart (φ : 𝓕.FieldOp) :
     ofFieldOp φ = crPart φ + anPart φ := by
   rw [ofFieldOp, crPart, anPart, ofFieldOpF_eq_crPartF_add_anPartF]
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
index 30ecc74..44d581c 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
@@ -384,8 +384,9 @@ lemma directSum_eq_bosonic_plus_fermionic
     abel
 
 /-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpAlgebra` is graded by `FieldStatistic`.
-  Those `ofCrAnList φs` for which `φs` has `bosonic` statistics span one part of the grading,
-  whilst those where `φs` has `fermionic` statistics span the other part of the grading. -/
+  Those `ofCrAnList φs` for which `φs` has an overall `bosonic` statistic span `bosonic`
+  submodule, whilst those `ofCrAnList φs` for which `φs` has an overall `fermionic` statistic span
+  the `fermionic` submodule. -/
 instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubmodule where
   one_mem := by
     simp only [statSubmodule]
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
index a28dae5..f37ea26 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
@@ -88,7 +88,16 @@ lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 
   simp only [add_sub_cancel]
   simp
 
-/-- The super commutor on the `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `superCommute` is the linear map
+  `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+  defined as the decent of `ι ∘ superCommuteF` in both arguments.
+  In particular for `φs` and `φs'` lists of `𝓕.CrAnFieldOp` in `FieldOpAlgebra 𝓕` the following
+  relation holds:
+
+  `superCommute φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs`
+
+  The notation `[a, b]ₛ` is used for `superCommute a b`.
+  -/
 noncomputable def superCommute : FieldOpAlgebra 𝓕 →ₗ[ℂ]
     FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift superCommuteRight superCommuteRight_eq_of_equiv
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
index 19e18f1..3c3bb4c 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
@@ -236,9 +236,10 @@ lemma directSum_eq_bosonic_plus_fermionic
     conv_lhs => rw [hx, hy]
     abel
 
-/-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is graded by `FieldStatistic`.
-  Those `ofCrAnListF φs` for which `φs` has `bosonic` statistics span one part  of the grading,
-  whilst those where `φs` has `fermionic` statistics span the other part of the grading. -/
+/-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is graded by `FieldStatistic`.
+  Those `ofCrAnListF φs` for which `φs` has an overall `bosonic` statistic span `bosonic`
+  submodule, whilst those `ofCrAnListF φs` for which `φs` has an overall `fermionic` statistic span
+  the `fermionic` submodule. -/
 instance fieldOpFreeAlgebraGrade :
     GradedAlgebra (A := 𝓕.FieldOpFreeAlgebra) statisticSubmodule where
   one_mem := by
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index 11fe440..b87f0bb 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -165,18 +165,19 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF .complete,
     .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum .complete,
     .h2 "Field-operator algebra",
-    .name ``FieldSpecification.FieldOpAlgebra .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ι .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.universality .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.anPart .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.crPart .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_eq_crPart_add_anPart .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.superCommute .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ι .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.universality .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .complete,
+    .name `FieldSpecification.FieldOpAlgebra.notation_drop .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.anPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.crPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_eq_crPart_add_anPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.superCommute .complete,
     .h1 "Time ordering",
     .name ``FieldSpecification.crAnTimeOrderRel .incomplete,
     .name ``FieldSpecification.crAnTimeOrderSign .incomplete,