PhysLean/HepLean/PerturbationTheory/Wick/Algebra.lean

/-
Copyright (c) 2024 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.Wick.Species
import HepLean.Lorentz.RealVector.Basic
import HepLean.Mathematics.Fin
import HepLean.SpaceTime.Basic
import HepLean.Mathematics.SuperAlgebra.Basic
import HepLean.Mathematics.List
import HepLean.Meta.Notes.Basic
import Init.Data.List.Sort.Basic
/-!

# Operator algebra

Currently this file is only for an example of Wick strings, correpsonding to a
theory with two complex scalar fields. The concepts will however generalize.

We will formally define the operator ring, in terms of the fields present in the theory.

## Futher reading

- https://physics.stackexchange.com/questions/258718/ and links therein
- Ryan Thorngren (https://physics.stackexchange.com/users/10336/ryan-thorngren), Fermions,
  different species and (anti-)commutation rules, URL (version: 2019-02-20) :
  https://physics.stackexchange.com/q/461929
- Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
-/

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:
  "

/-- The abstract notion of a operator algebra containing all the necessary ingrediants
  to do perturbation theory.
  Warning: The definition here is not complete. -/
@[note_attr]
structure WickAlgebra (S : Species) where
  /-- The underlying operator algebra. -/
  A : Type
  /-- The type `A` is a semiring. -/
  [A_semiring : Semiring A]
  /-- The type `A` is an algebra. -/
  [A_algebra : Algebra ℂ A]
  /-- Position based field operators. -/
  ψ : S.𝓯 → SpaceTime → A
  /-- Position based constructive operators. -/
  ψc : S.𝓯 → SpaceTime → A
  /-- Position based destructive operators. -/
  ψd : S.𝓯 → SpaceTime → A
  /-- Constructive asymptotic operators. -/
  φc : S.𝓯 → Lorentz.Contr 3 → A
  /-- Distructive asymptotic operators. -/
  φd : S.𝓯 → Lorentz.Contr 3 → A
  ψc_ψd : ∀ i x, ψc i x + ψd i x = ψ i x
  /- Self comutators. -/
  ψc_comm_ψc : ∀ i j x y, ψc i x * ψc j y + (S.commFactor i j) • ψc j y * ψc i x = 0
  ψd_comm_ψd : ∀ i j x y, ψd i x * ψd j y + (S.commFactor i j) • ψd j y * ψd i x = 0
  φc_comm_φc : ∀ i j x y, φc i x * φc j y + (S.commFactor i j) • φc j y * φc i x = 0
  φd_comm_φd : ∀ i j x y, φd i x * φd j y + (S.commFactor i j) • φd j y * φd i x = 0
  /- Cross comutators. -/

namespace WickAlgebra

variable {S : Species} (𝓞 : WickAlgebra S)

/-- The type `A` of a Wick algebra is a semi-ring. -/
instance : Semiring 𝓞.A := 𝓞.A_semiring

/-- The type `A` of a Wick algebra is an algebra. -/
instance : Algebra ℂ 𝓞.A := 𝓞.A_algebra

end WickAlgebra

namespace Species

variable (S : Species)

note r"
<h2>Order</h2>
Suppose we have a type $I$ with a order $r$, a map $g : I \to \mathbb{Z}/2$,
and a map $f : I \to A$ such that $f(i) \in A_{g(i)}$.
Consider the free algebra generated by $I$, which we will denote $A_I$.
The map $f$ can be extended to a map $T_r : A_I \to A$ such that
a monomial $i_1 \cdots i_n$ gets mapped to $(-1)^{K(σ)}f(i_{σ(1)})...f(i_{σ(n)})$ where $σ$ is the
permutation oredering the $i$'s by $r$ (preserving the order of terms which are equal under $r$),
and $K(σ)$ is the Koszul sign factor. (see e.g. PSE:24157)
<br><br>
There are two types $I$ we are intrested in.
"

/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
  for each fermion-fermion cross. -/
def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
    List I → ℂ
  | [] => 1
  | b :: l => if r a b then 1 else
    if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l

/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
    (ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
  | [] => by
    simp [koszulSignInsert]
  | b :: l => by
    simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
    intro _
    simp only [ha, Fin.isValue, zero_ne_one, false_and, ↓reduceIte]
    exact koszulSignInsert_boson r q a ha l

/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
  a list of based on `r`. -/
def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
    List I → ℂ
  | [] => 1
  | a :: l => koszulSignInsert r q a l * koszulSign r q l

@[simp]
lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
    (i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
  change koszulSign r q [i] = 1
  simp only [koszulSign, mul_one]
  rfl

noncomputable section

/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra ℂ (FreeMonoid I)` by `r` giving it
  a signed dependent on `q`. -/
def koszulOrderMonoidAlgebra {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
    MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
  Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid I)) ℂ (List I)
    (fun i => Finsupp.lsingle (R := ℂ) (List.insertionSort r i) (koszulSign r q i))

@[simp]
lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [DecidableRel r]
    (q : I → Fin 2) (i : List I) :
    koszulOrderMonoidAlgebra r q (MonoidAlgebra.of ℂ (FreeMonoid I) i) =
    (koszulSign r q i) • (MonoidAlgebra.of ℂ (FreeMonoid I) (List.insertionSort r i)) := by
  simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
    MonoidAlgebra.smul_single', mul_one]
  rw [MonoidAlgebra.ext_iff]
  intro x
  erw [Finsupp.lift_apply]
  simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
    one_mul]

@[simp]
lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
    (l : FreeMonoid I) (x : ℂ) :
    koszulOrderMonoidAlgebra r q (MonoidAlgebra.single l x)
    = (koszulSign r q l) • (MonoidAlgebra.single (List.insertionSort r l) x) := by
  simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
  rw [MonoidAlgebra.ext_iff]
  intro x'
  erw [Finsupp.lift_apply]
  simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
    one_mul, MonoidAlgebra.single]
  congr 2
  rw [NonUnitalNormedCommRing.mul_comm]

/-- Given a relation `r` on `I` sorts elements of `FreeAlgebra ℂ I` by `r` giving it
  a signed dependent on `q`. -/
def koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
    FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
  FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
  ∘ₗ koszulOrderMonoidAlgebra r q
  ∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap

lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i : I) :
    koszulOrder r q (FreeAlgebra.ι ℂ i) = FreeAlgebra.ι ℂ i := by
  simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
    koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, LinearMap.coe_comp, Function.comp_apply,
    AlgEquiv.toLinearMap_apply]
  rw [AlgEquiv.symm_apply_eq]
  simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
    AlgEquiv.ofAlgHom_apply, FreeAlgebra.lift_ι_apply]
  rw [@MonoidAlgebra.ext_iff]
  intro x
  erw [Finsupp.lift_apply]
  simp only [MonoidAlgebra.smul_single', List.insertionSort, List.orderedInsert,
    koszulSign_freeMonoid_of, mul_one, Finsupp.single_zero, Finsupp.sum_single_index]
  rfl

@[simp]
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
    (l : FreeMonoid I) :
    koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
    = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
    (MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
  simp [koszulOrder]

end

/-- The indexing set of constructive and destructive position based operators. -/
def ConstDestAlgebra.index : Type := Fin 2 × S.𝓯 × SpaceTime

/-- The free algebra generated by constructive and destructive parts of fields position-based
  fields. -/
abbrev ConstDestAlgebra := FreeAlgebra ℂ (ConstDestAlgebra.index S)

/-- The indexing set of position based field operators. -/
def FieldAlgebra.index : Type := S.𝓯 × SpaceTime

/-- The free algebra generated by fields. -/
abbrev FieldAlgebra := FreeAlgebra ℂ (FieldAlgebra.index S)

namespace ConstDestAlgebra

variable {S} (𝓞 : WickAlgebra S)

/-- The inclusion of constructive and destructive fields into the full operator algebra. -/
def toWickAlgebra : ConstDestAlgebra S →ₐ[ℂ] 𝓞.A :=
  FreeAlgebra.lift ℂ (fun (i, f, x) =>
    match i with
    | 0 => 𝓞.ψc f x
    | 1 => 𝓞.ψd f x)

@[simp]
lemma toWickAlgebra_ι_zero (x : S.𝓯 × SpaceTime) :
    toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ (0, x)) = 𝓞.ψc x.1 x.2 := by
  simp [toWickAlgebra]

@[simp]
lemma toWickAlgebra_ι_one (x : S.𝓯 × SpaceTime) :
    toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ (1, x)) = 𝓞.ψd x.1 x.2 := by
  simp [toWickAlgebra]

/-- The time ordering relation on constructive and destructive operators. -/
def timeOrderRel : index S → index S → Prop := fun x y => x.2.2 0 ≤ y.2.2 0

/-- The normal ordering relation on constructive and destructive operators. -/
def normalOrderRel : index S → index S → Prop := fun x y => x.1 ≤ y.1

/-- The normal ordering relation of constructive and destructive operators is decidable. -/
instance : DecidableRel (@normalOrderRel S) := fun a b => a.1.decLe b.1

noncomputable section

/-- The time ordering relation of constructive and destructive operators is decidable. -/
instance : DecidableRel (@timeOrderRel S) :=
  fun a b => Real.decidableLE (a.2.2 0) (b.2.2 0)

/-- The time ordering of constructive and destructive operators. -/
def timeOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
  koszulOrder timeOrderRel q

/-- The normal ordering of constructive and destructive operators. -/
def normalOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
  koszulOrder normalOrderRel q

/-- Contraction of constructive and destructive operators, defined as their time
  ordering minus their normal ordering. -/
def contract (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
  timeOrder q - normalOrder q

informal_lemma timeOrder_comm_normalOrder where
  math :≈ "time ordering and normal ordering commute."
  deps :≈ [``timeOrder, ``normalOrder]

end

end ConstDestAlgebra

namespace FieldAlgebra

variable {S} (𝓞 : WickAlgebra S)

/-- The inclusion fo the field algebra into the operator algebra. -/
def toWickAlgebra : FieldAlgebra S →ₐ[ℂ] 𝓞.A :=
  FreeAlgebra.lift ℂ (fun i => 𝓞.ψ i.1 i.2)

@[simp]
lemma toWickAlgebra_ι (i : index S) : toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ i) = 𝓞.ψ i.1 i.2 := by
  simp [toWickAlgebra]

/-- The time ordering relation in the field algebra. -/
def timeOrderRel : index S → index S → Prop := fun x y => x.2 0 ≤ y.2 0

/-- The time ordering relation in the field algebra is decidable. -/
noncomputable instance : DecidableRel (@timeOrderRel S) :=
  fun a b => Real.decidableLE (a.2 0) (b.2 0)

/-- The time ordering in the field algebra. -/
noncomputable def timeOrder (q : index S → Fin 2) : S.FieldAlgebra →ₗ[ℂ] S.FieldAlgebra :=
  koszulOrder timeOrderRel q

/-- Given a list of fields and a map `f` tell us which field is constructive and
  which is destructive, a list of constructive and destructive fields. -/
def listToConstDestList : (l : List (index S)) →
    (f : Fin l.length → Fin 2) → List (ConstDestAlgebra.index S)
  | [], _ => []
  | i :: l, f =>
    (f ⟨0, Nat.zero_lt_succ l.length⟩, i.1, i.2) :: listToConstDestList l (f ∘ Fin.succ)

@[simp]
lemma listToConstDestList_length (l : List (index S)) (f : Fin l.length → Fin 2) :
    (listToConstDestList l f).length = l.length := by
  induction l with
  | nil => rfl
  | cons i l ih =>
    simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Prod.mk.eta, add_left_inj]
    rw [ih]

lemma listToConstDestList_insertionSortEquiv (l : List (index S))
    (f : Fin l.length → Fin 2) :
    (HepLean.List.insertionSortEquiv ConstDestAlgebra.timeOrderRel (listToConstDestList l f))
    = (Fin.castOrderIso (by simp)).toEquiv.trans
    ((HepLean.List.insertionSortEquiv timeOrderRel l).trans
    (Fin.castOrderIso (by simp)).toEquiv) := by
  induction l with
  | nil =>
    simp [listToConstDestList, HepLean.List.insertionSortEquiv]
  | cons i l ih =>
    simp only [listToConstDestList, List.length_cons, Fin.zero_eta, List.insertionSort]
    conv_lhs => simp [HepLean.List.insertionSortEquiv]
    have h1 (l' : List (ConstDestAlgebra.index S)) :
        (HepLean.List.insertEquiv ConstDestAlgebra.timeOrderRel (f ⟨0, by simp⟩, i.1, i.2) l') =
        (Fin.castOrderIso (by simp)).toEquiv.trans
        ((HepLean.List.insertEquiv timeOrderRel (i.1, i.2) (l'.unzip).2).trans
        (Fin.castOrderIso (by simp [List.orderedInsert_length])).toEquiv) := by
      induction l' with
      | nil =>
        simp only [List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta, List.length_singleton,
          List.orderedInsert, HepLean.List.insertEquiv, Fin.castOrderIso_refl,
          OrderIso.refl_toEquiv, Equiv.trans_refl]
        rfl
      | cons j l' ih' =>
        by_cases hr : ConstDestAlgebra.timeOrderRel (f ⟨0, by simp⟩, i) j
        · rw [HepLean.List.insertEquiv_cons_pos]
          · erw [HepLean.List.insertEquiv_cons_pos]
            · rfl
            · exact hr
          · exact hr
        · rw [HepLean.List.insertEquiv_cons_neg]
          · erw [HepLean.List.insertEquiv_cons_neg]
            · simp only [List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta,
              List.orderedInsert, Prod.mk.eta, Fin.mk_one]
              erw [ih']
              ext x
              simp only [Prod.mk.eta, List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta,
                HepLean.Fin.equivCons_trans, Nat.succ_eq_add_one,
                HepLean.Fin.equivCons_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
                Fin.castOrderIso_apply, Fin.cast_trans, Fin.coe_cast]
              congr 2
              match x with
              | ⟨0, h⟩ => rfl
              | ⟨1, h⟩ => rfl
              | ⟨Nat.succ (Nat.succ x), h⟩ => rfl
            · exact hr
          · exact hr
    erw [h1]
    rw [ih]
    simp only [HepLean.Fin.equivCons_trans, Nat.succ_eq_add_one,
      HepLean.Fin.equivCons_castOrderIso, List.length_cons, Nat.add_zero, Nat.zero_eq,
      Fin.zero_eta]
    ext x
    conv_rhs => simp [HepLean.List.insertionSortEquiv]
    simp only [Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_trans,
      Fin.coe_cast]
    have h2' (i : ConstDestAlgebra.index S) (l' : List (ConstDestAlgebra.index S)) :
      (List.orderedInsert ConstDestAlgebra.timeOrderRel i l').unzip.2 =
      List.orderedInsert timeOrderRel i.2 l'.unzip.2 := by
      induction l' with
      | nil =>
        simp [HepLean.List.insertEquiv]
      | cons j l' ih' =>
        by_cases hij : ConstDestAlgebra.timeOrderRel i j
        · rw [List.orderedInsert_of_le]
          · erw [List.orderedInsert_of_le]
            · simp
            · exact hij
          · exact hij
        · simp only [List.orderedInsert, hij, ↓reduceIte, List.unzip_snd, List.map_cons]
          have hn : ¬ timeOrderRel i.2 j.2 := hij
          simp only [hn, ↓reduceIte, List.cons.injEq, true_and]
          simpa using ih'
    have h2 (l' : List (ConstDestAlgebra.index S)) :
        (List.insertionSort ConstDestAlgebra.timeOrderRel l').unzip.2 =
        List.insertionSort timeOrderRel l'.unzip.2 := by
      induction l' with
      | nil =>
        simp [HepLean.List.insertEquiv]
      | cons i l' ih' =>
        simp only [List.insertionSort, List.unzip_snd]
        simp only [List.unzip_snd] at h2'
        rw [h2']
        congr
        simpa using ih'
    rw [HepLean.List.insertEquiv_congr _ _ _ (h2 _)]
    simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
      Fin.cast_trans, Fin.coe_cast]
    have h3 : (List.insertionSort timeOrderRel (listToConstDestList l (f ∘ Fin.succ)).unzip.2) =
      List.insertionSort timeOrderRel l := by
      congr
      have h3' (l : List (index S)) (f : Fin l.length → Fin 2) :
        (listToConstDestList l (f)).unzip.2 = l := by
        induction l with
        | nil => rfl
        | cons i l ih' =>
          simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Prod.mk.eta,
            List.unzip_snd, List.map_cons, List.cons.injEq, true_and]
          simpa using ih' (f ∘ Fin.succ)
      rw [h3']
    rw [HepLean.List.insertEquiv_congr _ _ _ h3]
    simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
      Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
    rfl

lemma listToConstDestList_get (l : List (index S)) (f : Fin l.length → Fin 2) :
    (listToConstDestList l f).get = (fun i => (f i, l.get i)) ∘ Fin.cast (by simp) := by
  induction l with
  | nil =>
    funext i
    exact Fin.elim0 i
  | cons i l ih =>
    simp only [listToConstDestList, List.length_cons, Fin.zero_eta, List.get_eq_getElem]
    funext x
    match x with
    | ⟨0, h⟩ => rfl
    | ⟨x + 1, h⟩ =>
      simp only [List.length_cons, List.get_eq_getElem, Prod.mk.eta, List.getElem_cons_succ,
        Function.comp_apply, Fin.cast_mk]
      change (listToConstDestList l _).get _ = _
      rw [ih]
      simp

lemma listToConstDestList_timeOrder (l : List (index S)) (f : Fin l.length → Fin 2) :
    List.insertionSort ConstDestAlgebra.timeOrderRel (listToConstDestList l f) =
    listToConstDestList (List.insertionSort timeOrderRel l)
    (f ∘ (HepLean.List.insertionSortEquiv (timeOrderRel) l).symm) := by
  let l1 := List.insertionSort (ConstDestAlgebra.timeOrderRel) (listToConstDestList l f)
  let l2 := listToConstDestList (List.insertionSort timeOrderRel l)
    (f ∘ (HepLean.List.insertionSortEquiv (timeOrderRel) l).symm)
  change l1 = l2
  have hlen : l1.length = l2.length := by
    simp [l1, l2]
  have hget : l1.get = l2.get ∘ Fin.cast hlen := by
    rw [← HepLean.List.insertionSortEquiv_get]
    rw [listToConstDestList_get]
    rw [listToConstDestList_get]
    rw [← HepLean.List.insertionSortEquiv_get]
    funext i
    simp only [List.get_eq_getElem, Function.comp_apply, Fin.coe_cast, Fin.cast_trans]
    congr 2
    · rw [listToConstDestList_insertionSortEquiv]
      simp
    · rw [listToConstDestList_insertionSortEquiv]
      simp
  apply List.ext_get hlen
  rw [hget]
  simp

lemma listToConstDestList_koszulSignInsert (q : index S → Fin 2) (l : List (index S)) (i : index S)
    (f : Fin l.length → Fin 2) (a : Fin 2) :
    koszulSignInsert ConstDestAlgebra.timeOrderRel (fun i => q i.2) (a, i)
    (listToConstDestList l f) = koszulSignInsert timeOrderRel q i l := by
  induction l with
  | nil =>
    simp [listToConstDestList, koszulSignInsert]
  | cons j s ih =>
    simp only [koszulSignInsert, List.length_cons, Fin.zero_eta, Prod.mk.eta, Fin.isValue]
    by_cases hr : ConstDestAlgebra.timeOrderRel (a, i) (f ⟨0, by simp⟩, j)
    · rw [if_pos]
      · rw [if_pos]
        · exact hr
      · exact hr
    · rw [if_neg]
      · nth_rewrite 2 [if_neg]
        · rw [ih (f ∘ Fin.succ)]
        · exact hr
      · exact hr

lemma listToConstDestList_koszulSign (q : index S → Fin 2) (l : List (index S))
    (f : Fin l.length → Fin 2) :
    koszulSign ConstDestAlgebra.timeOrderRel (fun i => q i.2) (listToConstDestList l f) =
    koszulSign timeOrderRel q l := by
  induction l with
  | nil => rfl
  | cons i l ih =>
    simp only [koszulSign, List.length_cons, Fin.zero_eta, Prod.mk.eta]
    rw [ih]
    simp only [mul_eq_mul_right_iff]
    apply Or.inl
    exact listToConstDestList_koszulSignInsert q l i _ _

/-- The map from the field algebra to the algebra of constructive and destructive fields. -/
def toConstDestAlgebra : FieldAlgebra S →ₐ[ℂ] ConstDestAlgebra S :=
  FreeAlgebra.lift ℂ (fun i => FreeAlgebra.ι ℂ (0, i) + FreeAlgebra.ι ℂ (1, i))

@[simp]
lemma toConstDestAlgebra_ι (i : index S) : toConstDestAlgebra (FreeAlgebra.ι ℂ i) =
    FreeAlgebra.ι ℂ (0, i) + FreeAlgebra.ι ℂ (1, i) := by
  simp [toConstDestAlgebra]

lemma toConstDestAlgebra_single (x : ℂ) : (l : FreeMonoid (index S)) →
    toConstDestAlgebra (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
    = ∑ (f : Fin l.length → Fin 2), FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
      (MonoidAlgebra.single (listToConstDestList l f) x)
  | [] => by
    simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_nil, Finset.univ_unique,
      listToConstDestList, Finset.sum_const, Finset.card_singleton, one_smul]
    trans x • 1
    · trans toConstDestAlgebra (x • 1)
      · congr
        simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
          FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
          AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
        rfl
      · simp only [toConstDestAlgebra, Fin.isValue, map_smul, map_one]
    · simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, FreeMonoid.lift,
      FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk, AlgEquiv.ofAlgHom_symm_apply,
      MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
      rfl
  | i :: l => by
    simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_cons, listToConstDestList,
      Fin.zero_eta, Prod.mk.eta]
    have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single (i :: l) x) =
      (FreeAlgebra.ι ℂ i) *
      (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single l x)) := by
      simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
        AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
      congr
      simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
        MonoidHom.coe_mk, OneHom.coe_mk]
      change List.foldl (fun x1 x2 => x1 * x2)
        (FreeAlgebra.ι ℂ i) (List.map (FreeAlgebra.ι ℂ) l) = _
      match l with
      | [] =>
        simp only [List.map_nil, List.foldl_nil, ne_eq, FreeAlgebra.ι_ne_zero, not_false_eq_true,
          left_eq_mul₀]
        rfl
      | x :: l =>
        simp only [List.map_cons, List.foldl_cons]
        change _ = FreeAlgebra.ι ℂ i * List.foldl (fun x1 x2 => x1 * x2) _ _
        rw [List.foldl_assoc]
    rw [h1]
    rw [map_mul]
    trans ∑ f : Fin (l.length + 1) → Fin 2, (FreeAlgebra.ι ℂ ((f 0, i)) : ConstDestAlgebra S) *
      (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
      (Finsupp.single (listToConstDestList l (f ∘ Fin.succ)) x) : ConstDestAlgebra S)
    · rw [← (Fin.consEquiv (n := l.length) (fun _ => Fin 2)).sum_comp
        (α := FreeAlgebra ℂ (ConstDestAlgebra.index S))]
      erw [Finset.sum_product]
      simp only [toConstDestAlgebra_ι, Fin.isValue, Fin.consEquiv_apply, Fin.cons_zero,
        Fin.sum_univ_two]
      rw [← Finset.mul_sum, ← Finset.mul_sum]
      erw [← toConstDestAlgebra_single]
      rw [add_mul]
    · congr
      funext f
      simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
        AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
      congr
      simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
        MonoidHom.coe_mk, OneHom.coe_mk]
      match l with
      | [] =>
        simp only [listToConstDestList]
        change FreeAlgebra.ι ℂ (f 0, i) * 1 = _
        simp only [mul_one]
        rfl
      | x :: l =>
        simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Function.comp_apply,
          Fin.succ_zero_eq_one, Prod.mk.eta]
        change FreeAlgebra.ι ℂ (f 0, i) * List.foldl _ _ _ = List.foldl _ _ _
        simp only [List.map_cons, List.foldl_cons]
        haveI : Std.Associative fun
          (x1 x2 : FreeAlgebra ℂ (ConstDestAlgebra.index S)) => x1 * x2 := by
          exact Semigroup.to_isAssociative
        refine Eq.symm List.foldl_assoc

lemma toWickAlgebra_factor_toConstDestAlgebra :
    toWickAlgebra 𝓞 = (ConstDestAlgebra.toWickAlgebra 𝓞).comp toConstDestAlgebra := by
  refine FreeAlgebra.hom_ext ?_
  funext i
  simp only [Function.comp_apply, toWickAlgebra_ι, ConstDestAlgebra.toWickAlgebra, AlgHom.coe_comp,
    toConstDestAlgebra_ι, Fin.isValue, map_add, FreeAlgebra.lift_ι_apply]
  split
  rename_i x i_1 f x_1 heq
  simp_all only [Fin.isValue, Prod.mk.injEq]
  obtain ⟨left, right⟩ := heq
  subst left right
  exact Eq.symm (𝓞.ψc_ψd f x_1)

/-- Time ordering fields and then mapping to constructive and destructive fields is the same as
  mapping to constructive and destructive fields and then time ordering. -/
lemma timeOrder_comm_toConstDestAlgebra (q : index S → Fin 2) :
    (ConstDestAlgebra.timeOrder (fun i => q i.2)).comp toConstDestAlgebra.toLinearMap =
    toConstDestAlgebra.toLinearMap.comp (timeOrder q) := by
  let e : S.FieldAlgebra ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid (index S)) :=
    FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
  apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
  apply MonoidAlgebra.lhom_ext'
  intro l
  apply LinearMap.ext
  intro x
  simp only [AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_toLinearMap, LinearMap.coe_comp,
    Function.comp_apply, MonoidAlgebra.lsingle_apply, AlgEquiv.toLinearMap_apply,
    AlgHom.toLinearMap_apply, toConstDestAlgebra_single, map_sum, timeOrder, koszulOrder_single, e]
  simp only [FreeMonoid.length]
  let ew := Equiv.piCongrLeft' (fun _ => Fin 2)
    (HepLean.List.insertionSortEquiv (timeOrderRel) l)
  rw [← ew.sum_comp (α := FreeAlgebra ℂ (ConstDestAlgebra.index S))]
  congr
  funext f
  simp only [ConstDestAlgebra.timeOrder, koszulOrder_single, EmbeddingLike.apply_eq_iff_eq]
  congr 1
  · rw [listToConstDestList_timeOrder]
    simp only [ew]
    rfl
  · simp only [mul_eq_mul_right_iff]
    exact Or.inl (listToConstDestList_koszulSign q l f)

end FieldAlgebra

end Species

informal_definition asymptoicContract where
  math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator [φd(i), ψ(j)]."
  ref :≈ "See e.g. http://www.dylanjtemples.com:82/solutions/QFT_Solution_I-6.pdf"

informal_definition contractAsymptotic where
  math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator [ψ(i), φc(j)]."

informal_definition asymptoicContractAsymptotic where
  math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator
    [φd(i), φc(j)]."

informal_lemma contraction_in_center where
  math :≈ "The contraction of two fields is in the center of the algebra."
  deps :≈ [``WickAlgebra]

informal_lemma contraction_non_dual_is_zero where
  math :≈ "The contraction of two fields is zero if the fields are not dual to each other."
  deps :≈ [``WickAlgebra]

informal_lemma timeOrder_single where
  math :≈ "The time ordering of a single field is the normal ordering of that field."
  proof :≈ "Follows from the definitions."
  deps :≈ [``WickAlgebra]

informal_lemma timeOrder_pair where
  math :≈ "The time ordering of two fields is the normal ordering of the fields plus the
    contraction of the fields."
  proof :≈ "Follows from the definition of contraction."
  deps :≈ [``WickAlgebra]

informal_definition WickMap where
  math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
    `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
  physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
    the necessary properties for lots of theorems to hold."
  deps :≈ [``WickAlgebra]

informal_lemma normalOrder_wickMap where
  math :≈ "Any normal ordering maps to zero under a Wick map."
  deps :≈ [``WickMap]

end Wick