feat: Some properties of normal order

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean

@@ -422,5 +422,33 @@ lemma ι_eq_zero_iff_ι_bosonicProj_fermonicProj_zero (x : CrAnAlgebra 𝓕) :
     rw [← bosonicProj_add_fermionicProj x]
     simp_all
 
+/-!
+
+## Constructors
+
+-/
+
+/-- An element of `FieldOpAlgebra` from a `States`. -/
+def ofFieldOp (φ : 𝓕.States) : 𝓕.FieldOpAlgebra := ι (ofState φ)
+
+lemma ofFieldOp_eq_ι_ofState (φ : 𝓕.States) : ofFieldOp φ = ι (ofState φ) := rfl
+
+/-- An element of `FieldOpAlgebra` from a list of `States`. -/
+def ofFieldOpList (φs : List 𝓕.States) : 𝓕.FieldOpAlgebra := ι (ofStateList φs)
+
+lemma ofFieldOpList_eq_ι_ofStateList (φs : List 𝓕.States) :
+  ofFieldOpList φs = ι (ofStateList φs) := rfl
+
+/-- An element of `FieldOpAlgebra` from a `CrAnStates`. -/
+def ofCrAnFieldOp (φ : 𝓕.CrAnStates) : 𝓕.FieldOpAlgebra := ι (ofCrAnState φ)
+
+lemma ofCrAnFieldOp_eq_ι_ofCrAnState (φ : 𝓕.CrAnStates) :
+  ofCrAnFieldOp φ = ι (ofCrAnState φ) := rfl
+
+/-- An element of `FieldOpAlgebra` from a list of `CrAnStates`. -/
+def ofCrAnFieldOpList (φs : List 𝓕.CrAnStates) : 𝓕.FieldOpAlgebra := ι (ofCrAnList φs)
+
+lemma ofCrAnFieldOpList_eq_ι_ofCrAnList (φs : List 𝓕.CrAnStates) :
+  ofCrAnFieldOpList φs = ι (ofCrAnList φs) := rfl
 end FieldOpAlgebra
 end FieldSpecification

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean

@@ -4,7 +4,7 @@ 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
+import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute
 /-!
 
 # Normal Ordering on Field operator algebra
@@ -231,5 +231,60 @@ noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra
     rw [← map_smul, ι_apply, ι_apply]
     simp
 
+@[inherit_doc normalOrder]
+scoped[FieldSpecification.FieldOpAlgebra] notation "𝓝(" a ")" => normalOrder a
+
+/-!
+
+## Properties of normal ordering.
+
+-/
+
+lemma normalOrder_eq_ι_normalOrderF (a : 𝓕.CrAnAlgebra) :
+    𝓝(ι a) = ι 𝓝ᶠ(a) := rfl
+
+/-!
+
+### Normal order and super commutes
+
+-/
+
+@[simp]
+lemma normalOrder_superCommute_eq_zero (a b : 𝓕.FieldOpAlgebra) :
+    𝓝([a, b]ₛ) = 0 := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  rw [superCommute_eq_ι_superCommuteF, normalOrder_eq_ι_normalOrderF]
+  simp
+
+@[simp]
+lemma normalOrder_superCommute_left_eq_zero (a b c: 𝓕.FieldOpAlgebra) :
+    𝓝([a, b]ₛ * c) = 0 := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  obtain ⟨c, rfl⟩ := ι_surjective c
+  rw [superCommute_eq_ι_superCommuteF, ← map_mul, normalOrder_eq_ι_normalOrderF]
+  simp
+
+@[simp]
+lemma normalOrder_superCommute_right_eq_zero (a b c: 𝓕.FieldOpAlgebra) :
+    𝓝(c * [a, b]ₛ) = 0 := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  obtain ⟨c, rfl⟩ := ι_surjective c
+  rw [superCommute_eq_ι_superCommuteF, ← map_mul, normalOrder_eq_ι_normalOrderF]
+  simp
+
+@[simp]
+lemma normalOrder_superCommute_mid_eq_zero (a b c d : 𝓕.FieldOpAlgebra) :
+    𝓝(a * [c, d]ₛ * b) = 0 := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  obtain ⟨c, rfl⟩ := ι_surjective c
+  obtain ⟨d, rfl⟩ := ι_surjective d
+  rw [superCommute_eq_ι_superCommuteF, ← map_mul, ← map_mul, normalOrder_eq_ι_normalOrderF]
+  simp
+
+
 end FieldOpAlgebra
 end FieldSpecification

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean

@@ -114,8 +114,8 @@ noncomputable def superCommute : FieldOpAlgebra 𝓕 →ₗ[ℂ]
 @[inherit_doc superCommute]
 scoped[FieldSpecification.FieldOpAlgebra] notation "[" a "," b "]ₛ" => superCommute a b
 
-lemma ι_superCommuteF_eq_superCommute (a b : 𝓕.CrAnAlgebra) :
-    ι [a, b]ₛca = [ι a, ι b]ₛ := rfl
+lemma superCommute_eq_ι_superCommuteF (a b : 𝓕.CrAnAlgebra) :
+    [ι a, ι b]ₛ = ι [a, b]ₛca := rfl
 
 end FieldOpAlgebra
 end FieldSpecification