refactor: rm grade update SuperCommuteCoef
This commit is contained in:
jstoobysmith
parent
83f5fc5e9c
commit
9c0c499292
3 changed files with 36 additions and 137 deletions
|
|
@ -1,104 +0,0 @@
|
|||
/-
|
||||
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 Mathlib.Algebra.FreeAlgebra
|
||||
import Mathlib.Algebra.Lie.OfAssociative
|
||||
import Mathlib.Analysis.Complex.Basic
|
||||
/-!
|
||||
|
||||
# Grade
|
||||
|
||||
The grade `0` (for boson) or `1` (for fermion) of a list of fields.
|
||||
|
||||
-/
|
||||
|
||||
namespace Wick
|
||||
|
||||
/-- Given a grading map `q : I → Fin 2` and a list `l : List I` counts the parity of the number of
|
||||
elements in `l` which are of grade `1`. -/
|
||||
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_count {I : Type} (q : I → Fin 2) (l : List I) :
|
||||
grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons r0 r ih =>
|
||||
simp only [grade, Fin.isValue]
|
||||
rw [List.countP_cons]
|
||||
simp only [Fin.isValue, decide_eq_true_eq]
|
||||
rw [ih]
|
||||
by_cases h: q r0 = 1
|
||||
· simp only [h, Fin.isValue, ↓reduceIte]
|
||||
split
|
||||
next h1 =>
|
||||
simp_all only [Fin.isValue, ↓reduceIte, one_ne_zero]
|
||||
split
|
||||
next h2 =>
|
||||
simp_all only [Fin.isValue, one_ne_zero]
|
||||
have ha (a : ℕ) (ha : a % 2 = 0) : (a + 1) % 2 ≠ 0 := by
|
||||
omega
|
||||
exact ha (List.countP (fun i => decide (q i = 1)) r) h1 h2
|
||||
next h2 => simp_all only [Fin.isValue]
|
||||
next h1 =>
|
||||
simp_all only [Fin.isValue, ↓reduceIte]
|
||||
split
|
||||
next h2 => simp_all only [Fin.isValue]
|
||||
next h2 =>
|
||||
simp_all only [Fin.isValue, zero_ne_one]
|
||||
have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
|
||||
omega
|
||||
exact h2 (ha (List.countP (fun i => decide (q i = 1)) r) h1)
|
||||
· have h0 : q r0 = 0 := by omega
|
||||
simp only [h0, Fin.isValue, zero_ne_one, ↓reduceIte, add_zero]
|
||||
by_cases hn : (List.countP (fun i => decide (q i = 1)) r).mod 2 = 0
|
||||
· simp [hn]
|
||||
· simp [hn]
|
||||
|
||||
lemma grade_perm {I : Type} (q : I → Fin 2) {l l' : List I} (h : l.Perm l') :
|
||||
grade q l = grade q l' := by
|
||||
rw [grade_count, grade_count, h.countP_eq]
|
||||
|
||||
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
|
||||
apply grade_perm
|
||||
exact List.perm_orderedInsert le1 i l
|
||||
|
||||
@[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
|
||||
apply grade_perm
|
||||
exact List.perm_insertionSort le1 l
|
||||
|
||||
end Wick
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Mathematics.List
|
||||
import HepLean.PerturbationTheory.Wick.Signs.Grade
|
||||
import HepLean.PerturbationTheory.FieldStatistics
|
||||
/-!
|
||||
|
||||
# Koszul signs and ordering for lists and algebras
|
||||
|
|
@ -13,15 +13,19 @@ import HepLean.PerturbationTheory.Wick.Signs.Grade
|
|||
|
||||
namespace Wick
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic)
|
||||
|
||||
/-- Given two lists `la` and `lb` returns `-1` if they are both of grade `1` and
|
||||
`1` otherwise. This corresponds to the sign associated with the super commutator
|
||||
when commuting `la` and `lb` in the free algebra.
|
||||
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
|
||||
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
|
||||
def superCommuteCoef (la lb : List 𝓕) : ℂ :=
|
||||
if FieldStatistic.ofList q la = fermionic ∧
|
||||
FieldStatistic.ofList q lb = fermionic then - 1 else 1
|
||||
|
||||
lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
|
||||
lemma superCommuteCoef_comm (la lb : List 𝓕) :
|
||||
superCommuteCoef q la lb = superCommuteCoef q lb la := by
|
||||
simp only [superCommuteCoef, Fin.isValue]
|
||||
congr 1
|
||||
|
|
@ -33,57 +37,57 @@ lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
|
|||
the lift of `l` and `r` (by summing over fibers) in the
|
||||
free algebra over `Σ i, f i`.
|
||||
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
|
||||
def superCommuteLiftCoef {I : Type} {f : I → Type}
|
||||
(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)
|
||||
def superCommuteLiftCoef {f : 𝓕 → Type} (l : List (Σ i, f i)) (r : List 𝓕) : ℂ :=
|
||||
(if FieldStatistic.ofList (fun i => q i.fst) l = fermionic ∧
|
||||
FieldStatistic.ofList q r = fermionic then -1 else 1)
|
||||
|
||||
lemma superCommuteLiftCoef_empty {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) :
|
||||
lemma superCommuteLiftCoef_empty {f : 𝓕 → Type} (l : List (Σ i, f i)) :
|
||||
superCommuteLiftCoef q l [] = 1 := by
|
||||
simp [superCommuteLiftCoef]
|
||||
|
||||
lemma superCommuteCoef_perm_snd {I : Type} (q : I → Fin 2) (la lb lb' : List I)
|
||||
lemma superCommuteCoef_perm_snd (la lb lb' : List 𝓕)
|
||||
(h : lb.Perm lb') :
|
||||
superCommuteCoef q la lb = superCommuteCoef q la lb' := by
|
||||
rw [superCommuteCoef, superCommuteCoef, grade_perm q h]
|
||||
rw [superCommuteCoef, superCommuteCoef, FieldStatistic.ofList_perm q h]
|
||||
|
||||
lemma superCommuteCoef_mul_self {I : Type} (q : I → Fin 2) (l lb : List I) :
|
||||
lemma superCommuteCoef_mul_self (l lb : List 𝓕) :
|
||||
superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
|
||||
simp only [superCommuteCoef, Fin.isValue, mul_ite, mul_neg, mul_one]
|
||||
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
|
||||
have ha (a b : FieldStatistic) : (if a = fermionic ∧ b = fermionic then
|
||||
-if a = fermionic ∧ b = fermionic then -1 else 1
|
||||
else if a = fermionic ∧ b = fermionic then -1 else 1) = (1 : ℂ) := by
|
||||
fin_cases a <;> fin_cases b
|
||||
any_goals rfl
|
||||
simp
|
||||
exact ha (grade q l) (grade q lb)
|
||||
exact ha (FieldStatistic.ofList q l) (FieldStatistic.ofList q lb)
|
||||
|
||||
lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
|
||||
lemma superCommuteCoef_empty (la : List 𝓕) :
|
||||
superCommuteCoef q la [] = 1 := by
|
||||
simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
|
||||
simp only [superCommuteCoef, ofList_empty, reduceCtorEq, and_false, ↓reduceIte]
|
||||
|
||||
lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
|
||||
lemma superCommuteCoef_append (la lb lc : List 𝓕) :
|
||||
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,
|
||||
simp only [superCommuteCoef, Fin.isValue, ofList_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
|
||||
by_cases hla : ofList q la = fermionic
|
||||
· by_cases hlb : ofList q lb = fermionic
|
||||
· by_cases hlc : ofList q lc = fermionic
|
||||
· simp [hlc, hlb, hla]
|
||||
· have hc : grade q lc = 0 := by
|
||||
omega
|
||||
· have hc : ofList q lc = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (ofList q lc)).mp hlc
|
||||
simp [hc, hlb, hla]
|
||||
· have hb : grade q lb = 0 := by
|
||||
omega
|
||||
by_cases hlc : grade q lc = 1
|
||||
· have hb : ofList q lb = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (ofList q lb)).mp hlb
|
||||
by_cases hlc : ofList q lc = fermionic
|
||||
· simp [hlc, hb]
|
||||
· have hc : grade q lc = 0 := by
|
||||
omega
|
||||
· have hc : ofList q lc = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (ofList q lc)).mp hlc
|
||||
simp [hc, hb]
|
||||
· have ha : grade q la = 0 := by
|
||||
omega
|
||||
· have ha : ofList q la = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (ofList q la)).mp hla
|
||||
simp [ha]
|
||||
|
||||
lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
|
||||
lemma superCommuteCoef_cons (i : 𝓕) (la lb : List 𝓕) :
|
||||
superCommuteCoef q la (i :: lb) = superCommuteCoef q la [i] * superCommuteCoef q la lb := by
|
||||
trans superCommuteCoef q la ([i] ++ lb)
|
||||
simp only [List.singleton_append]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue