Merge pull request #334 from HEPLean/NotesFix

docs: More doc updates for Wick's theorem

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -24,24 +24,24 @@ variable (𝓕 : FieldSpecification)
 def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
   { x |
     (∃ (φ1 φ2 φ3 : 𝓕.CrAnFieldOp),
-        x = [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca)
+        x = [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF)
     ∨ (∃ (φc φc' : 𝓕.CrAnFieldOp) (_ : 𝓕 |>ᶜ φc = .create) (_ : 𝓕 |>ᶜ φc' = .create),
-      x = [ofCrAnOpF φc, ofCrAnOpF φc']ₛca)
+      x = [ofCrAnOpF φc, ofCrAnOpF φc']ₛF)
     ∨ (∃ (φa φa' : 𝓕.CrAnFieldOp) (_ : 𝓕 |>ᶜ φa = .annihilate) (_ : 𝓕 |>ᶜ φa' = .annihilate),
-      x = [ofCrAnOpF φa, ofCrAnOpF φa']ₛca)
+      x = [ofCrAnOpF φa, ofCrAnOpF φa']ₛF)
     ∨ (∃ (φ φ' : 𝓕.CrAnFieldOp) (_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')),
-      x = [ofCrAnOpF φ, ofCrAnOpF φ']ₛca)}
+      x = [ofCrAnOpF φ, ofCrAnOpF φ']ₛF)}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpAlgebra` is defined as the quotient
   of the free algebra `𝓕.FieldOpFreeAlgebra` by the ideal generated by
-- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛca` for `φc` and `φc'` field creation operators.
+- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛF` for `φc` and `φc'` field creation operators.
   This corresponds to the condition that two creation operators always super-commute.
-- `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` field annihilation operators.
+- `[ofCrAnOpF φa, ofCrAnOpF φa']ₛF` for `φa` and `φa'` field annihilation operators.
   This corresponds to the condition that two annihilation operators always super-commute.
-- `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` operators with different statistics.
+- `[ofCrAnOpF φ, ofCrAnOpF φ']ₛF` for `φ` and `φ'` operators with different statistics.
   This corresponds to the condition that two operators with different statistics always
   super-commute. In other words, fermions and bosons always super-commute.
-- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`. This corresponds to the condition,
+- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF`. This corresponds to the condition,
   when combined with the conditions above, that the super-commutator is in the center
   of the algebra.
 -/
@@ -70,7 +70,7 @@ lemma equiv_iff_exists_add (x y : FieldOpFreeAlgebra 𝓕) :
     rw [equiv_iff_sub_mem_ideal]
     simp [ha]
 
-/-- For a field specification `𝓕`, the projection
+/-- For a field specification `𝓕`, `ι` is defined as the projection
 
 `𝓕.FieldOpFreeAlgebra →ₐ[ℂ] FieldOpAlgebra 𝓕`
 
@@ -100,7 +100,7 @@ lemma ι_of_mem_fieldOpIdealSet (x : FieldOpFreeAlgebra 𝓕) (hx : x ∈ 𝓕.f
   simpa using hx
 
 lemma ι_superCommuteF_of_create_create (φc φc' : 𝓕.CrAnFieldOp) (hφc : 𝓕 |>ᶜ φc = .create)
-    (hφc' : 𝓕 |>ᶜ φc' = .create) : ι [ofCrAnOpF φc, ofCrAnOpF φc']ₛca = 0 := by
+    (hφc' : 𝓕 |>ᶜ φc' = .create) : ι [ofCrAnOpF φc, ofCrAnOpF φc']ₛF = 0 := by
   apply ι_of_mem_fieldOpIdealSet
   simp only [fieldOpIdealSet, exists_and_left, Set.mem_setOf_eq]
   simp only [exists_prop]
@@ -110,7 +110,7 @@ lemma ι_superCommuteF_of_create_create (φc φc' : 𝓕.CrAnFieldOp) (hφc : 
 
 lemma ι_superCommuteF_of_annihilate_annihilate (φa φa' : 𝓕.CrAnFieldOp)
     (hφa : 𝓕 |>ᶜ φa = .annihilate) (hφa' : 𝓕 |>ᶜ φa' = .annihilate) :
-    ι [ofCrAnOpF φa, ofCrAnOpF φa']ₛca = 0 := by
+    ι [ofCrAnOpF φa, ofCrAnOpF φa']ₛF = 0 := by
   apply ι_of_mem_fieldOpIdealSet
   simp only [fieldOpIdealSet, exists_and_left, Set.mem_setOf_eq]
   simp only [exists_prop]
@@ -120,7 +120,7 @@ lemma ι_superCommuteF_of_annihilate_annihilate (φa φa' : 𝓕.CrAnFieldOp)
   use φa, φa', hφa, hφa'
 
 lemma ι_superCommuteF_of_diff_statistic {φ ψ : 𝓕.CrAnFieldOp}
-    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca = 0 := by
+    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF = 0 := by
   apply ι_of_mem_fieldOpIdealSet
   simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq]
   right
@@ -129,8 +129,8 @@ lemma ι_superCommuteF_of_diff_statistic {φ ψ : 𝓕.CrAnFieldOp}
   use φ, ψ
 
 lemma ι_superCommuteF_zero_of_fermionic (φ ψ : 𝓕.CrAnFieldOp)
-    (h : [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca ∈ statisticSubmodule fermionic) :
-    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca = 0 := by
+    (h : [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF ∈ statisticSubmodule fermionic) :
+    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF = 0 := by
   rw [← ofCrAnListF_singleton, ← ofCrAnListF_singleton] at h ⊢
   rcases statistic_neq_of_superCommuteF_fermionic h with h | h
   · simp only [ofCrAnListF_singleton]
@@ -139,8 +139,8 @@ lemma ι_superCommuteF_zero_of_fermionic (φ ψ : 𝓕.CrAnFieldOp)
   · simp [h]
 
 lemma ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero (φ ψ : 𝓕.CrAnFieldOp) :
-    [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca ∈ statisticSubmodule bosonic ∨
-    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca = 0 := by
+    [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF ∈ statisticSubmodule bosonic ∨
+    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF = 0 := by
   rcases superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic [φ] [ψ] with h | h
   · simp_all [ofCrAnListF_singleton]
   · simp_all only [ofCrAnListF_singleton]
@@ -155,14 +155,14 @@ lemma ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero (φ ψ : 𝓕.CrAnFie
 
 @[simp]
 lemma ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) :
-    ι [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca = 0 := by
+    ι [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF = 0 := by
   apply ι_of_mem_fieldOpIdealSet
   simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq]
   left
   use φ1, φ2, φ3
 
 lemma ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnOpF (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) :
-    ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca, ofCrAnOpF φ3]ₛca = 0 := by
+    ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF, ofCrAnOpF φ3]ₛF = 0 := by
   rw [← ofCrAnListF_singleton, ← ofCrAnListF_singleton, ← ofCrAnListF_singleton]
   rcases superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic [φ1] [φ2] with h | h
   · rw [bonsonic_superCommuteF_symm h]
@@ -175,7 +175,7 @@ lemma ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnOpF (φ1 φ2 φ3
 
 lemma ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF (φ1 φ2 : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) :
-    ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca, ofCrAnListF φs]ₛca = 0 := by
+    ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF, ofCrAnListF φs]ₛF = 0 := by
   rw [← ofCrAnListF_singleton, ← ofCrAnListF_singleton]
   rcases superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic [φ1] [φ2] with h | h
   · rw [superCommuteF_bosonic_ofCrAnListF_eq_sum _ _ h]
@@ -185,27 +185,27 @@ lemma ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF (φ1 φ2 :
 
 @[simp]
 lemma ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra (φ1 φ2 : 𝓕.CrAnFieldOp)
-    (a : 𝓕.FieldOpFreeAlgebra) : ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca, a]ₛca = 0 := by
-  change (ι.toLinearMap ∘ₗ superCommuteF [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca) a = _
-  have h1 : (ι.toLinearMap ∘ₗ superCommuteF [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca) = 0 := by
+    (a : 𝓕.FieldOpFreeAlgebra) : ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF, a]ₛF = 0 := by
+  change (ι.toLinearMap ∘ₗ superCommuteF [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF) a = _
+  have h1 : (ι.toLinearMap ∘ₗ superCommuteF [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF) = 0 := by
     apply (ofCrAnListFBasis.ext fun l ↦ ?_)
     simp [ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF]
   rw [h1]
   simp
 
 lemma ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF (φ1 φ2 : 𝓕.CrAnFieldOp)
-    (a : 𝓕.FieldOpFreeAlgebra) : ι a * ι [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca -
-    ι [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca * ι a = 0 := by
+    (a : 𝓕.FieldOpFreeAlgebra) : ι a * ι [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF -
+    ι [ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF * ι a = 0 := by
   rcases ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero φ1 φ2 with h | h
   swap
   · simp [h]
-  trans - ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛca, a]ₛca
+  trans - ι [[ofCrAnOpF φ1, ofCrAnOpF φ2]ₛF, a]ₛF
   · rw [bosonic_superCommuteF h]
     simp
   · simp
 
 lemma ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center (φ ψ : 𝓕.CrAnFieldOp) :
-    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛca ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
+    ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
   rw [Subalgebra.mem_center_iff]
   intro a
   obtain ⟨a, rfl⟩ := ι_surjective a

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean

@@ -32,7 +32,7 @@ is zero.
 
 lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero
     (φa φa' : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) :
-    ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * ofCrAnListF φs') = 0 := by
+    ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛF * ofCrAnListF φs') = 0 := by
   rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa) with hφa | hφa
   <;> rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa') with hφa' | hφa'
   · rw [normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF φa φa' hφa hφa' φs φs']
@@ -53,27 +53,27 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero
 lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero
     (φa φa' : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp)
     (a : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * a) = 0 := by
+    ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛF * a) = 0 := by
   have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
-      mulLinearMap (ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca) = 0 := by
+      mulLinearMap (ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛF) = 0 := by
     apply ofCrAnListFBasis.ext
     intro l
     simp only [FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
       AlgHom.toLinearMap_apply, LinearMap.zero_apply]
     exact ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero φa φa' φs l
   change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
-    mulLinearMap ((ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca))) a = 0
+    mulLinearMap ((ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛF))) a = 0
   rw [hf]
   simp
 
 lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul (φa φa' : 𝓕.CrAnFieldOp)
     (a b : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnOpF φa']ₛF * b) = 0 := by
   rw [mul_assoc]
   change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
-    ([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b)) a = 0
+    ([ofCrAnOpF φa, ofCrAnOpF φa']ₛF * b)) a = 0
   have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
-      ([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
+      ([ofCrAnOpF φa, ofCrAnOpF φa']ₛF * b) = 0 := by
     apply ofCrAnListFBasis.ext
     intro l
     simp only [mulLinearMap, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp,
@@ -86,7 +86,7 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul (φa φa' : 𝓕.CrAnF
 
 lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnListF φs]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnListF φs]ₛF * b) = 0 := by
   rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum]
   rw [Finset.mul_sum, Finset.sum_mul]
   rw [map_sum, map_sum]
@@ -98,7 +98,7 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul (φa : 
 
 lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnOpF φa]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnOpF φa]ₛF * b) = 0 := by
   rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_symm, ofCrAnListF_singleton]
   simp only [FieldStatistic.instCommGroup.eq_1, FieldStatistic.ofList_singleton, mul_neg,
     Algebra.mul_smul_comm, neg_mul, Algebra.smul_mul_assoc, map_neg, map_smul]
@@ -107,7 +107,7 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul (φa : 
 
 lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul
     (φs φs' : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnListF φs']ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnListF φs']ₛF * b) = 0 := by
   rw [superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, Finset.mul_sum, Finset.sum_mul]
   rw [map_sum, map_sum]
   apply Fintype.sum_eq_zero
@@ -119,7 +119,7 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul
 lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul
     (φs : List 𝓕.CrAnFieldOp)
     (a b c : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [ofCrAnListF φs, c]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnListF φs, c]ₛF * b) = 0 := by
   change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
     mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnListF φs)) c = 0
   have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
@@ -135,7 +135,7 @@ lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul
 
 @[simp]
 lemma ι_normalOrderF_superCommuteF_eq_zero_mul
-    (a b c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛca * b) = 0 := by
+    (a b c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛF * b) = 0 := by
   change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
     mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) d = 0
   have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
@@ -151,25 +151,25 @@ lemma ι_normalOrderF_superCommuteF_eq_zero_mul
 
 @[simp]
 lemma ι_normalOrder_superCommuteF_eq_zero_mul_right (b c d : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ([d, c]ₛca * b) = 0 := by
+    ι 𝓝ᶠ([d, c]ₛF * b) = 0 := by
   rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 b c d]
   simp
 
 @[simp]
 lemma ι_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [d, c]ₛca) = 0 := by
+    ι 𝓝ᶠ(a * [d, c]ₛF) = 0 := by
   rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a 1 c d]
   simp
 
 @[simp]
 lemma ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.FieldOpFreeAlgebra) :
-    ι 𝓝ᶠ(a * [d, c]ₛca * b1 * b2) = 0 := by
+    ι 𝓝ᶠ(a * [d, c]ₛF * b1 * b2) = 0 := by
   rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a (b1 * b2) c d]
   congr 2
   noncomm_ring
 
 @[simp]
-lemma ι_normalOrderF_superCommuteF_eq_zero (c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
+lemma ι_normalOrderF_superCommuteF_eq_zero (c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ([d, c]ₛF) = 0 := by
   rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d]
   simp
 

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -324,7 +324,7 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (φ : 𝓕.Fi
 
 /--
 Within a proto-operator algebra we have that
-`φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛca`.
+`φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛF`.
 -/
 lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
     (φs : List 𝓕.FieldOp) : ofFieldOp φ * 𝓝(ofFieldOpList φs) =

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean

@@ -66,7 +66,7 @@ lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
 - `φsΛ.staticContract`
 - `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through
   uncontracted fields in `φ₀…φₖ₋₁`
-- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
+- the normal ordering of `[φsΛ]ᵘᶜ` with the field operator `φs[k]` removed.
 
 The proof of this result ultimately relies on
 - `staticContract_insert_some` to rewrite static contractions.

HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean

@@ -20,13 +20,13 @@ namespace FieldOpAlgebra
 variable {𝓕 : FieldSpecification}
 
 lemma ι_superCommuteF_eq_zero_of_ι_right_zero (a b : 𝓕.FieldOpFreeAlgebra) (h : ι b = 0) :
-    ι [a, b]ₛca = 0 := by
+    ι [a, b]ₛF = 0 := by
   rw [superCommuteF_expand_bosonicProjF_fermionicProjF]
   rw [ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero] at h
   simp_all
 
 lemma ι_superCommuteF_eq_zero_of_ι_left_zero (a b : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) :
-    ι [a, b]ₛca = 0 := by
+    ι [a, b]ₛF = 0 := by
   rw [superCommuteF_expand_bosonicProjF_fermionicProjF]
   rw [ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero] at h
   simp_all
@@ -38,12 +38,12 @@ lemma ι_superCommuteF_eq_zero_of_ι_left_zero (a b : 𝓕.FieldOpFreeAlgebra) (
 -/
 
 lemma ι_superCommuteF_right_zero_of_mem_ideal (a b : 𝓕.FieldOpFreeAlgebra)
-    (h : b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι [a, b]ₛca = 0 := by
+    (h : b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι [a, b]ₛF = 0 := by
   apply ι_superCommuteF_eq_zero_of_ι_right_zero
   exact (ι_eq_zero_iff_mem_ideal b).mpr h
 
 lemma ι_superCommuteF_eq_of_equiv_right (a b1 b2 : 𝓕.FieldOpFreeAlgebra) (h : b1 ≈ b2) :
-    ι [a, b1]ₛca = ι [a, b2]ₛca := by
+    ι [a, b1]ₛF = ι [a, b2]ₛF := by
   rw [equiv_iff_sub_mem_ideal] at h
   rw [LinearMap.sub_mem_ker_iff.mp]
   simp only [LinearMap.mem_ker, ← map_sub]
@@ -68,10 +68,10 @@ noncomputable def superCommuteRight (a : 𝓕.FieldOpFreeAlgebra) :
     simp
 
 lemma superCommuteRight_apply_ι (a b : 𝓕.FieldOpFreeAlgebra) :
-    superCommuteRight a (ι b) = ι [a, b]ₛca := by rfl
+    superCommuteRight a (ι b) = ι [a, b]ₛF := by rfl
 
 lemma superCommuteRight_apply_quot (a b : 𝓕.FieldOpFreeAlgebra) :
-    superCommuteRight a ⟦b⟧= ι [a, b]ₛca := by rfl
+    superCommuteRight a ⟦b⟧= ι [a, b]ₛF := by rfl
 
 lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 ≈ a2) :
     superCommuteRight a1 = superCommuteRight a2 := by
@@ -126,7 +126,7 @@ noncomputable def superCommute : FieldOpAlgebra 𝓕 →ₗ[ℂ]
 scoped[FieldSpecification.FieldOpAlgebra] notation "[" a "," b "]ₛ" => superCommute a b
 
 lemma superCommute_eq_ι_superCommuteF (a b : 𝓕.FieldOpFreeAlgebra) :
-    [ι a, ι b]ₛ = ι [a, b]ₛca := rfl
+    [ι a, ι b]ₛ = ι [a, b]ₛF := rfl
 
 /-!