refactor: Split files

HepLean/Mathematics/List.lean

@@ -142,4 +142,16 @@ lemma insertionSort_eq_ofFn {α : Type} {r : α → α → Prop} [DecidableRel r
   rw [insertionSortEquiv_get (r := r)]
   exact Eq.symm (List.ofFn_get (List.insertionSort r l))
 
+lemma insertionSort_eraseIdx {α : Type} {r : α → α → Prop} [DecidableRel r] :
+    (l : List α) →
+    (i : Fin (List.insertionSort r l).length) →
+    List.eraseIdx (List.insertionSort r l) i =
+    List.insertionSort r (List.eraseIdx l ((insertionSortEquiv r l).symm i))
+  | [], i => by
+    simp
+  | a :: l, i => by
+    rw [insertionSortEquiv]
+    simp
+
+
 end HepLean.List

HepLean/PerturbationTheory/Wick/Koszul/Contraction.lean

@@ -0,0 +1,215 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.OperatorMap
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
+  match i with
+  | none => l
+  | some i => List.eraseIdx l i
+
+inductive ContractionsAux {I : Type} : (l : List I) → (aux : List I) → Type
+  | nil : ContractionsAux [] []
+  | single {a : I} : ContractionsAux [a] [a]
+  | cons {l : List I} {aux : List I} {a b: I} (i : Option (Fin (b :: aux).length)) :
+    ContractionsAux (b :: l) aux → ContractionsAux (a :: b :: l) (optionErase (b :: aux) i)
+
+def Contractions {I : Type} (l : List I) : Type := Σ aux, ContractionsAux l aux
+
+namespace Contractions
+
+variable {I : Type} {l : List I} (c : Contractions l)
+
+def normalize : List I := c.1
+
+lemma normalize_length_le : c.normalize.length ≤ l.length := by
+  cases c
+  rename_i aux c
+  induction c with
+  | nil =>
+    simp [normalize]
+  | single =>
+    simp [normalize]
+  | cons i c ih =>
+    simp [normalize, optionErase]
+    match i with
+    | none =>
+      simpa using ih
+    | some i =>
+      simp
+      rw [List.length_eraseIdx]
+      simp [normalize] at ih
+      simp
+      exact Nat.le_add_right_of_le ih
+
+lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], ContractionsAux.nil⟩ := by
+  cases a
+  rename_i aux c
+  cases c
+  rfl
+
+lemma contractions_single {i : I} (a : Contractions [i]) : a = ⟨[i], ContractionsAux.single⟩ := by
+  cases a
+  rename_i aux c
+  cases c
+  rfl
+
+def consConsEquiv {a b : I} {l : List I} :
+    Contractions (a :: b :: l) ≃ (c : Contractions (b :: l)) × Option (Fin (b :: c.normalize).length) where
+  toFun c :=
+    match c with
+    | ⟨aux, c⟩ =>
+    match c with
+    | ContractionsAux.cons (aux := aux') i c => ⟨⟨aux', c⟩, i⟩
+  invFun ci :=
+    ⟨(optionErase (b :: ci.fst.normalize) ci.2), ContractionsAux.cons (a := a) ci.2 ci.1.2⟩
+  left_inv c := by
+    match c with
+    | ⟨aux, c⟩ =>
+    match c with
+    | ContractionsAux.cons (aux := aux') i c => rfl
+  right_inv ci := by rfl
+
+instance decidable : (l : List I) → DecidableEq (Contractions l)
+  | [] => fun a b =>
+    match a, b with
+    | ⟨_, a⟩, ⟨_, b⟩ =>
+    match a, b with
+    | ContractionsAux.nil , ContractionsAux.nil => isTrue rfl
+  | _ :: [] => fun a b =>
+    match a, b with
+    | ⟨_, a⟩, ⟨_, b⟩ =>
+    match a, b with
+    | ContractionsAux.single , ContractionsAux.single => isTrue rfl
+  | _ :: b :: l =>
+    haveI : DecidableEq (Contractions (b :: l)) := decidable (b :: l)
+    haveI : DecidableEq ((c : Contractions (b :: l)) × Option (Fin (b :: c.normalize).length)) :=
+      Sigma.instDecidableEqSigma
+    Equiv.decidableEq consConsEquiv
+
+instance fintype  : (l : List I) → Fintype (Contractions l)
+  | [] => {
+    elems := {⟨[], ContractionsAux.nil⟩}
+    complete := by
+      intro a
+      rw [Finset.mem_singleton]
+      exact contractions_nil a}
+  | a :: [] => {
+    elems := {⟨[a], ContractionsAux.single⟩}
+    complete := by
+      intro a
+      rw [Finset.mem_singleton]
+      exact contractions_single a}
+  | a :: b :: l =>
+    haveI : Fintype (Contractions (b :: l)) := fintype (b :: l)
+    haveI : Fintype ((c : Contractions (b :: l)) × Option (Fin (b :: c.normalize).length)) :=
+      Sigma.instFintype
+    Fintype.ofEquiv _ consConsEquiv.symm
+
+-- This definition is not correct.
+def superCommuteTermAux {l : List I} {aux : List I} : (c : ContractionsAux l aux)  → FreeAlgebra ℂ I
+  | ContractionsAux.nil => 1
+  | ContractionsAux.single => 1
+  | ContractionsAux.cons i c => superCommuteTermAux c
+
+def superCommuteTerm {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    {r : List I} (c : Contractions r) : FreeAlgebra ℂ (Σ i, f i) :=
+    freeAlgebraMap f (superCommuteTermAux c.2)
+
+lemma superCommuteTerm_center {f : I → Type} [∀ i, Fintype (f i)]
+    {A : Type} [Semiring A] [Algebra ℂ A]
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [SuperCommuteCenterMap F] :
+    F (c.superCommuteTerm) ∈ Subalgebra.center ℂ A := by
+  sorry
+
+def toTerm {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) {r : List I}
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    (c : Contractions r) : FreeAlgebra ℂ (Σ i, f i) :=
+  c.superCommuteTerm * koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)
+
+lemma toTerm_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+     : toTerm q le1 (⟨[], ContractionsAux.nil⟩ : Contractions [])  = 1 := by
+  simp [toTerm, normalize]
+  rw [ofListM_empty]
+  simp
+  sorry
+
+end Contractions
+
+lemma wick_cons_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (r : List I)
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    (tle : I → I → Prop) [DecidableRel tle]
+    (i : (Σ i, f i)) (hi : ∀ j, le1 j i)
+    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I) (b a : I)
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [SuperCommuteCenterMap F]
+    (bn bp : (Σ i, f i))
+    (hb : ofListM f [b] 1 = ofList [bn] 1 + ofList [bp] 1)
+    (ih : F (ofListM f (a :: r) 1) = ∑ c : Contractions (a :: r), F (c.toTerm q le1)) :
+    F (ofListM f (b :: a :: r) 1) =  ∑ c : Contractions (b :: a :: r),  F (c.toTerm q le1)  := by
+  rw [ofListM_cons_eq_ofListM, map_mul]
+  rw [ih]
+  rw [Finset.mul_sum]
+  rw  [← Contractions.consConsEquiv.symm.sum_comp]
+  simp
+  erw [Finset.sum_sigma]
+  congr
+  funext c
+  rw [Contractions.toTerm]
+  rw [map_mul, ← mul_assoc]
+  have hi := c.superCommuteTerm_center F
+  rw [Subalgebra.mem_center_iff] at hi
+  rw [hi]
+  rw [mul_assoc]
+  rw [← map_mul]
+  rw [hb]
+  rw [add_mul]
+  rw [ofList_singleton, mul_koszulOrder_le, ← ofList_singleton]
+  rw [map_add]
+  conv_lhs =>
+    rhs
+    rhs
+    rw [ofList_singleton]
+  rw [le_all_mul_koszulOrder]
+  rw [← add_assoc]
+  rw [← map_add, ← map_add]
+  conv_lhs =>
+    rhs
+    rw [← map_add]
+    rw [← add_mul]
+    rw [← ofList_singleton]
+    rw [← hb]
+    rw [map_add]
+  rw [mul_add]
+  conv_lhs =>
+    rhs
+    rw [superCommute_ofList_ofListM_sum]
+
+  sorry
+
+
+
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/Grade.lean

@@ -0,0 +1,86 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.Order
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
+  | [] => 0
+  | a :: l => if q a = grade q l then 0 else 1
+
+@[simp]
+lemma grade_freeMonoid  {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
+  simp only [grade, Fin.isValue]
+  have ha (a : Fin 2) : (if a = 0 then 0 else 1) = a := by
+    fin_cases a <;> rfl
+  rw [ha]
+
+@[simp]
+lemma grade_empty {I : Type} (q : I → Fin 2) : grade q [] = 0 := by
+  simp [grade]
+
+@[simp]
+lemma grade_append {I : Type} (q : I → Fin 2) (l r : List I) :
+    grade q (l ++ r) = if grade q l = grade q r then 0 else 1 := by
+  induction l with
+  | nil =>
+    simp only [List.nil_append, grade_empty, Fin.isValue]
+    have ha (a : Fin 2) : (if 0 = a then 0 else 1) = a := by
+      fin_cases a <;> rfl
+    exact Eq.symm (Fin.eq_of_val_eq (congrArg Fin.val (ha (grade q r))))
+  | cons a l ih =>
+    simp only [grade, List.append_eq, Fin.isValue]
+    erw [ih]
+    have hab (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
+         if (if a = b then 0 else 1) = c then 0 else 1 := by
+      fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
+    exact hab (q a) (grade q l) (grade q r)
+
+lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (l : List I) ( i : I ) :
+    grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
+  induction l with
+  | nil => simp
+  | cons j l ih =>
+    simp
+    by_cases hij : le1 i j
+    · simp [hij]
+    · simp [hij]
+      rw [grade]
+      rw [ih]
+      simp [grade]
+      have h1 (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) = if b = if a = c then 0 else 1 then 0 else 1 := by
+        fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
+      exact h1 _ _ _
+
+@[simp]
+lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (l : List I) :
+    grade q (List.insertionSort le1 l) = grade q l := by
+  induction l with
+  | nil => simp
+  | cons j l ih =>
+    simp [grade]
+    rw [grade_orderedInsert]
+    simp [grade]
+    rw [ih]
+
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/OfList.lean

@@ -0,0 +1,408 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.Grade
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+def ofList {I : Type} (l : List I) (x : ℂ) : FreeAlgebra ℂ I :=
+  FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
+
+lemma ofList_pair {I : Type} (l r : List I) (x y : ℂ) :
+    ofList (l ++ r) (x * y) = ofList l x * ofList r y := by
+  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, EmbeddingLike.apply_eq_iff_eq]
+  rfl
+
+lemma ofList_triple {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
+    ofList (la ++ lb ++ lc) (xa * xb * xc) = ofList la xa * ofList lb xb * ofList lc xc := by
+  rw [ofList_pair, ofList_pair]
+
+lemma ofList_triple_assoc {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
+    ofList (la ++ (lb ++ lc)) (xa * (xb * xc)) = ofList la xa * ofList lb xb * ofList lc xc := by
+  rw [ofList_pair, ofList_pair]
+  exact Eq.symm (mul_assoc (ofList la xa) (ofList lb xb) (ofList lc xc))
+
+lemma ofList_cons_eq_ofList {I : Type} (l : List I) (i : I) (x : ℂ) :
+    ofList (i :: l) x = ofList [i] 1 * ofList l x := by
+  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, one_mul,
+    EmbeddingLike.apply_eq_iff_eq]
+  rfl
+
+lemma ofList_singleton {I : Type} (i : I) :
+    ofList [i] 1 = FreeAlgebra.ι ℂ i := by
+  simp only [ofList, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+    MonoidAlgebra.single, AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+  rfl
+
+lemma ofList_eq_smul_one {I : Type} (l : List I) (x : ℂ) :
+    ofList l x = x • ofList l 1 := by
+  simp only [ofList]
+  rw [← map_smul]
+  simp
+
+lemma ofList_empty {I : Type} : ofList [] 1 = (1 : FreeAlgebra ℂ I) := by
+  simp only [ofList, EmbeddingLike.map_eq_one_iff]
+  rfl
+
+lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra ℂ I) := by
+  rw [ofList_eq_smul_one, ofList_empty]
+
+
+lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (l : List I) (x : ℂ) :
+    koszulOrder r q (ofList l x) = (koszulSign r q l) • ofList (List.insertionSort r l) x := by
+  rw [ofList]
+  rw [koszulOrder_single]
+  change ofList (List.insertionSort r l) _ = _
+  rw [ofList_eq_smul_one]
+  conv_rhs => rw [ofList_eq_smul_one]
+  rw [smul_smul]
+
+def freeAlgebraMap {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
+    FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
+  FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
+
+lemma freeAlgebraMap_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)  :
+    freeAlgebraMap f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
+  simp [freeAlgebraMap]
+
+def ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ℂ) :
+    FreeAlgebra ℂ (Σ i, f i) :=
+  freeAlgebraMap f (ofList l x)
+
+lemma ofListM_empty  {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
+  ofListM f [] 1 = 1 := by
+  simp only [ofListM, EmbeddingLike.map_eq_one_iff]
+  rw [ofList_empty]
+  exact map_one (freeAlgebraMap f)
+
+lemma ofListM_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I)  (x : ℂ) :
+    ofListM f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩) * (ofListM f r x) := by
+  rw [ofListM, ofList_cons_eq_ofList, ofList_singleton, map_mul]
+  conv_lhs => lhs; rw [freeAlgebraMap]
+  rw [ofListM]
+  simp
+
+lemma ofListM_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (x : ℂ) :
+    ofListM f [i] x = ∑ j : f i, x • FreeAlgebra.ι ℂ ⟨i, j⟩ := by
+  simp only [ofListM]
+  rw [ofList_eq_smul_one, ofList_singleton, map_smul]
+  rw [freeAlgebraMap_ι]
+  rw [Finset.smul_sum]
+
+lemma ofListM_cons_eq_ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I)  (x : ℂ) :
+    ofListM f (i :: r) x = ofListM f [i] 1 * ofListM f r x  := by
+  rw [ofListM_cons, ofListM_singleton]
+  simp only [one_smul]
+
+def liftM {I : Type} (f : I → Type) [∀ i, Fintype (f i)]  :
+    (l : List I) →  (a : Π i, f (l.get i)) →  List (Σ i, f i)
+  | [], _ => []
+  | i :: l, a => ⟨i, a ⟨0, Nat.zero_lt_succ l.length⟩⟩ :: liftM f l (fun i => a (Fin.succ i))
+
+@[simp]
+lemma liftM_length {I : Type} (f : I → Type) [∀ i, Fintype (f i)]  (r : List I) (a : Π i, f (r.get i)) :
+    (liftM f r a).length = r.length := by
+  induction r with
+  | nil => rfl
+  | cons i r ih =>
+    simp only [liftM, List.length_cons, Fin.zero_eta, add_left_inj]
+    rw [ih]
+
+lemma liftM_get {I : Type} (f : I → Type) [∀ i, Fintype (f i)]  (r : List I) (a : Π i, f (r.get i)) :
+    (liftM f r a).get = (fun i => ⟨r.get i, a i⟩) ∘ Fin.cast (by simp) := by
+  induction r with
+  | nil =>
+    funext i
+    exact Fin.elim0 i
+  | cons i l ih =>
+    simp only [liftM, 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 (liftM f _ _).get _ = _
+      rw [ih]
+      simp
+
+lemma ofListM_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)]  (x : ℂ) :
+    (l : List I) → ofListM f l x = ∑ (a : Π i, f (l.get i)), ofList (liftM f l a) x
+  | [] => by
+    simp only [ofListM, List.length_nil, List.get_eq_getElem, Finset.univ_unique, liftM,
+      Finset.sum_const, Finset.card_singleton, one_smul]
+    rw [ofList_eq_smul_one, map_smul, ofList_empty, ofList_eq_smul_one, ofList_empty, map_one]
+  | i :: l => by
+    rw [ofListM_cons, ofListM_expand f x l]
+    let e1 :  f i × (Π j, f (l.get j)) ≃ (Π j, f ((i :: l).get j)) :=
+      (Fin.insertNthEquiv (fun j => f ((i :: l).get j)) 0)
+    rw [← e1.sum_comp (α := FreeAlgebra ℂ _)]
+    erw [Finset.sum_product]
+    rw [Finset.sum_mul]
+    conv_lhs =>
+      rhs
+      intro n
+      rw [Finset.mul_sum]
+    congr
+    funext j
+    congr
+    funext n
+    rw [← ofList_singleton, ← ofList_pair, one_mul]
+    rfl
+
+
+@[simp]
+lemma liftM_grade {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (r : List I) (a : Π i, f (r.get i))  :
+    grade (fun i => q i.fst) (liftM f r a) = 1 ↔ grade q r = 1 := by
+  induction r with
+  | nil =>
+    simp [liftM]
+  | cons i r ih =>
+    simp only [grade, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
+    have ih' := ih (fun i => a i.succ)
+    have h1 : grade (fun i => q i.fst) (liftM f r fun i => a i.succ) = grade q r  := by
+      by_cases h : grade q r = 1
+      · simp_all
+      · have h0 : grade q r = 0 := by
+          omega
+        rw [h0] at ih'
+        simp only [Fin.isValue, zero_ne_one, iff_false] at ih'
+        have h0' : grade (fun i => q i.fst) (liftM f r fun i => a i.succ)  = 0 := by
+          omega
+        rw [h0, h0']
+    rw [h1]
+
+lemma liftM_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) : (r : List I) →  (a : Π i, f (r.get i)) → (n : ℕ) →
+    grade (fun i => q i.fst) (List.take n (liftM f r a)) = grade q (List.take n r)
+  | [], _, _ => by
+    simp [liftM]
+  | i :: r, a, 0 => by
+    simp
+  | i :: r, a, Nat.succ n => by
+    simp only [grade, Fin.isValue]
+    have ih : grade (fun i => q i.fst) (List.take n (liftM f r fun i => a i.succ))  = grade q (List.take n r) := by
+      refine (liftM_grade_take q r (fun i => a i.succ) n)
+    rw [ih]
+
+
+lemma koszulSignInsert_liftM  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (a : (j : Fin l.length) → f (l.get j)) (x : (i : I) × f i):
+    koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x
+      (liftM f l a)  =
+    koszulSignInsert le1 q x.1 l := by
+  induction l with
+  | nil => simp [koszulSignInsert]
+  | cons b l ih =>
+    simp [koszulSignInsert]
+    rw [ih]
+
+lemma koszulSign_liftM  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (a : (i : Fin l.length) → f (l.get i)) :
+    koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) (liftM f l a) =
+    koszulSign le1 q l := by
+  induction l with
+  | nil => simp [koszulSign]
+  | cons i l ih =>
+    simp [koszulSign, liftM]
+    rw [ih]
+    congr 1
+    rw [koszulSignInsert_liftM]
+
+lemma insertionSortEquiv_liftM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (le1 : I → I → Prop) [DecidableRel le1](l : List I)  (a : (i : Fin l.length) → f (l.get i))  :
+    (HepLean.List.insertionSortEquiv (fun i j => le1 i.fst j.fst) (liftM f l a)) =
+    (Fin.castOrderIso (by simp)).toEquiv.trans ((HepLean.List.insertionSortEquiv le1 l).trans
+    (Fin.castOrderIso (by simp)).toEquiv) := by
+  induction l with
+  | nil =>
+    simp [liftM, HepLean.List.insertionSortEquiv]
+  | cons i l ih =>
+    simp only [liftM, List.length_cons, Fin.zero_eta, List.insertionSort]
+    conv_lhs => simp [HepLean.List.insertionSortEquiv]
+    have h1 (l' : List (Σ i, f i)) :
+        (HepLean.List.insertEquiv  (fun i j => le1 i.fst j.fst) ⟨i, a ⟨0, by simp⟩⟩ l') =
+        (Fin.castOrderIso (by simp)).toEquiv.trans
+        ((HepLean.List.insertEquiv le1 i (List.map (fun i => i.1) l')).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 : (fun (i j : Σ i, f i) => le1 i.fst j.fst) ⟨i, a ⟨0, by simp⟩⟩  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 : Σ i, f i) (l' : List ( Σ i, f i)) :
+      List.map (fun i => i.1) (List.orderedInsert (fun i j => le1 i.fst j.fst) i l') =
+      List.orderedInsert le1 i.1 (List.map (fun i => i.1) l') := by
+      induction l' with
+      | nil =>
+        simp [HepLean.List.insertEquiv]
+      | cons j l' ih' =>
+        by_cases hij : (fun i j => le1 i.fst j.fst)  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 : ¬ le1 i.1 j.1 := hij
+          simp only [hn, ↓reduceIte, List.cons.injEq, true_and]
+          simpa using ih'
+    have h2 (l' : List ( Σ i, f i)) :
+        List.map (fun i => i.1) (List.insertionSort (fun i j => le1 i.fst j.fst) l') =
+        List.insertionSort le1 (List.map (fun i => i.1) l') := 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
+    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 le1 (List.map (fun i => i.1) (liftM f l (fun i => a i.succ)))) =
+      List.insertionSort le1 l := by
+      congr
+      have h3' (l : List I) (a : Π (i : Fin l.length), f (l.get i)) :
+        List.map (fun i => i.1) (liftM f l a) = l := by
+        induction l with
+        | nil => rfl
+        | cons i l ih' =>
+          simp only [liftM, List.length_cons, Fin.zero_eta, Prod.mk.eta,
+            List.unzip_snd, List.map_cons, List.cons.injEq, true_and]
+          simpa using ih' _
+      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]
+
+lemma insertionSort_liftM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (le1 : I → I → Prop) [DecidableRel le1](l : List I)  (a : (i : Fin l.length) → f (l.get i))
+    :
+    List.insertionSort (fun i j => le1 i.fst j.fst) (liftM f l a) =
+    liftM f (List.insertionSort le1 l)
+    (Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
+      congr 1
+      rw [← HepLean.List.insertionSortEquiv_get]
+      simp))) a) := by
+  let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) (liftM f l a)
+  let l2 := liftM f (List.insertionSort le1 l)
+    (Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
+      congr 1
+      rw [← HepLean.List.insertionSortEquiv_get]
+      simp))) a)
+  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 [liftM_get, liftM_get]
+    funext i
+    rw [insertionSortEquiv_liftM]
+    simp only [ Function.comp_apply, Equiv.symm_trans_apply,
+      OrderIso.toEquiv_symm, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
+      Fin.cast_trans, Fin.cast_eq_self, id_eq, eq_mpr_eq_cast, Fin.coe_cast, Sigma.mk.inj_iff]
+    apply And.intro
+    · have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le1) l) (Fin.cast (by simp) i)
+      rw [← h1]
+      simp
+    · simp [Equiv.piCongr]
+      exact (cast_heq _ _).symm
+  apply List.ext_get hlen
+  rw [hget]
+  simp
+
+lemma koszulOrder_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListM f l x) =
+    freeAlgebraMap f (koszulOrder le1 q (ofList l x)) := by
+  rw [koszulOrder_ofList]
+  rw [map_smul]
+  change _ = _ • ofListM _ _ _
+  rw [ofListM_expand]
+  rw [map_sum]
+  conv_lhs =>
+    rhs
+    intro a
+    rw [koszulOrder_ofList]
+    rw [koszulSign_liftM]
+  rw [← Finset.smul_sum]
+  apply congrArg
+  conv_lhs =>
+    rhs
+    intro n
+    rw [insertionSort_liftM]
+  rw [ofListM_expand]
+  refine Fintype.sum_equiv ((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
+  congr 1
+  · rw [← HepLean.List.insertionSortEquiv_get]
+    simp
+  · intro x
+    rfl
+
+lemma koszulOrder_ofListM_eq_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListM f l x) =
+    koszulSign le1 q l • ofListM f (List.insertionSort le1 l) x := by
+  rw [koszulOrder_ofListM, koszulOrder_ofList, map_smul]
+  rfl
+
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/OperatorMap.lean

@@ -0,0 +1,194 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.SuperCommuteM
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+class SuperCommuteCenterMap {A :  Type} [Semiring A] [Algebra ℂ A]
+    (f : FreeAlgebra ℂ I →ₐ[ℂ] A) : Prop where
+  prop : ∀ i j, f (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) ∈ Subalgebra.center ℂ A
+
+namespace SuperCommuteCenterMap
+
+variable {I : Type}  {A :  Type} [Semiring A] [Algebra ℂ A]
+    (f : FreeAlgebra ℂ I →ₐ[ℂ] A) [SuperCommuteCenterMap f]
+
+lemma ofList_fst (q : I → Fin 2) (i j : I) :
+    f (superCommute q (ofList [i] xa) (FreeAlgebra.ι ℂ j)) ∈ Subalgebra.center ℂ A := by
+  have h1 : f (superCommute q (ofList [i] xa) (FreeAlgebra.ι ℂ j)) =
+      xa • f (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) := by
+    rw [← map_smul]
+    congr
+    rw [ofList_eq_smul_one, ofList_singleton]
+    rw [map_smul]
+    rfl
+  rw [h1]
+  refine Subalgebra.smul_mem (Subalgebra.center ℂ A) ?_ xa
+  exact prop i j
+
+lemma ofList_freeAlgebraMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (c :  (Σ i, f i))  (x  : ℂ)
+    {A :  Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
+    [SuperCommuteCenterMap F] (b : I) :
+    F ((superCommute fun i => q i.fst) (ofList [c] x) ((freeAlgebraMap f) (FreeAlgebra.ι ℂ b)))
+    ∈ Subalgebra.center ℂ A := by
+  rw [freeAlgebraMap_ι]
+  rw [map_sum, map_sum]
+  refine Subalgebra.sum_mem (Subalgebra.center ℂ A) ?h
+  intro n hn
+  exact ofList_fst F (fun i => q i.fst) c ⟨b, n⟩
+
+end SuperCommuteCenterMap
+
+lemma superCommuteTake_superCommuteCenterMap {I : Type} (q : I → Fin 2) (lb : List I) (xa xb : ℂ) (n : ℕ)
+    (hn : n < lb.length) {A :  Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ I →ₐ[ℂ] A)
+    [SuperCommuteCenterMap f] (i : I) :
+    f (superCommuteTake q [i] lb xa xb n hn) =
+    f (superCommute q (ofList [i] xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩)))
+    * (superCommuteCoef q [i] (List.take n lb) •
+    f (ofList (List.eraseIdx lb n) xb)) := by
+  have hn : f ((superCommute q) (ofList [i] xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩))) ∈
+    Subalgebra.center ℂ A := SuperCommuteCenterMap.ofList_fst f q i (lb.get ⟨n, hn⟩)
+  rw [Subalgebra.mem_center_iff] at hn
+  rw [superCommuteTake, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
+    ← map_mul, ← ofList_pair]
+  congr
+  · exact Eq.symm (List.eraseIdx_eq_take_drop_succ lb n)
+  · exact one_mul xb
+
+
+lemma superCommuteTakeM_F {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (c :  (Σ i, f i)) (r : List I) (x y : ℂ)  (n : ℕ)
+    (hn : n < r.length)
+    {A :  Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
+    [SuperCommuteCenterMap F] :
+    F (superCommuteTakeM q [c] r x y n hn) = superCommuteCoefM q [c] (List.take n r) •
+    (F (superCommute (fun i => q i.1) (ofList [c] x) (freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
+    * F (ofListM f (List.eraseIdx r n) y)) := by
+  rw [superCommuteTakeM]
+  rw [map_smul]
+  congr
+  rw [map_mul, map_mul]
+  have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((freeAlgebraMap f) (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
+    ∈ Subalgebra.center ℂ A :=
+      SuperCommuteCenterMap.ofList_freeAlgebraMap q c x F (r.get ⟨n, hn⟩)
+  rw [Subalgebra.mem_center_iff] at h1
+  rw [h1, mul_assoc, ← map_mul]
+  congr
+  rw [ofListM, ofListM, ofListM, ← map_mul]
+  congr
+  rw [← ofList_pair, one_mul]
+  congr
+  exact Eq.symm (List.eraseIdx_eq_take_drop_succ r n)
+
+
+lemma koszulOrder_superCommuteM_le {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (r : List I) (x : ℂ)
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    (i : (Σ i, f i)) (hi : ∀ j, le1 j i)
+    {A : Type} [Semiring A] [Algebra ℂ A]
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [SuperCommuteCenterMap F] :
+    F (koszulOrder le1 (fun i => q i.fst)
+     (superCommute (fun i => q i.1) (FreeAlgebra.ι ℂ i) (ofListM f r x))) = 0 := by
+  sorry
+
+lemma koszulOrder_of_le_all {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (r : List I) (x : ℂ) (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    (i : (Σ i, f i)) (hi : ∀ j, le1 j i)
+    {A : Type} [Semiring A] [Algebra ℂ A]
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [SuperCommuteCenterMap F] :
+    F (koszulOrder le1 (fun i => q i.fst)
+    (ofListM f r x * FreeAlgebra.ι ℂ i))
+    = superCommuteCoefM q [i] r • F (koszulOrder le1 (fun i => q i.fst)
+      (FreeAlgebra.ι ℂ i * ofListM f r x)) := by
+  conv_lhs =>
+    rhs
+    rhs
+    rw [← ofList_singleton]
+    rw [ofListM_ofList_superCommute q]
+  rw [map_sub]
+  rw [sub_eq_add_neg]
+  rw [map_add]
+  conv_lhs =>
+    rhs
+    rhs
+    rw [map_smul]
+    rw [← neg_smul]
+  rw [map_smul, map_smul, map_smul]
+  rw [ofList_singleton, koszulOrder_superCommuteM_le]
+  · simp
+  · exact fun j => hi j
+
+lemma le_all_mul_koszulOrder {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (r : List I) (x : ℂ) (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    (i : (Σ i, f i)) (hi : ∀ j, le1 j i)
+    {A : Type} [Semiring A] [Algebra ℂ A]
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [SuperCommuteCenterMap F] :
+    F (FreeAlgebra.ι ℂ i * koszulOrder le1 (fun i => q i.fst)
+    (ofListM f r x)) = F ((koszulOrder le1 fun i => q i.fst) (FreeAlgebra.ι ℂ i * ofListM f r x)) +
+    F (((superCommute fun i => q i.fst) (ofList [i] 1))
+        ((koszulOrder le1 fun i => q i.fst) (ofListM f r x))) := by
+    sorry
+/-
+  rw [map_smul]
+  rw [Algebra.mul_smul_comm, map_smul]
+  change koszulSign le1 q r • F (FreeAlgebra.ι ℂ i * (ofListM f (List.insertionSort le1 r) x)) = _
+  rw [← ofList_singleton]
+  rw [ofList_ofListM_superCommute q]
+  rw [map_add]
+  rw [smul_add]
+  rw [← map_smul]
+  conv_lhs =>
+    lhs
+    rhs
+    rw [← Algebra.smul_mul_assoc]
+    rw [smul_smul, mul_comm, ← smul_smul]
+    rw [ ofListM, ← map_smul, ← koszulOrder_ofList, ← koszulOrder_ofListM, ofList_singleton]
+    rw [Algebra.smul_mul_assoc]
+  rw [koszulOrder_mul_ge]
+  rw [map_smul]
+  rw [koszulOrder_of_le_all]
+  rw [smul_smul]
+  have h1 : (superCommuteCoefM q [i] (List.insertionSort le1 r) * superCommuteCoefM q [i] r) = 1 := by
+    simp [superCommuteCoefM]
+    have ha (a b : Fin 2): (if a = 1 ∧ b = 1 then
+      -if a = 1 ∧ b = 1 then -1 else 1
+      else if a = 1 ∧ b = 1 then -1 else (1 : ℂ)) = 1 := by
+      fin_cases a <;> fin_cases b
+      · rfl
+      · rfl
+      · rfl
+      · simp only [Fin.mk_one, Fin.isValue, and_self, ↓reduceIte, neg_neg]
+    exact ha _ _
+  rw [h1]
+  simp only [one_smul]
+  conv_lhs =>
+    rhs
+    rw [← map_smul, ← map_smul]
+    rw [ ofListM, ← map_smul, ← koszulOrder_ofList, ← koszulOrder_ofListM]
+  congr
+  rw [ofList_singleton]
+  · exact fun j => hi j
+  · exact fun j => hi j.fst
+-/
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/Order.lean

@@ -0,0 +1,303 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+/-- 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))
+
+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
+
+@[simp]
+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]
+
+@[simp]
+lemma koszulOrder_ι_pair  {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i j : I) :
+    koszulOrder r q (FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j) =
+    if r i j then FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j else
+    (koszulSign r q [i, j]) • (FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i) := by
+  have h1 : FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j =
+    FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i, j] 1) := by
+    simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+      AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+    rfl
+  conv_lhs => rw [h1]
+  simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
+    LinearMap.coe_comp, Function.comp_apply, AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply,
+    koszulOrderMonoidAlgebra_single, List.insertionSort, List.orderedInsert,
+    MonoidAlgebra.smul_single', mul_one]
+  by_cases hr : r i j
+  · rw [if_pos hr, if_pos hr]
+    simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+      AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single]
+    have hKS : koszulSign r q [i, j] = 1 := by
+      simp only [koszulSign, koszulSignInsert, Fin.isValue, mul_one, ite_eq_left_iff,
+        ite_eq_right_iff, and_imp]
+      exact fun a a_1 a_2 => False.elim (a hr)
+    rw [hKS]
+    simp only [one_smul]
+    rfl
+  · rw [if_neg hr, if_neg hr]
+    simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+      AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single]
+    rfl
+
+@[simp]
+lemma koszulOrder_one  {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
+    koszulOrder r q 1 = 1 := by
+  trans koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
+  congr
+  · simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+    AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+    rfl
+  · simp only [koszulOrder_single, List.insertionSort, mul_one, EmbeddingLike.map_eq_one_iff]
+    rfl
+
+lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (i : I) (A : FreeAlgebra ℂ I) (hi : ∀ j, r i j) :
+    FreeAlgebra.ι ℂ i * koszulOrder r q A = koszulOrder r q (FreeAlgebra.ι ℂ i * A) := by
+  let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := {
+    toFun := fun x => FreeAlgebra.ι ℂ i * x,
+    map_add' := fun x y => by
+      simp [mul_add],
+    map_smul' := by simp}
+  change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) _
+  have f_single (l : FreeMonoid I) (x : ℂ) :
+      f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
+      = (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (i :: l) x)) := by
+    simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
+    have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i] 1) := by
+      simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+        AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+      rfl
+    rw [hf]
+    rw [@AlgEquiv.eq_symm_apply]
+    simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, one_mul]
+    rfl
+  have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
+    let e : FreeAlgebra ℂ I ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
+      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 [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
+      MonoidAlgebra.lsingle_apply]
+    erw [koszulOrder_single]
+    rw [f_single]
+    erw [f_single]
+    rw [koszulOrder_single]
+    congr 2
+    · simp only [List.insertionSort]
+      have hi (l : List I) : i :: l = List.orderedInsert r i l := by
+        induction l with
+        | nil => rfl
+        | cons j l ih =>
+          refine (List.orderedInsert_of_le r l (hi j)).symm
+      exact hi _
+    · congr 1
+      rw [koszulSign]
+      have h1 (l : List I) : koszulSignInsert r q i l = 1  := by
+        induction l with
+        | nil => rfl
+        | cons j l ih =>
+          simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
+          intro h
+          exact False.elim (h (hi j))
+      rw [h1]
+      simp
+  rw [h1]
+
+lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (i : I) (A : FreeAlgebra ℂ I) (hi : ∀ j, r j i) :
+    koszulOrder r q A * FreeAlgebra.ι ℂ i  = koszulOrder r q (A * FreeAlgebra.ι ℂ i) := by
+  let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := {
+    toFun := fun x => x * FreeAlgebra.ι ℂ i ,
+    map_add' := fun x y => by
+      simp [add_mul],
+    map_smul' := by simp}
+  change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) A
+  have f_single (l : FreeMonoid I) (x : ℂ) :
+      f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
+      = (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (l.toList ++ [i]) x)) := by
+    simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
+    have hf : FreeAlgebra.ι ℂ i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i] 1) := by
+      simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+        AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+      rfl
+    rw [hf]
+    rw [@AlgEquiv.eq_symm_apply]
+    simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, mul_one]
+    rfl
+  have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
+    let e : FreeAlgebra ℂ I ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
+      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 [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
+      MonoidAlgebra.lsingle_apply]
+    erw [koszulOrder_single]
+    rw [f_single]
+    erw [f_single]
+    rw [koszulOrder_single]
+    congr 3
+    · change (List.insertionSort r l) ++ [i] = List.insertionSort r (l.toList ++ [i])
+      have hoi (l : List I) (j : I) : List.orderedInsert r j (l ++ [i]) =
+          List.orderedInsert r j l ++ [i] := by
+        induction l with
+        | nil => simp [hi]
+        | cons b l ih =>
+          simp only [List.orderedInsert, List.append_eq]
+          by_cases hr : r j b
+          · rw [if_pos hr, if_pos hr]
+            rfl
+          · rw [if_neg hr, if_neg hr]
+            rw [ih]
+            rfl
+      have hI (l : List I) : (List.insertionSort r l) ++ [i] = List.insertionSort r (l ++ [i]) := by
+        induction l with
+        | nil => rfl
+        | cons j l ih =>
+          simp only [List.insertionSort, List.append_eq]
+          rw [← ih]
+          rw [hoi]
+      rw [hI]
+      rfl
+    · have hI (l : List I) : koszulSign r q l = koszulSign r q (l ++ [i]) := by
+        induction l with
+        | nil => simp [koszulSign, koszulSignInsert]
+        | cons j l ih =>
+          simp only [koszulSign, List.append_eq]
+          rw [ih]
+          simp only [mul_eq_mul_right_iff]
+          apply Or.inl
+          have hKI (l : List I) (j : I) : koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
+            induction l with
+            | nil => simp [koszulSignInsert, hi]
+            | cons b l ih =>
+              simp only [koszulSignInsert, Fin.isValue, List.append_eq]
+              by_cases hr : r j b
+              · rw [if_pos hr, if_pos hr]
+              · rw [if_neg hr, if_neg hr]
+                rw [ih]
+          rw [hKI]
+      rw [hI]
+      rfl
+  rw [h1]
+
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/SuperCommute.lean

@@ -0,0 +1,289 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.OfList
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
+    MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
+  Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid I)) ℂ (List I)
+    (fun r =>
+      Finsupp.lsingle (R := ℂ) (l ++ r) 1 +
+      if grade q l = 1 ∧ grade q r = 1 then
+        Finsupp.lsingle (R := ℂ) (r ++ l) 1
+      else
+        - Finsupp.lsingle (R := ℂ) (r ++ l) 1)
+
+def superCommuteAlgebra {I : Type} (q : I → Fin 2) :
+    MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
+  Finsupp.lift (FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I) ℂ (List I) fun l =>
+    (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
+    ∘ₗ superCommuteMonoidAlgebra q l
+    ∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap)
+
+def superCommute {I : Type} (q : I → Fin 2) :
+    FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
+  superCommuteAlgebra q
+  ∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
+
+lemma equivMonoidAlgebraFreeMonoid_freeAlgebra  {I : Type}  (i  : I) :
+    (FreeAlgebra.equivMonoidAlgebraFreeMonoid (FreeAlgebra.ι ℂ i)) = Finsupp.single (FreeMonoid.of i) 1  := by
+  simp [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.single]
+
+@[simp]
+lemma superCommute_ι {I : Type} (q : I → Fin 2)  (i j  : I)  :
+    superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) =
+    FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j +
+    if q i = 1 ∧ q j = 1 then
+      FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i
+    else
+      - FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i := by
+  simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
+    AlgEquiv.toAlgHom_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
+    AlgEquiv.toLinearMap_apply, equivMonoidAlgebraFreeMonoid_freeAlgebra, Fin.isValue, neg_mul]
+  erw [Finsupp.lift_apply]
+  simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, grade_freeMonoid,
+    zero_smul, Finsupp.sum_single_index, one_smul, LinearMap.coe_comp, Function.comp_apply,
+    AlgEquiv.toLinearMap_apply, equivMonoidAlgebraFreeMonoid_freeAlgebra]
+  conv_lhs =>
+    rhs
+    erw [Finsupp.lift_apply]
+  simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, Fin.isValue,
+    smul_add, MonoidAlgebra.smul_single', mul_one, smul_ite, smul_neg, Finsupp.sum_add,
+    Finsupp.single_zero, Finsupp.sum_single_index, grade_freeMonoid, neg_zero, ite_self,
+    AlgEquiv.ofAlgHom_symm_apply, map_add, MonoidAlgebra.lift_single, one_smul]
+  congr
+  by_cases hq : q i = 1 ∧ q j = 1
+  · rw [if_pos hq, if_pos hq]
+    simp only [MonoidAlgebra.lift_single, one_smul]
+    obtain ⟨left, right⟩ := hq
+    rfl
+  · rw [if_neg hq, if_neg hq]
+    simp only [map_neg, MonoidAlgebra.lift_single, one_smul, neg_inj]
+    rfl
+
+lemma superCommute_ofList_ofList  {I : Type} (q : I → Fin 2)  (l r  : List I) (x y : ℂ) :
+    superCommute q (ofList l x) (ofList r y) =
+    ofList (l ++ r) (x * y) + (if grade q l = 1 ∧ grade q r = 1 then
+    ofList (r ++ l) (y * x) else - ofList (r ++ l) (y * x)) := by
+  simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
+    AlgEquiv.toAlgHom_toLinearMap, ofList, LinearMap.coe_comp, Function.comp_apply,
+    AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, Fin.isValue]
+  erw [Finsupp.lift_apply]
+  simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, zero_smul,
+    Finsupp.sum_single_index, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply,
+    AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply]
+  conv_lhs =>
+    rhs
+    rhs
+    erw [Finsupp.lift_apply]
+  simp only [Fin.isValue, smul_add, MonoidAlgebra.smul_single', mul_one, smul_ite, smul_neg,
+    Finsupp.sum_add, Finsupp.single_zero, Finsupp.sum_single_index, neg_zero, ite_self, map_add]
+  by_cases hg : grade q l = 1 ∧ grade q r = 1
+  · simp only [hg, Fin.isValue, and_self, ↓reduceIte]
+    congr
+    · rw [← map_smul]
+      congr
+      exact MonoidAlgebra.smul_single' x (l ++ r) y
+    · rw [← map_smul]
+      congr
+      rw [mul_comm]
+      exact MonoidAlgebra.smul_single' x (r ++ l) y
+  · simp only [Fin.isValue, hg, ↓reduceIte, map_neg, smul_neg]
+    congr
+    · rw [← map_smul]
+      congr
+      exact MonoidAlgebra.smul_single' x (l ++ r) y
+    · rw [← map_smul]
+      congr
+      rw [mul_comm]
+      exact MonoidAlgebra.smul_single' x (r ++ l) y
+
+@[simp]
+lemma superCommute_zero {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
+    superCommute q a 0 = 0 := by
+  simp [superCommute]
+
+@[simp]
+lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
+    superCommute q a 1 = 0 := by
+  let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := (LinearMap.flip (superCommute q)) 1
+  have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1) = (1 : FreeAlgebra ℂ I) := by
+    simp_all only [EmbeddingLike.map_eq_one_iff]
+    rfl
+  have f_single (l : FreeMonoid I) (x : ℂ) :
+      f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
+      = 0 := by
+    simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
+      AlgEquiv.toAlgHom_toLinearMap, LinearMap.flip_apply, LinearMap.coe_comp, Function.comp_apply,
+      AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, f]
+    rw [← h1]
+    erw [Finsupp.lift_apply]
+    simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, zero_smul,
+      Finsupp.sum_single_index, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply,
+      AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, smul_eq_zero,
+      EmbeddingLike.map_eq_zero_iff]
+    apply Or.inr
+    conv_lhs =>
+      erw [Finsupp.lift_apply]
+    simp
+  have hf : f = 0 := by
+    let e : FreeAlgebra ℂ I ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
+      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 [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
+      MonoidAlgebra.lsingle_apply, LinearMap.zero_comp, LinearMap.zero_apply]
+    erw [f_single]
+  change f a = _
+  rw [hf]
+  simp
+
+def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : ℂ :=
+  if grade q la = 1 ∧ grade q lb = 1 then - 1 else  1
+
+lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
+    superCommuteCoef q la [] = 1 := by
+  simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
+
+lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc  : List I) :
+    superCommuteCoef q la (lb ++ lc) = superCommuteCoef q la lb * superCommuteCoef q la lc := by
+  simp only [superCommuteCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
+    mul_ite, mul_neg, mul_one]
+  by_cases hla : grade q la = 1
+  · by_cases hlb : grade q lb = 1
+    · by_cases hlc : grade q lc = 1
+      · simp [hlc, hlb, hla]
+      · have hc : grade q lc = 0 := by
+          omega
+        simp [hc, hlb, hla]
+    · have hb : grade q lb = 0 := by
+        omega
+      by_cases hlc : grade q lc = 1
+      · simp [hlc, hb]
+      · have hc : grade q lc = 0 := by
+          omega
+        simp [hc, hb]
+  · have ha : grade q la = 0 := by
+      omega
+    simp [ha]
+
+lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (xa xb xc : ℂ) :
+    superCommute q (ofList la xa) (ofList lb xb * ofList lc xc) =
+    (superCommute q (ofList la xa) (ofList lb xb) * ofList lc xc +
+    superCommuteCoef q la lb • ofList lb xb * superCommute q (ofList la xa) (ofList lc xc)) := by
+  simp only [Algebra.smul_mul_assoc]
+  conv_lhs => rw [← ofList_pair]
+  simp only [superCommute_ofList_ofList, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
+    imp_false]
+  simp only [superCommute_ofList_ofList, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
+    imp_false, ofList_triple_assoc, ofList_triple, ofList_pair, superCommuteCoef]
+  by_cases hla : grade q la = 1
+  · simp only [hla, Fin.isValue, true_and, ite_not, ite_smul, neg_smul, one_smul]
+    by_cases hlb : grade q lb = 1
+    · simp only [hlb, Fin.isValue, ↓reduceIte]
+      by_cases hlc : grade q lc = 1
+      · simp only [Fin.isValue, hlc, ↓reduceIte]
+        simp only [mul_assoc, add_mul, mul_add]
+        abel
+      · have hc : grade q lc  = 0 := by
+          omega
+        simp only [Fin.isValue, hc, one_ne_zero, ↓reduceIte, zero_ne_one]
+        simp only [mul_assoc, add_mul, mul_add, mul_neg, neg_add_rev, neg_neg]
+        abel
+    · have hb : grade q lb = 0 := by
+        omega
+      simp only [hb, Fin.isValue, zero_ne_one, ↓reduceIte]
+      by_cases hlc : grade q lc = 1
+      · simp only [Fin.isValue, hlc, zero_ne_one, ↓reduceIte]
+        simp only [mul_assoc, add_mul, neg_mul, mul_add]
+        abel
+      · have hc : grade q lc  = 0 := by
+          omega
+        simp only [Fin.isValue, hc, ↓reduceIte, zero_ne_one]
+        simp only [mul_assoc, add_mul, neg_mul, mul_add, mul_neg]
+        abel
+  · simp only [Fin.isValue, hla, false_and, ↓reduceIte, mul_assoc, add_mul, neg_mul, mul_add,
+    mul_neg, smul_add, one_smul, smul_neg]
+    abel
+
+def superCommuteTake {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
+  (hn : n < lb.length) : FreeAlgebra ℂ I :=
+  superCommuteCoef q la (List.take n lb) •
+  ofList (List.take n lb) 1 *
+  superCommute q (ofList la xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩))
+  * ofList (List.drop (n + 1) lb) xb
+
+lemma superCommute_ofList_cons {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (b1 : I) :
+    superCommute q (ofList la xa) (ofList (b1 :: lb) xb) =
+    superCommute q (ofList la xa) (FreeAlgebra.ι ℂ b1) * ofList lb xb +
+    superCommuteCoef q la [b1] •
+    (ofList [b1] 1) * superCommute q (ofList la xa) (ofList lb xb) := by
+  rw [ofList_cons_eq_ofList]
+  rw [superCommute_ofList_mul]
+  congr
+  · exact ofList_singleton b1
+
+lemma superCommute_ofList_sum  {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
+    superCommute q (ofList la xa) (ofList lb xb) =
+    ∑ (n : Fin lb.length), superCommuteTake q la lb xa xb n n.prop := by
+  induction lb with
+  | nil =>
+    simp only [superCommute_ofList_ofList, List.append_nil, Fin.isValue, grade_empty, zero_ne_one,
+      and_false, ↓reduceIte, List.nil_append, List.length_nil, Finset.univ_eq_empty,
+      Finset.sum_empty]
+    ring_nf
+    abel
+  | cons b lb ih =>
+    rw [superCommute_ofList_cons, ih]
+    have h0 :  ((superCommute q) (ofList la xa)) (FreeAlgebra.ι ℂ b) * ofList lb xb  =
+        superCommuteTake q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
+      simp [superCommuteTake, superCommuteCoef_empty, ofList_empty]
+    rw [h0]
+    have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ I) : ∑ n, f n =  f ⟨0,
+        Nat.zero_lt_succ lb.length⟩ + ∑ n, f (Fin.succ n) := by
+      exact Fin.sum_univ_succAbove f ⟨0, Nat.zero_lt_succ lb.length⟩
+    rw [hf]
+    congr
+    rw [Finset.mul_sum]
+    congr
+    funext n
+    simp only [superCommuteTake, Fin.eta, List.get_eq_getElem, Algebra.smul_mul_assoc,
+      Algebra.mul_smul_comm, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
+      List.getElem_cons_succ, List.drop_succ_cons]
+    congr 1
+    · rw [mul_comm, ← superCommuteCoef_append]
+      rfl
+    · simp only [← mul_assoc, mul_eq_mul_right_iff]
+      exact Or.inl (Or.inl (ofList_cons_eq_ofList (List.take (↑n) lb) b 1).symm)
+
+lemma koszulOrder_superCommute_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (i j : I) (hle : r i j) (a1 a2 : FreeAlgebra ℂ I) :
+    koszulOrder r q (a1 * superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) * a2) =
+    0 := by
+  sorry
+
+end
+end Wick

HepLean/PerturbationTheory/Wick/Koszul/SuperCommuteM.lean

@@ -0,0 +1,214 @@
+/-
+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
+import Mathlib.Data.Fin.Tuple.Take
+import HepLean.PerturbationTheory.Wick.Koszul.SuperCommute
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+lemma superCommute_ofList_ofListM  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
+    ofList l x * ofListM f r y +
+    (if grade (fun i => q i.1) l = 1 ∧ grade q r = 1 then
+    ofListM f r y * ofList l x else - ofListM f r y * ofList l x) := by
+  conv_lhs => rw [ofListM_expand]
+  rw [map_sum]
+  conv_rhs =>
+    lhs
+    rw [ofListM_expand, Finset.mul_sum]
+  conv_rhs =>
+    rhs
+    rhs
+    rw [ofListM_expand, ← Finset.sum_neg_distrib, Finset.sum_mul]
+  conv_rhs =>
+    rhs
+    lhs
+    rw [ofListM_expand, Finset.sum_mul]
+  rw [← Finset.sum_ite_irrel]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext a
+  rw [superCommute_ofList_ofList]
+  congr 1
+  · exact ofList_pair l (liftM f r a) x y
+  congr 1
+  · simp
+  · exact ofList_pair (liftM f r a) l y x
+  · rw [ofList_pair]
+    simp only [neg_mul]
+
+def superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : ℂ :=
+    (if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
+
+lemma superCommuteCoefM_empty  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)):
+    superCommuteCoefM q l [] = 1 := by
+  simp [superCommuteCoefM]
+
+lemma superCommute_ofList_ofListM_superCommuteCoefM  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
+    ofList l x * ofListM f r y - superCommuteCoefM q l r • ofListM f r y * ofList l x := by
+  rw [superCommute_ofList_ofListM, superCommuteCoefM]
+  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
+  · simp [hq]
+  · simp [hq]
+    abel
+
+lemma ofList_ofListM_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    ofList l x * ofListM f r y = superCommuteCoefM q l r • ofListM f r y * ofList l x
+    + superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
+  rw [superCommute_ofList_ofListM_superCommuteCoefM]
+  abel
+
+lemma ofListM_ofList_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+  ofListM f r y * ofList l x = superCommuteCoefM q l r • (ofList l x * ofListM f r y)
+    - superCommuteCoefM q l r • superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
+  rw [ofList_ofListM_superCommute, superCommuteCoefM]
+  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
+  · simp [hq]
+  · simp [hq]
+
+lemma superCommuteCoefM_append {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
+    superCommuteCoefM q l (r1 ++ r2) = superCommuteCoefM q l r1 * superCommuteCoefM q l r2 := by
+  simp only [superCommuteCoefM, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
+    mul_ite, mul_neg, mul_one]
+  by_cases hla : grade (fun i => q i.1) l = 1
+  · by_cases hlb : grade q r1 = 1
+    · by_cases hlc : grade q r2 = 1
+      · simp [hlc, hlb, hla]
+      · have hc : grade q r2 = 0 := by
+          omega
+        simp [hc, hlb, hla]
+    · have hb : grade q r1 = 0 := by
+        omega
+      by_cases hlc : grade q r2 = 1
+      · simp [hlc, hb]
+      · have hc : grade q r2 = 0 := by
+          omega
+        simp [hc, hb]
+  · have ha : grade (fun i => q i.1) l = 0 := by
+      omega
+    simp [ha]
+
+def superCommuteTakeM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ)  (n : ℕ)
+    (hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
+  superCommuteCoefM q l (List.take n r) •
+  (ofListM f (List.take n r) 1 *
+  superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))
+  * ofListM f (List.drop (n + 1) r) y)
+
+lemma superCommuteM_ofList_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (b1 : I) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListM f (b1 :: r) y) =
+    superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ b1)) * ofListM f r y +
+    superCommuteCoefM q l [b1] •
+    (ofListM f [b1] 1) * superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
+  rw [ofListM_cons]
+  conv_lhs =>
+    rhs
+    rw [ofListM_expand]
+    rw [Finset.mul_sum]
+  rw [map_sum]
+  trans ∑ n, ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x)) (( FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList (liftM f r n) y)
+  · apply congrArg
+    funext n
+    rw [← map_sum]
+    congr
+    rw [Finset.sum_mul]
+  conv_rhs =>
+    lhs
+    rw [ofListM_expand, Finset.mul_sum]
+  conv_rhs =>
+    rhs
+    rhs
+    rw [ofListM_expand]
+    rw [map_sum]
+  conv_rhs =>
+    rhs
+    rw [Finset.mul_sum]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext n
+  rw [freeAlgebraMap_ι, map_sum, Finset.sum_mul]
+  conv_rhs =>
+    rhs
+    rw [ofListM_singleton]
+    rw [Finset.smul_sum, Finset.sum_mul]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext b
+  trans ((superCommute fun i => q i.fst) (ofList l x)) (ofList (⟨b1, b⟩ :: liftM f r n) y)
+  · congr
+    rw [ofList_cons_eq_ofList]
+    rw [ofList_singleton]
+  rw [superCommute_ofList_cons]
+  congr
+  rw [ofList_singleton]
+  simp
+
+lemma superCommute_ofList_ofListM_sum  {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
+    ∑ (n : Fin r.length), superCommuteTakeM q l r x y n n.prop  := by
+  induction r with
+  | nil =>
+    simp only [superCommute_ofList_ofListM, Fin.isValue, grade_empty, zero_ne_one, and_false,
+      ↓reduceIte, neg_mul, List.length_nil, Finset.univ_eq_empty, Finset.sum_empty]
+    rw [ofListM, ofList_empty']
+    simp
+  | cons b r ih =>
+    rw [superCommuteM_ofList_cons]
+    have h0 :  ((superCommute fun i => q i.fst) (ofList l x)) ((freeAlgebraMap f) (FreeAlgebra.ι ℂ b)) * ofListM f r y  =
+        superCommuteTakeM q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
+      simp [superCommuteTakeM, superCommuteCoefM_empty, ofListM_empty]
+    rw [h0]
+    have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n =  g ⟨0,
+        Nat.zero_lt_succ r.length⟩ + ∑ n, g (Fin.succ n) := by
+      exact Fin.sum_univ_succAbove g ⟨0, Nat.zero_lt_succ r.length⟩
+    rw [hf]
+    congr
+    rw [ih]
+    rw [Finset.mul_sum]
+    congr
+    funext n
+    simp only [superCommuteTakeM, Fin.eta, List.get_eq_getElem, Algebra.mul_smul_comm,
+      Algebra.smul_mul_assoc, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
+      List.getElem_cons_succ, List.drop_succ_cons]
+    congr 1
+    · rw [mul_comm, ← superCommuteCoefM_append]
+      rfl
+    · simp only [← mul_assoc, mul_eq_mul_right_iff]
+      apply Or.inl
+      apply Or.inl
+      rw [ofListM, ofListM, ofListM]
+      rw [← map_mul]
+      congr
+      rw [← ofList_pair, one_mul]
+      rfl
+
+end
+end Wick