feat: Redefine FieldOpAlgebra

2025-01-28 11:53:24 +00:00 · 2025-01-28 11:53:24 +00:00 · 48b0a60f34
commit 48b0a60f34
parent 43343376bd
6 changed files with 469 additions and 23 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean
@ -3,8 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
-import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 import Mathlib.RingTheory.GradedAlgebra.Basic
 /-!
@ -25,6 +24,19 @@ noncomputable section
 def statisticSubmodule  (f : FieldStatistic) :  Submodule ℂ 𝓕.CrAnAlgebra  :=
  Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ (𝓕 |>ₛ φs) = f}

+lemma ofCrAnList_mem_statisticSubmodule_of (φs : List 𝓕.CrAnStates) (f : FieldStatistic)
+  (h : (𝓕 |>ₛ φs) = f) :
+    ofCrAnList φs ∈ statisticSubmodule f  := by
+  refine Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, h⟩⟩
+
+lemma ofCrAnList_bosonic_or_fermionic (φs : List 𝓕.CrAnStates) :
+    ofCrAnList φs ∈ statisticSubmodule bosonic ∨ ofCrAnList φs ∈ statisticSubmodule fermionic := by
+  by_cases h : (𝓕 |>ₛ φs) = bosonic
+  · left
+    exact ofCrAnList_mem_statisticSubmodule_of φs bosonic h
+  · right
+    exact ofCrAnList_mem_statisticSubmodule_of φs fermionic (by simpa using h)
+
 /-- The projection of an element of `CrAnAlgebra` onto it's bosonic part. -/
 def bosonicProj : 𝓕.CrAnAlgebra →ₗ[ℂ] statisticSubmodule (𝓕 := 𝓕) bosonic :=
  Basis.constr ofCrAnListBasis ℂ fun φs =>
@ -276,6 +288,15 @@ instance : GradedAlgebra (A := 𝓕.CrAnAlgebra) statisticSubmodule where
      fermionicProj_of_fermionic_part, zero_add]
    conv_rhs => rw [directSum_eq_bosonic_plus_fermionic a]

+lemma eq_zero_of_bosonic_and_fermionic {a : 𝓕.CrAnAlgebra}
+    (hb : a ∈ statisticSubmodule bosonic) (hf : a ∈ statisticSubmodule fermionic) : a = 0 := by
+  have ha := bosonicProj_of_mem_bosonic a hb
+  have hb := fermionicProj_of_mem_fermionic a hf
+  have hc := (bosonicProj_add_fermionicProj a)
+  rw [ha, hb] at hc
+  simpa using hc
+
+
 end

 end CrAnAlgebra
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Grading
 /-!

 # Super Commute
@ -438,6 +439,349 @@ lemma superCommute_ofCrAnList_ofStateList_eq_sum (φs : List 𝓕.CrAnStates) :
    · simp
    · simp [Finset.mul_sum, smul_smul, ofStateList_cons, mul_assoc,
        FieldStatistic.ofList_cons_eq_mul, mul_comm]
+/-!
+
+## Interaction with grading.
+
+-/
+
+lemma superCommute_grade {a b : 𝓕.CrAnAlgebra} {f1 f2 : FieldStatistic}
+    (ha : a ∈ statisticSubmodule f1) (hb : b ∈ statisticSubmodule f2) :
+    [a, b]ₛca ∈ statisticSubmodule (f1 + f2) := by
+  let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule f2) : Prop :=
+       [a, a2]ₛca ∈ statisticSubmodule (f1 + f2)
+  change p b hb
+  apply Submodule.span_induction (p := p)
+  · intro x hx
+    obtain ⟨φs, rfl, hφs⟩ := hx
+    simp [p]
+    let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule f1) : Prop :=
+        [a2 , ofCrAnList φs]ₛca ∈ statisticSubmodule (f1 + f2)
+    change p a ha
+    apply Submodule.span_induction (p := p)
+    · intro x hx
+      obtain ⟨φs', rfl, hφs'⟩ := hx
+      simp [p]
+      rw [superCommute_ofCrAnList_ofCrAnList]
+      apply Submodule.sub_mem _
+      · apply ofCrAnList_mem_statisticSubmodule_of
+        rw [ofList_append_eq_mul, hφs, hφs']
+      · apply Submodule.smul_mem
+        apply ofCrAnList_mem_statisticSubmodule_of
+        rw [ofList_append_eq_mul, hφs, hφs']
+        rw [mul_comm]
+    · simp [p]
+    · intro x y hx hy hp1 hp2
+      simp [p]
+      exact Submodule.add_mem _ hp1 hp2
+    · intro c x hx hp1
+      simp [p]
+      exact Submodule.smul_mem _ c hp1
+    · exact ha
+  · simp [p]
+  · intro x y hx hy hp1 hp2
+    simp [p]
+    exact Submodule.add_mem _ hp1 hp2
+  · intro c x hx hp1
+    simp [p]
+    exact Submodule.smul_mem _ c hp1
+  · exact hb
+
+lemma superCommute_bosonic_bosonic {a b : 𝓕.CrAnAlgebra}
+    (ha : a ∈ statisticSubmodule bosonic) (hb : b ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = a * b - b * a := by
+  let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule bosonic) : Prop :=
+       [a, a2]ₛca = a * a2 - a2 * a
+  change p b hb
+  apply Submodule.span_induction (p := p)
+  · intro x hx
+    obtain ⟨φs, rfl, hφs⟩ := hx
+    let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule bosonic) : Prop :=
+        [a2 , ofCrAnList φs]ₛca = a2 * ofCrAnList φs - ofCrAnList φs * a2
+    change p a ha
+    apply Submodule.span_induction (p := p)
+    · intro x hx
+      obtain ⟨φs', rfl, hφs'⟩ := hx
+      simp [p]
+      rw [superCommute_ofCrAnList_ofCrAnList]
+      simp [hφs, ofCrAnList_append]
+    · simp [p]
+    · intro x y hx hy hp1 hp2
+      simp_all [p, mul_add, add_mul]
+      abel
+    · intro c x hx hp1
+      simp_all [p, smul_sub]
+    · exact ha
+  · simp [p]
+  · intro x y hx hy hp1 hp2
+    simp_all [p, mul_add, add_mul]
+    abel
+  · intro c x hx hp1
+    simp_all [p, smul_sub]
+  · exact hb
+
+
+lemma superCommute_bosonic_fermionic {a b : 𝓕.CrAnAlgebra}
+    (ha : a ∈ statisticSubmodule bosonic) (hb : b ∈ statisticSubmodule fermionic) :
+    [a, b]ₛca = a * b - b * a := by
+  let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule fermionic) : Prop :=
+       [a, a2]ₛca = a * a2 - a2 * a
+  change p b hb
+  apply Submodule.span_induction (p := p)
+  · intro x hx
+    obtain ⟨φs, rfl, hφs⟩ := hx
+    let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule bosonic) : Prop :=
+        [a2 , ofCrAnList φs]ₛca = a2 * ofCrAnList φs - ofCrAnList φs * a2
+    change p a ha
+    apply Submodule.span_induction (p := p)
+    · intro x hx
+      obtain ⟨φs', rfl, hφs'⟩ := hx
+      simp [p]
+      rw [superCommute_ofCrAnList_ofCrAnList]
+      simp [hφs, hφs', ofCrAnList_append]
+    · simp [p]
+    · intro x y hx hy hp1 hp2
+      simp_all [p, mul_add, add_mul]
+      abel
+    · intro c x hx hp1
+      simp_all [p, smul_sub]
+    · exact ha
+  · simp [p]
+  · intro x y hx hy hp1 hp2
+    simp_all [p, mul_add, add_mul]
+    abel
+  · intro c x hx hp1
+    simp_all [p, smul_sub]
+  · exact hb
+
+
+lemma superCommute_fermionic_bonsonic {a b : 𝓕.CrAnAlgebra}
+    (ha : a ∈ statisticSubmodule fermionic) (hb : b ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = a * b - b * a := by
+  let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule bosonic) : Prop :=
+       [a, a2]ₛca = a * a2 - a2 * a
+  change p b hb
+  apply Submodule.span_induction (p := p)
+  · intro x hx
+    obtain ⟨φs, rfl, hφs⟩ := hx
+    let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule fermionic) : Prop :=
+        [a2 , ofCrAnList φs]ₛca = a2 * ofCrAnList φs - ofCrAnList φs * a2
+    change p a ha
+    apply Submodule.span_induction (p := p)
+    · intro x hx
+      obtain ⟨φs', rfl, hφs'⟩ := hx
+      simp [p]
+      rw [superCommute_ofCrAnList_ofCrAnList]
+      simp [hφs, hφs', ofCrAnList_append]
+    · simp [p]
+    · intro x y hx hy hp1 hp2
+      simp_all [p, mul_add, add_mul]
+      abel
+    · intro c x hx hp1
+      simp_all [p, smul_sub]
+    · exact ha
+  · simp [p]
+  · intro x y hx hy hp1 hp2
+    simp_all [p, mul_add, add_mul]
+    abel
+  · intro c x hx hp1
+    simp_all [p, smul_sub]
+  · exact hb
+
+lemma superCommute_bonsonic {a b : 𝓕.CrAnAlgebra}  (hb : b ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = a * b - b * a := by
+  rw [← bosonicProj_add_fermionicProj a]
+  simp only [map_add, LinearMap.add_apply]
+  rw [superCommute_bosonic_bosonic (by simp) hb, superCommute_fermionic_bonsonic (by simp) hb]
+  simp only [add_mul, mul_add]
+  abel
+
+lemma bosonic_superCommute {a b : 𝓕.CrAnAlgebra}  (ha : a ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = a * b - b * a := by
+  rw [← bosonicProj_add_fermionicProj b]
+  simp only [map_add, LinearMap.add_apply]
+  rw [superCommute_bosonic_bosonic ha (by simp), superCommute_bosonic_fermionic ha (by simp)]
+  simp only [add_mul, mul_add]
+  abel
+
+lemma superCommute_bonsonic_symm {a b : 𝓕.CrAnAlgebra}  (hb : b ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = - [b, a]ₛca := by
+  rw [bosonic_superCommute hb, superCommute_bonsonic hb]
+  simp
+
+lemma bonsonic_superCommute_symm {a b : 𝓕.CrAnAlgebra}  (ha : a ∈ statisticSubmodule bosonic) :
+    [a, b]ₛca = - [b, a]ₛca := by
+  rw [bosonic_superCommute ha, superCommute_bonsonic ha]
+  simp
+
+lemma superCommute_fermionic_fermionic {a b : 𝓕.CrAnAlgebra}
+    (ha : a ∈ statisticSubmodule fermionic) (hb : b ∈ statisticSubmodule fermionic) :
+    [a, b]ₛca = a * b + b * a := by
+  let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule fermionic) : Prop :=
+       [a, a2]ₛca = a * a2 + a2 * a
+  change p b hb
+  apply Submodule.span_induction (p := p)
+  · intro x hx
+    obtain ⟨φs, rfl, hφs⟩ := hx
+    let p (a2 : 𝓕.CrAnAlgebra) (hx : a2 ∈ statisticSubmodule fermionic) : Prop :=
+        [a2 , ofCrAnList φs]ₛca = a2 * ofCrAnList φs + ofCrAnList φs * a2
+    change p a ha
+    apply Submodule.span_induction (p := p)
+    · intro x hx
+      obtain ⟨φs', rfl, hφs'⟩ := hx
+      simp [p]
+      rw [superCommute_ofCrAnList_ofCrAnList]
+      simp [hφs, hφs', ofCrAnList_append]
+    · simp [p]
+    · intro x y hx hy hp1 hp2
+      simp_all [p, mul_add, add_mul]
+      abel
+    · intro c x hx hp1
+      simp_all [p, smul_sub]
+    · exact ha
+  · simp [p]
+  · intro x y hx hy hp1 hp2
+    simp_all [p, mul_add, add_mul]
+    abel
+  · intro c x hx hp1
+    simp_all [p, smul_sub]
+  · exact hb
+
+lemma superCommute_fermionic_fermionic_symm {a b : 𝓕.CrAnAlgebra}
+    (ha : a ∈ statisticSubmodule fermionic) (hb : b ∈ statisticSubmodule fermionic) :
+    [a, b]ₛca = [b, a]ₛca := by
+  rw [superCommute_fermionic_fermionic ha hb]
+  rw [superCommute_fermionic_fermionic hb ha]
+  abel
+
+lemma superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic (φs φs' : List 𝓕.CrAnStates) :
+     [ofCrAnList φs, ofCrAnList φs']ₛca ∈ statisticSubmodule bosonic ∨
+    [ofCrAnList φs, ofCrAnList φs']ₛca ∈ statisticSubmodule fermionic := by
+  by_cases h1 : (𝓕 |>ₛ φs) = bosonic <;> by_cases h2 : (𝓕 |>ₛ φs') = bosonic
+  · left
+    have h : bosonic = bosonic + bosonic := by
+      simp only [add_eq_mul, instCommGroup, mul_self]
+      rfl
+    rw [h]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ h1
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ h2
+  · right
+    have h : fermionic = bosonic + fermionic := by
+      simp only [add_eq_mul, instCommGroup, mul_self]
+      rfl
+    rw [h]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ h1
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h2)
+  · right
+    have h : fermionic = fermionic + bosonic := by
+      simp only [add_eq_mul, instCommGroup, mul_self]
+      rfl
+    rw [h]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h1)
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ h2
+  · left
+    have h : bosonic = fermionic + fermionic := by
+      simp only [add_eq_mul, instCommGroup, mul_self]
+      rfl
+    rw [h]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h1)
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h2)
+
+
+lemma superCommute_bosonic_ofCrAnList_eq_sum (a : 𝓕.CrAnAlgebra) (φs : List 𝓕.CrAnStates)
+    (ha : a ∈ statisticSubmodule bosonic) :
+    [a, ofCrAnList φs]ₛca = ∑ (n : Fin φs.length),
+      ofCrAnList (φs.take n) * [a, ofCrAnState (φs.get n)]ₛca *
+      ofCrAnList (φs.drop (n + 1)) := by
+  let p (a : 𝓕.CrAnAlgebra) (ha : a ∈ statisticSubmodule bosonic) : Prop :=
+       [a, ofCrAnList φs]ₛca = ∑ (n : Fin φs.length),
+      ofCrAnList (φs.take n) * [a, ofCrAnState (φs.get n)]ₛca *
+      ofCrAnList (φs.drop (n + 1))
+  change p a ha
+  apply Submodule.span_induction (p := p)
+  · intro a ha
+    obtain ⟨φs, rfl, hφs⟩ := ha
+    simp [p]
+    rw [superCommute_ofCrAnList_ofCrAnList_eq_sum]
+    congr
+    funext n
+    simp [hφs]
+  · simp [p]
+  · intro x y hx hy hpx hpy
+    simp_all [p]
+    rw [← Finset.sum_add_distrib]
+    congr
+    funext n
+    simp [mul_add, add_mul]
+  · intro c x hx hpx
+    simp_all [p, Finset.smul_sum]
+  · exact ha
+
+
+lemma superCommute_fermionic_ofCrAnList_eq_sum (a : 𝓕.CrAnAlgebra) (φs : List 𝓕.CrAnStates)
+    (ha : a ∈ statisticSubmodule fermionic) :
+    [a, ofCrAnList φs]ₛca = ∑ (n : Fin φs.length),  𝓢(fermionic, 𝓕 |>ₛ φs.take n) •
+      ofCrAnList (φs.take n) * [a, ofCrAnState (φs.get n)]ₛca *
+      ofCrAnList (φs.drop (n + 1)) := by
+  let p (a : 𝓕.CrAnAlgebra) (ha : a ∈ statisticSubmodule fermionic) : Prop :=
+       [a, ofCrAnList φs]ₛca = ∑ (n : Fin φs.length), 𝓢(fermionic, 𝓕 |>ₛ φs.take n) •
+      ofCrAnList (φs.take n) * [a, ofCrAnState (φs.get n)]ₛca *
+      ofCrAnList (φs.drop (n + 1))
+  change p a ha
+  apply Submodule.span_induction (p := p)
+  · intro a ha
+    obtain ⟨φs, rfl, hφs⟩ := ha
+    simp [p]
+    rw [superCommute_ofCrAnList_ofCrAnList_eq_sum]
+    congr
+    funext n
+    simp [hφs]
+  · simp [p]
+  · intro x y hx hy hpx hpy
+    simp_all [p]
+    rw [← Finset.sum_add_distrib]
+    congr
+    funext n
+    simp [mul_add, add_mul]
+  · intro c x hx hpx
+    simp_all [p, Finset.smul_sum]
+    congr
+    funext x
+    simp [smul_smul, mul_comm]
+  · exact ha
+
+
+lemma statistic_neq_of_superCommute_fermionic {φs φs' : List 𝓕.CrAnStates}
+    (h : [ofCrAnList φs, ofCrAnList φs']ₛca ∈ statisticSubmodule fermionic) :
+    (𝓕 |>ₛ φs) ≠ (𝓕 |>ₛ φs') ∨ [ofCrAnList φs, ofCrAnList φs']ₛca = 0 := by
+  by_cases h0 : [ofCrAnList φs, ofCrAnList φs']ₛca = 0
+  · simp [h0]
+  simp [h0]
+  by_contra hn
+  refine h0 (eq_zero_of_bosonic_and_fermionic ?_ h)
+  by_cases hc : (𝓕 |>ₛ φs) = bosonic
+  · have h1 : bosonic = bosonic + bosonic := by
+      simp
+      rfl
+    rw [h1]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _ hc
+    apply ofCrAnList_mem_statisticSubmodule_of _ _
+    rw [← hn, hc]
+  · have h1 : bosonic = fermionic + fermionic := by
+      simp
+      rfl
+    rw [h1]
+    apply superCommute_grade
+    apply ofCrAnList_mem_statisticSubmodule_of _ _
+    simpa using hc
+    apply ofCrAnList_mem_statisticSubmodule_of _ _
+    rw [← hn]
+    simpa using hc

 end CrAnAlgebra

--- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean
@ -3,10 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.WickContraction.TimeContract
-import HepLean.Meta.Remark.Basic
-import Mathlib.RingTheory.TwoSidedIdeal.Operations
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
 import Mathlib.Algebra.RingQuot
+import Mathlib.RingTheory.TwoSidedIdeal.Operations
 /-!

 # Field operator algebra
@ -15,9 +14,7 @@ import Mathlib.Algebra.RingQuot

 namespace FieldSpecification
 open CrAnAlgebra
-open ProtoOperatorAlgebra
 open HepLean.List
-open WickContraction
 open FieldStatistic

 variable (𝓕 : FieldSpecification)
@ -26,8 +23,8 @@ variable (𝓕 : FieldSpecification)
  This contains e.g. the super-commutor of two creation operators. -/
 def fieldOpIdealSet : Set (CrAnAlgebra 𝓕) :=
  { x |
-    (∃ (φ ψ : 𝓕.CrAnStates) (a : CrAnAlgebra 𝓕),
-        x = a * [ofCrAnState φ, ofCrAnState ψ]ₛca - [ofCrAnState φ, ofCrAnState ψ]ₛca * a)
+    (∃ (φ1 φ2 φ3 : 𝓕.CrAnStates),
+        x = [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca)
    ∨ (∃ (φc φc' : 𝓕.CrAnStates) (_ : 𝓕 |>ᶜ φc = .create) (_ : 𝓕 |>ᶜ φc' = .create),
      x = [ofCrAnState φc, ofCrAnState φc']ₛca)
    ∨ (∃ (φa φa' : 𝓕.CrAnStates) (_ : 𝓕 |>ᶜ φa = .annihilate) (_ : 𝓕 |>ᶜ φa' = .annihilate),
@ -75,19 +72,6 @@ lemma ι_of_mem_fieldOpIdealSet (x : CrAnAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpI
  refine RingConGen.Rel.of x 0 ?_
  simpa using hx

-lemma ι_superCommute_ofCrAnState_ofCrAnState_mem_center (φ ψ : 𝓕.CrAnStates) :
-    ι [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
-  rw [Subalgebra.mem_center_iff]
-  intro b
-  obtain ⟨b, rfl⟩ := ι_surjective b
-  rw [← map_mul, ← map_mul]
-  rw [LinearMap.sub_mem_ker_iff.mp]
-  simp only [LinearMap.mem_ker]
-  apply ι_of_mem_fieldOpIdealSet
-  simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq]
-  left
-  use φ, ψ, b
-
 lemma ι_superCommute_of_create_create (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = .create)
    (hφc' : 𝓕 |>ᶜ φc' = .create) : ι [ofCrAnState φc, ofCrAnState φc']ₛca = 0 := by
  apply ι_of_mem_fieldOpIdealSet
@ -117,5 +101,95 @@ lemma ι_superCommute_of_diff_statistic (φ ψ : 𝓕.CrAnStates)
  right
  use φ, ψ

+lemma ι_superCommute_zero_of_fermionic (φ ψ : 𝓕.CrAnStates)
+    (h : [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ statisticSubmodule fermionic) :
+    ι [ofCrAnState φ, ofCrAnState ψ]ₛca = 0 := by
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton] at h ⊢
+  rcases statistic_neq_of_superCommute_fermionic h with h | h
+  · simp [ofCrAnList_singleton]
+    apply ι_superCommute_of_diff_statistic _ _
+    simpa using h
+  · simp [h]
+
+lemma ι_superCommute_ofCrAnState_ofCrAnState_bosonic_or_zero (φ ψ : 𝓕.CrAnStates) :
+     [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ statisticSubmodule bosonic  ∨
+     ι [ofCrAnState φ, ofCrAnState ψ]ₛca = 0 := by
+  rcases superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic [φ] [ψ] with h | h
+  · simp_all [ofCrAnList_singleton]
+  · simp_all [ofCrAnList_singleton]
+    right
+    exact ι_superCommute_zero_of_fermionic _ _ h
+
+/-!
+
+## Super-commutes are in the center
+
+-/
+
+@[simp]
+lemma ι_superCommute_ofCrAnState_superCommute_ofCrAnState_ofCrAnState (φ1 φ2 φ3 : 𝓕.CrAnStates) :
+    ι [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca = 0 := by
+  apply ι_of_mem_fieldOpIdealSet
+  simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq]
+  left
+  use φ1, φ2, φ3
+
+@[simp]
+lemma ι_superCommute_superCommute_ofCrAnState_ofCrAnState_ofCrAnState (φ1 φ2 φ3 : 𝓕.CrAnStates) :
+    ι [[ofCrAnState φ1, ofCrAnState φ2]ₛca, ofCrAnState φ3]ₛca = 0 := by
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_singleton]
+  rcases superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic [φ1] [φ2] with h | h
+  · rw [bonsonic_superCommute_symm h]
+    simp [ofCrAnList_singleton]
+  · rcases ofCrAnList_bosonic_or_fermionic [φ3] with h' | h'
+    · rw [superCommute_bonsonic_symm h']
+      simp [ofCrAnList_singleton]
+    · rw [superCommute_fermionic_fermionic_symm h h']
+      simp [ofCrAnList_singleton]
+
+@[simp]
+lemma ι_superCommute_superCommute_ofCrAnState_ofCrAnState_ofCrAnList (φ1 φ2 : 𝓕.CrAnStates)
+    (φs : List 𝓕.CrAnStates) :
+    ι [[ofCrAnState φ1, ofCrAnState φ2]ₛca, ofCrAnList φs]ₛca = 0 := by
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton]
+  rcases superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic [φ1] [φ2] with h | h
+  · rw [superCommute_bosonic_ofCrAnList_eq_sum _ _ h]
+    simp [ofCrAnList_singleton]
+  · rw [superCommute_fermionic_ofCrAnList_eq_sum _ _ h]
+    simp [ofCrAnList_singleton]
+
+@[simp]
+lemma ι_superCommute_superCommute_ofCrAnState_ofCrAnState_crAnAlgebra (φ1 φ2 : 𝓕.CrAnStates)
+    (a : 𝓕.CrAnAlgebra) : ι [[ofCrAnState φ1, ofCrAnState φ2]ₛca, a]ₛca = 0 := by
+  change (ι.toLinearMap ∘ₗ superCommute [ofCrAnState φ1, ofCrAnState φ2]ₛca) a = _
+  have h1 : (ι.toLinearMap ∘ₗ superCommute [ofCrAnState φ1, ofCrAnState φ2]ₛca) = 0 := by
+    apply (ofCrAnListBasis.ext fun l ↦ ?_)
+    simp
+  rw [h1]
+  simp
+
+lemma ι_commute_crAnAlgebra_superCommute_ofCrAnState_ofCrAnState (φ1 φ2 : 𝓕.CrAnStates)
+    (a : 𝓕.CrAnAlgebra) : ι a * ι [ofCrAnState φ1, ofCrAnState φ2]ₛca -
+    ι [ofCrAnState φ1, ofCrAnState φ2]ₛca * ι a = 0 := by
+  rcases ι_superCommute_ofCrAnState_ofCrAnState_bosonic_or_zero φ1 φ2 with h | h
+  swap
+  · simp [h]
+  trans - ι [[ofCrAnState φ1, ofCrAnState φ2]ₛca, a]ₛca
+  · rw [bosonic_superCommute h]
+    simp
+  · simp
+
+lemma ι_superCommute_ofCrAnState_ofCrAnState_mem_center (φ ψ : 𝓕.CrAnStates) :
+    ι [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
+  rw [Subalgebra.mem_center_iff]
+  intro a
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  have h0 := ι_commute_crAnAlgebra_superCommute_ofCrAnState_ofCrAnState φ ψ a
+  trans ι ((superCommute (ofCrAnState φ)) (ofCrAnState ψ)) * ι a + 0
+  swap
+  simp
+  rw [← h0]
+  abel
+
 end FieldOpAlgebra
 end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
@ -3,6 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic
 /-!

@ -12,7 +13,6 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic

 namespace FieldSpecification
 open CrAnAlgebra
-open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
 open FieldStatistic
--- a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
@ -300,5 +300,8 @@ instance : AddMonoid FieldStatistic where
    simp only [instCommGroup, Finset.prod_const, Finset.card_univ, Fintype.card_fin]
    rfl

+@[simp]
+lemma add_eq_mul (a b : FieldStatistic) : a + b = a * b := rfl
+
 end ofListTake
 end FieldStatistic
--- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
@ -71,6 +71,10 @@ lemma exchangeSign_bosonic (a : FieldStatistic) : 𝓢(a, bosonic) = 1 := by
 lemma bosonic_exchangeSign (a : FieldStatistic) : 𝓢(bosonic, a) = 1 := by
  rw [exchangeSign_symm, exchangeSign_bosonic]

+@[simp]
+lemma fermionic_exchangeSign_fermionic : 𝓢(fermionic, fermionic) =  - 1 := by
+  rfl
+
 lemma exchangeSign_eq_if (a b : FieldStatistic) :
    𝓢(a, b) = if a = fermionic ∧ b = fermionic then - 1 else 1 := by
  fin_cases a <;> fin_cases b <;> rfl