Koszul sign

def Wick.koszulSign {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] : List 𝓕 → ℂ

Gives a factor of - 1 for every fermion-fermion (q is 1) crossing that occurs when sorting a list of based on r.

Equations

• Wick.koszulSign q le [] = 1
• Wick.koszulSign q le (a :: l) = Wick.koszulSignInsert q le a l * Wick.koszulSign q le l

@[simp]

theorem Wick.koszulSign_singleton {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) : koszulSign q le [φ] = 1

theorem Wick.koszulSign_mul_self {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (l : List 𝓕) : koszulSign q le l * koszulSign q le l = 1

@[simp]

theorem Wick.koszulSign_freeMonoid_of {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) : koszulSign q le (FreeMonoid.of φ) = 1

theorem Wick.koszulSignInsert_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (φs : List 𝓕) (n : Fin φs.length) (heq : q (φs.get n) = FieldStatistic.bosonic) : koszulSignInsert q le φ (φs.eraseIdx ↑n) = koszulSignInsert q le φ φs

theorem Wick.koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φs : List 𝓕) (n : Fin φs.length) (heq : q (φs.get n) = FieldStatistic.bosonic) : koszulSign q le (φs.eraseIdx ↑n) = koszulSign q le φs

theorem Wick.koszulSign_insertIdx {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) (φs : List 𝓕) (n : ℕ) (hn : n ≤ φs.length) : koszulSign q le (List.insertIdx n φ φs) = (FieldStatistic.exchangeSign (q φ)) (FieldStatistic.ofList q (List.take n φs)) * koszulSign q le φs * (FieldStatistic.exchangeSign (q φ)) (FieldStatistic.ofList q (List.take (↑((PhysLean.List.insertionSortEquiv le (List.insertIdx n φ φs)) ⟨n, ⋯⟩)) (List.insertionSort le (List.insertIdx n φ φs))))

theorem Wick.insertIdx_eraseIdx {I : Type} (n : ℕ) (r : List I) (hn : n < r.length) : List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r

theorem Wick.koszulSign_eraseIdx {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φs : List 𝓕) (n : Fin φs.length) : koszulSign q le (φs.eraseIdx ↑n) = koszulSign q le φs * (FieldStatistic.exchangeSign (q (φs.get n))) (FieldStatistic.ofList q (List.take (↑n) φs)) * (FieldStatistic.exchangeSign (q (φs.get n))) (FieldStatistic.ofList q (List.take (↑((PhysLean.List.insertionSortEquiv le φs) n)) (List.insertionSort le φs)))

theorem Wick.koszulSign_eraseIdx_insertionSortMinPos {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) (φs : List 𝓕) : koszulSign q le ((φ :: φs).eraseIdx ↑(PhysLean.List.insertionSortMinPos le φ φs)) = koszulSign q le (φ :: φs) * (FieldStatistic.exchangeSign (q (PhysLean.List.insertionSortMin le φ φs))) (FieldStatistic.ofList q (List.take (↑(PhysLean.List.insertionSortMinPos le φ φs)) (φ :: φs)))

theorem Wick.koszulSign_swap_eq_rel_cons {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ : 𝓕} (h1 : le φ ψ) (h2 : le ψ φ) (φs' : List 𝓕) : koszulSign q le (φ :: ψ :: φs') = koszulSign q le (ψ :: φ :: φs')

theorem Wick.koszulSign_swap_eq_rel {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ : 𝓕} (h1 : le φ ψ) (h2 : le ψ φ) (φs φs' : List 𝓕) : koszulSign q le (φs ++ φ :: ψ :: φs') = koszulSign q le (φs ++ ψ :: φ :: φs')

theorem Wick.koszulSign_eq_rel_eq_stat_append {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ : 𝓕} [IsTrans 𝓕 le] (h1 : le φ ψ) (h2 : le ψ φ) (hq : q ψ = q φ) (φs : List 𝓕) : koszulSign q le (φ :: ψ :: φs) = koszulSign q le φs

theorem Wick.koszulSign_eq_rel_eq_stat {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ : 𝓕} [IsTrans 𝓕 le] (h1 : le φ ψ) (h2 : le ψ φ) (hq : q ψ = q φ) (φs' φs : List 𝓕) : koszulSign q le (φs' ++ φ :: ψ :: φs) = koszulSign q le (φs' ++ φs)

theorem Wick.koszulSign_of_sorted {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φs : List 𝓕) (hs : List.Sorted le φs) : koszulSign q le φs = 1

@[simp]

theorem Wick.koszulSign_of_insertionSort {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φs : List 𝓕) : koszulSign q le (List.insertionSort le φs) = 1

theorem Wick.koszulSign_of_append_eq_insertionSort_left {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φs φs' : List 𝓕) : koszulSign q le (φs ++ φs') = koszulSign q le (List.insertionSort le φs ++ φs') * koszulSign q le φs

theorem Wick.koszulSign_of_append_eq_insertionSort {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φs'' φs φs' : List 𝓕) : koszulSign q le (φs'' ++ φs ++ φs') = koszulSign q le (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le φs

koszulSign with permutations

theorem Wick.koszulSign_perm_eq_append {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTrans 𝓕 le] (φ : 𝓕) (φs φs' φs2 : List 𝓕) (hp : φs.Perm φs') (h : ∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) : koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)

theorem Wick.koszulSign_perm_eq {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTrans 𝓕 le] (φ : 𝓕) (φs1 φs φs' φs2 : List 𝓕) (h : ∀ φ' ∈ φs, le φ φ' ∧ le φ' φ) (hp : φs.Perm φs') : koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)