Merge pull request #268 from HEPLean/WickContract
feat: Introduce field statistics
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
fee2852367
17 changed files with 874 additions and 846 deletions
|
|
@ -118,12 +118,12 @@ import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
|
|||
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
|
||||
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
|
||||
import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
|
||||
import HepLean.PerturbationTheory.Wick.Contraction
|
||||
import HepLean.PerturbationTheory.Wick.CreateAnnilateSection
|
||||
import HepLean.PerturbationTheory.FieldStatistics
|
||||
import HepLean.PerturbationTheory.Wick.Contractions
|
||||
import HepLean.PerturbationTheory.Wick.CreateAnnihilateSection
|
||||
import HepLean.PerturbationTheory.Wick.KoszulOrder
|
||||
import HepLean.PerturbationTheory.Wick.OfList
|
||||
import HepLean.PerturbationTheory.Wick.OperatorMap
|
||||
import HepLean.PerturbationTheory.Wick.Signs.Grade
|
||||
import HepLean.PerturbationTheory.Wick.Signs.InsertSign
|
||||
import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
|
||||
import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
|
||||
|
|
|
|||
|
|
@ -342,28 +342,28 @@ lemma pauliMatrix_contr_down_0 :
|
|||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 1, 1]
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
enter [1, 1, 1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
enter [1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
enter [1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
|
|
@ -416,12 +416,10 @@ lemma pauliMatrix_contr_down_1 :
|
|||
congr 1
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· rw [basisVectorContrPauli]
|
||||
congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_down_2 :
|
||||
{(basisVector ![Color.down, Color.down] fun _ => 2) | μ ν ⊗
|
||||
|
|
|
|||
|
|
@ -92,28 +92,28 @@ lemma pauliMatrix_contr_lower_0_1_1 :
|
|||
lhs
|
||||
rw [basis_contr_pauliMatrix_basis_tree_expand_tensor]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 1, 1]
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_pos (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; lhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; lhs; rhs; rhs; lhs
|
||||
enter [1, 1, 1, 1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; lhs; rhs; rhs; lhs
|
||||
enter [1, 1, 1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs;
|
||||
enter [1, 1, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
enter [1, 2, 2, 1]
|
||||
rw [contrBasisVectorMul_neg (by decide)]
|
||||
conv =>
|
||||
lhs
|
||||
|
|
@ -122,11 +122,9 @@ lemma pauliMatrix_contr_lower_0_1_1 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_1_0_1 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗
|
||||
|
|
@ -167,11 +165,9 @@ lemma pauliMatrix_contr_lower_1_0_1 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_1_1_0 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗
|
||||
|
|
@ -212,11 +208,9 @@ lemma pauliMatrix_contr_lower_1_1_0 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 1
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_2_0_1 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗
|
||||
|
|
@ -258,11 +252,9 @@ lemma pauliMatrix_contr_lower_2_0_1 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_2_1_0 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗
|
||||
|
|
@ -304,11 +296,9 @@ lemma pauliMatrix_contr_lower_2_1_0 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_3_0_0 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗
|
||||
|
|
@ -350,11 +340,9 @@ lemma pauliMatrix_contr_lower_3_0_0 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
lemma pauliMatrix_contr_lower_3_1_1 :
|
||||
{(basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗
|
||||
|
|
@ -396,11 +384,9 @@ lemma pauliMatrix_contr_lower_3_1_1 :
|
|||
/- Simplifying. -/
|
||||
congr 1
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
· congr 2
|
||||
funext k
|
||||
fin_cases k <;> rfl
|
||||
decide
|
||||
|
||||
/-! TODO: Work out why `pauliCo_prod_basis_expand'` is needed. -/
|
||||
/-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
|
||||
|
|
@ -549,13 +535,9 @@ theorem pauliCo_contr_pauliContr :
|
|||
abel
|
||||
rw [h1]
|
||||
congr
|
||||
· funext i
|
||||
fin_cases i <;> rfl
|
||||
· funext i
|
||||
fin_cases i <;> rfl
|
||||
· funext i
|
||||
fin_cases i <;> rfl
|
||||
· funext i
|
||||
fin_cases i <;> rfl
|
||||
· decide
|
||||
· decide
|
||||
· decide
|
||||
· decide
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
|
|||
153
HepLean/PerturbationTheory/FieldStatistics.lean
Normal file
153
HepLean/PerturbationTheory/FieldStatistics.lean
Normal file
|
|
@ -0,0 +1,153 @@
|
|||
/-
|
||||
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
|
||||
/-!
|
||||
|
||||
# Field statistics
|
||||
|
||||
Basic properties related to whether a field, or list of fields, is bosonic or fermionic.
|
||||
|
||||
-/
|
||||
|
||||
/-- A field can either be bosonic or fermionic in nature.
|
||||
That is to say, they can either have Bose-Einstein statistics or
|
||||
Fermi-Dirac statistics. -/
|
||||
inductive FieldStatistic : Type where
|
||||
| bosonic : FieldStatistic
|
||||
| fermionic : FieldStatistic
|
||||
deriving DecidableEq
|
||||
|
||||
namespace FieldStatistic
|
||||
|
||||
variable {𝓕 : Type}
|
||||
|
||||
/-- Field statics form a finite type. -/
|
||||
instance : Fintype FieldStatistic where
|
||||
elems := {bosonic, fermionic}
|
||||
complete := by
|
||||
intro c
|
||||
cases c
|
||||
· exact Finset.mem_insert_self bosonic {fermionic}
|
||||
· refine Finset.insert_eq_self.mp ?_
|
||||
exact rfl
|
||||
|
||||
@[simp]
|
||||
lemma fermionic_not_eq_bonsic : ¬ fermionic = bosonic := by
|
||||
intro h
|
||||
exact FieldStatistic.noConfusion h
|
||||
|
||||
lemma bonsic_eq_fermionic_false : bosonic = fermionic ↔ false := by
|
||||
simp only [reduceCtorEq, Bool.false_eq_true]
|
||||
|
||||
@[simp]
|
||||
lemma neq_fermionic_iff_eq_bosonic (a : FieldStatistic) : ¬ a = fermionic ↔ a = bosonic := by
|
||||
fin_cases a
|
||||
· simp
|
||||
· simp
|
||||
|
||||
@[simp]
|
||||
lemma bosonic_neq_iff_fermionic_eq (a : FieldStatistic) : ¬ bosonic = a ↔ fermionic = a := by
|
||||
fin_cases a
|
||||
· simp
|
||||
· simp
|
||||
|
||||
@[simp]
|
||||
lemma fermionic_neq_iff_bosonic_eq (a : FieldStatistic) : ¬ fermionic = a ↔ bosonic = a := by
|
||||
fin_cases a
|
||||
· simp
|
||||
· simp
|
||||
|
||||
lemma eq_self_if_eq_bosonic {a : FieldStatistic} :
|
||||
(if a = bosonic then bosonic else fermionic) = a := by
|
||||
fin_cases a <;> rfl
|
||||
|
||||
lemma eq_self_if_bosonic_eq {a : FieldStatistic} :
|
||||
(if bosonic = a then bosonic else fermionic) = a := by
|
||||
fin_cases a <;> rfl
|
||||
|
||||
/-- The field statistics of a list of fields is fermionic if ther is an odd number of fermions,
|
||||
otherwise it is bosonic. -/
|
||||
def ofList (s : 𝓕 → FieldStatistic) : (φs : List 𝓕) → FieldStatistic
|
||||
| [] => bosonic
|
||||
| φ :: φs => if s φ = ofList s φs then bosonic else fermionic
|
||||
|
||||
@[simp]
|
||||
lemma ofList_singleton (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s [φ] = s φ := by
|
||||
simp only [ofList, Fin.isValue]
|
||||
rw [eq_self_if_eq_bosonic]
|
||||
|
||||
@[simp]
|
||||
lemma ofList_freeMonoid (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s (FreeMonoid.of φ) = s φ :=
|
||||
ofList_singleton s φ
|
||||
|
||||
@[simp]
|
||||
lemma ofList_empty (s : 𝓕 → FieldStatistic) : ofList s [] = bosonic := rfl
|
||||
|
||||
@[simp]
|
||||
lemma ofList_append (s : 𝓕 → FieldStatistic) (l r : List 𝓕) :
|
||||
ofList s (l ++ r) = if ofList s l = ofList s r then bosonic else fermionic := by
|
||||
induction l with
|
||||
| nil =>
|
||||
simp only [List.nil_append, ofList_empty, Fin.isValue, eq_self_if_bosonic_eq]
|
||||
| cons a l ih =>
|
||||
have hab (a b c : FieldStatistic) :
|
||||
(if a = (if b = c then bosonic else fermionic) then bosonic else fermionic) =
|
||||
if (if a = b then bosonic else fermionic) = c then bosonic else fermionic := by
|
||||
fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
|
||||
simp only [ofList, List.append_eq, Fin.isValue, ih, hab]
|
||||
|
||||
lemma ofList_eq_countP (s : 𝓕 → FieldStatistic) (φs : List 𝓕) :
|
||||
ofList s φs = if Nat.mod (List.countP (fun i => decide (s i = fermionic)) φs) 2 = 0 then
|
||||
bosonic else fermionic := by
|
||||
induction φs with
|
||||
| nil => simp
|
||||
| cons r0 r ih =>
|
||||
simp only [ofList]
|
||||
rw [List.countP_cons]
|
||||
simp only [decide_eq_true_eq]
|
||||
by_cases hr : s r0 = fermionic
|
||||
· simp only [hr, ↓reduceIte]
|
||||
simp_all only
|
||||
split
|
||||
next h =>
|
||||
simp_all only [↓reduceIte, fermionic_not_eq_bonsic]
|
||||
split
|
||||
next h_1 =>
|
||||
simp_all only [fermionic_not_eq_bonsic]
|
||||
have ha (a : ℕ) (ha : a % 2 = 0) : (a + 1) % 2 ≠ 0 := by
|
||||
omega
|
||||
exact ha (List.countP (fun i => decide (s i = fermionic)) r) h h_1
|
||||
next h_1 => simp_all only
|
||||
next h =>
|
||||
simp_all only [↓reduceIte]
|
||||
split
|
||||
next h_1 => rfl
|
||||
next h_1 =>
|
||||
simp_all only [reduceCtorEq]
|
||||
have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
|
||||
omega
|
||||
exact h_1 (ha (List.countP (fun i => decide (s i = fermionic)) r) h)
|
||||
· simp only [neq_fermionic_iff_eq_bosonic] at hr
|
||||
by_cases hx : (List.countP (fun i => decide (s i = fermionic)) r).mod 2 = 0
|
||||
· simpa [hx, hr] using ih.symm
|
||||
· simpa [hx, hr] using ih.symm
|
||||
|
||||
lemma ofList_perm (s : 𝓕 → FieldStatistic) {l l' : List 𝓕} (h : l.Perm l') :
|
||||
ofList s l = ofList s l' := by
|
||||
rw [ofList_eq_countP, ofList_eq_countP, h.countP_eq]
|
||||
|
||||
lemma ofList_orderedInsert (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1]
|
||||
(φs : List 𝓕) (φ : 𝓕) : ofList s (List.orderedInsert le1 φ φs) = ofList s (φ :: φs) :=
|
||||
ofList_perm s (List.perm_orderedInsert le1 φ φs)
|
||||
|
||||
@[simp]
|
||||
lemma ofList_insertionSort (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1]
|
||||
(φs : List 𝓕) : ofList s (List.insertionSort le1 φs) = ofList s φs :=
|
||||
ofList_perm s (List.perm_insertionSort le1 φs)
|
||||
|
||||
end FieldStatistic
|
||||
|
|
@ -12,34 +12,35 @@ import HepLean.PerturbationTheory.Wick.OperatorMap
|
|||
|
||||
namespace Wick
|
||||
|
||||
noncomputable section
|
||||
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type}
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`
|
||||
which have the list `aux` uncontracted. -/
|
||||
inductive ContractionsAux {I : Type} : (l : List I) → (aux : List I) → Type
|
||||
inductive ContractionsAux : (l : List 𝓕) → (aux : List 𝓕) → Type
|
||||
| nil : ContractionsAux [] []
|
||||
| cons {l : List I} {aux : List I} {a : I} (i : Option (Fin aux.length)) :
|
||||
| cons {l : List 𝓕} {aux : List 𝓕} {a : 𝓕} (i : Option (Fin aux.length)) :
|
||||
ContractionsAux l aux → ContractionsAux (a :: l) (optionEraseZ aux a i)
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`. -/
|
||||
def Contractions {I : Type} (l : List I) : Type := Σ aux, ContractionsAux l aux
|
||||
def Contractions (l : List 𝓕) : Type := Σ aux, ContractionsAux l aux
|
||||
|
||||
namespace Contractions
|
||||
|
||||
variable {I : Type} {l : List I} (c : Contractions l)
|
||||
variable {l : List 𝓕} (c : Contractions l)
|
||||
|
||||
/-- The list of uncontracted fields. -/
|
||||
def normalize : List I := c.1
|
||||
def normalize : List 𝓕 := c.1
|
||||
|
||||
lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], ContractionsAux.nil⟩ := by
|
||||
lemma contractions_nil (a : Contractions ([] : List 𝓕)) : a = ⟨[], ContractionsAux.nil⟩ := by
|
||||
cases a
|
||||
rename_i aux c
|
||||
cases c
|
||||
rfl
|
||||
|
||||
lemma contractions_single {i : I} (a : Contractions [i]) : a =
|
||||
lemma contractions_single {i : 𝓕} (a : Contractions [i]) : a =
|
||||
⟨[i], ContractionsAux.cons none ContractionsAux.nil⟩ := by
|
||||
cases a
|
||||
rename_i aux c
|
||||
|
|
@ -52,7 +53,7 @@ lemma contractions_single {i : I} (a : Contractions [i]) : a =
|
|||
exact Fin.elim0 x
|
||||
|
||||
/-- For the nil list of fields there is only one contraction. -/
|
||||
def nilEquiv : Contractions ([] : List I) ≃ Unit where
|
||||
def nilEquiv : Contractions ([] : List 𝓕) ≃ Unit where
|
||||
toFun _ := ()
|
||||
invFun _ := ⟨[], ContractionsAux.nil⟩
|
||||
left_inv a := Eq.symm (contractions_nil a)
|
||||
|
|
@ -61,7 +62,7 @@ def nilEquiv : Contractions ([] : List I) ≃ Unit where
|
|||
/-- The equivalence between contractions of `a :: l` and contractions of
|
||||
`Contractions l` paired with an optional element of `Fin (c.normalize).length` specifying
|
||||
what `a` contracts with if any. -/
|
||||
def consEquiv {a : I} {l : List I} :
|
||||
def consEquiv {a : 𝓕} {l : List 𝓕} :
|
||||
Contractions (a :: l) ≃ (c : Contractions l) × Option (Fin (c.normalize).length) where
|
||||
toFun c :=
|
||||
match c with
|
||||
|
|
@ -78,7 +79,7 @@ def consEquiv {a : I} {l : List I} :
|
|||
right_inv ci := by rfl
|
||||
|
||||
/-- The type of contractions is decidable. -/
|
||||
instance decidable : (l : List I) → DecidableEq (Contractions l)
|
||||
instance decidable : (l : List 𝓕) → DecidableEq (Contractions l)
|
||||
| [] => fun a b =>
|
||||
match a, b with
|
||||
| ⟨_, a⟩, ⟨_, b⟩ =>
|
||||
|
|
@ -91,7 +92,7 @@ instance decidable : (l : List I) → DecidableEq (Contractions l)
|
|||
Equiv.decidableEq consEquiv
|
||||
|
||||
/-- The type of contractions is finite. -/
|
||||
instance fintype : (l : List I) → Fintype (Contractions l)
|
||||
instance fintype : (l : List 𝓕) → Fintype (Contractions l)
|
||||
| [] => {
|
||||
elems := {⟨[], ContractionsAux.nil⟩}
|
||||
complete := by
|
||||
|
|
@ -106,42 +107,42 @@ instance fintype : (l : List I) → Fintype (Contractions l)
|
|||
|
||||
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
|
||||
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
|
||||
structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] where
|
||||
/-- The creation part of the fields. The label `n` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the negative (left) direction. -/
|
||||
𝓑n : I → (Σ i, f i)
|
||||
𝓑n : 𝓕 → (Σ i, f i)
|
||||
/-- The annhilation part of the fields. The label `p` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the positive (right) direction. -/
|
||||
𝓑p : I → (Σ i, f i)
|
||||
𝓑p : 𝓕 → (Σ i, f i)
|
||||
/-- The complex coefficent of creation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧n : I → ℂ
|
||||
𝓧n : 𝓕 → ℂ
|
||||
/-- The complex coefficent of annhilation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧p : I → ℂ
|
||||
𝓧p : 𝓕 → ℂ
|
||||
h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
|
||||
h𝓑n : ∀ i j, le1 (𝓑n i) j
|
||||
h𝓑p : ∀ i j, le1 j (𝓑p i)
|
||||
|
||||
/-- In the static wick's theorem, the term associated with a contraction `c` containing
|
||||
the contractions. -/
|
||||
def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
noncomputable def toCenterTerm (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(q : 𝓕 → FieldStatistic)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A) :
|
||||
{r : List I} → (c : Contractions r) → (S : Splitting f le1) → A
|
||||
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le1) → A
|
||||
| [], ⟨[], .nil⟩, _ => 1
|
||||
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
|
||||
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
|
||||
superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
|
||||
F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListLift f [aux'.get n] 1))
|
||||
|
||||
lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) {r : List I}
|
||||
lemma toCenterTerm_none (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(q : 𝓕 → FieldStatistic) {r : List 𝓕}
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
|
||||
(S : Splitting f le1) (a : I) (c : Contractions r) :
|
||||
(S : Splitting f le1) (a : 𝓕) (c : Contractions r) :
|
||||
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S =
|
||||
toCenterTerm f q le1 F c S := by
|
||||
rw [consEquiv]
|
||||
|
|
@ -149,34 +150,33 @@ lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
|||
dsimp [toCenterTerm]
|
||||
rfl
|
||||
|
||||
lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(q : 𝓕 → FieldStatistic)
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
|
||||
{r : List I} → (c : Contractions r) → (S : Splitting f le1) →
|
||||
(c.toCenterTerm f q le1 F S) ∈ Subalgebra.center ℂ A
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F] :
|
||||
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le) →
|
||||
(c.toCenterTerm f q le F S) ∈ Subalgebra.center ℂ A
|
||||
| [], ⟨[], .nil⟩, _ => by
|
||||
dsimp [toCenterTerm]
|
||||
exact Subalgebra.one_mem (Subalgebra.center ℂ A)
|
||||
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => by
|
||||
dsimp [toCenterTerm]
|
||||
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
|
||||
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
|
||||
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
|
||||
dsimp [toCenterTerm]
|
||||
refine Subalgebra.mul_mem (Subalgebra.center ℂ A) ?hx ?hy
|
||||
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
|
||||
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
|
||||
apply Subalgebra.smul_mem
|
||||
rw [ofListLift_expand]
|
||||
rw [map_sum, map_sum]
|
||||
refine Subalgebra.sum_mem (Subalgebra.center ℂ A) ?hy.hx.h
|
||||
intro x _
|
||||
simp only [CreateAnnilateSect.toList]
|
||||
simp only [CreateAnnihilateSect.toList]
|
||||
rw [ofList_singleton]
|
||||
exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
|
||||
(le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
|
||||
(le := le) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
|
||||
|
||||
end Contractions
|
||||
|
||||
end
|
||||
end Wick
|
||||
|
|
@ -12,36 +12,45 @@ import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
|
|||
|
||||
namespace Wick
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
/-- The sections of `Σ i, f i` over a list `l : List I`.
|
||||
/-- The sections of `Σ i, f i` over a list `l : List 𝓕`.
|
||||
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
|
||||
each field as a `creation` or an `annilation` operator. E.g. the number of terms
|
||||
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
|
||||
operators at this point (e.g. ansymptotic states) this is accounted for. -/
|
||||
def CreateAnnilateSect {I : Type} (f : I → Type) (l : List I) : Type :=
|
||||
def CreateAnnihilateSect {𝓕 : Type} (f : 𝓕 → Type) (l : List 𝓕) : Type :=
|
||||
Π i, f (l.get i)
|
||||
|
||||
namespace CreateAnnilateSect
|
||||
namespace CreateAnnihilateSect
|
||||
|
||||
variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : CreateAnnilateSect f l)
|
||||
section basic_defs
|
||||
|
||||
/-- The type `CreateAnnilateSect f l` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnilateSect f l) := Pi.fintype
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {l : List 𝓕} (a : CreateAnnihilateSect f l)
|
||||
|
||||
/-- The type `CreateAnnihilateSect f l` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnihilateSect f l) := Pi.fintype
|
||||
|
||||
/-- The section got by dropping the first element of `l` if it exists. -/
|
||||
def tail : {l : List I} → (a : CreateAnnilateSect f l) → CreateAnnilateSect f l.tail
|
||||
def tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → CreateAnnihilateSect f l.tail
|
||||
| [], a => a
|
||||
| _ :: _, a => fun i => a (Fin.succ i)
|
||||
|
||||
/-- For a list of fields `i :: l` the value of the section at the head `i`. -/
|
||||
def head {i : I} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
|
||||
def head {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
|
||||
|
||||
end basic_defs
|
||||
|
||||
section toList_basic
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic)
|
||||
{l : List 𝓕} (a : CreateAnnihilateSect f l)
|
||||
|
||||
/-- The list `List (Σ i, f i)` defined by `a`. -/
|
||||
def toList : {l : List I} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
|
||||
def toList : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → List (Σ i, f i)
|
||||
| [], _ => []
|
||||
| i :: _, a => ⟨i, a.head⟩ :: toList a.tail
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma toList_length : (toList a).length = l.length := by
|
||||
induction l with
|
||||
|
|
@ -50,19 +59,16 @@ lemma toList_length : (toList a).length = l.length := by
|
|||
simp only [toList, List.length_cons, Fin.zero_eta]
|
||||
rw [ih]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_tail : {l : List I} → (a : CreateAnnilateSect f l) → toList a.tail = (toList a).tail
|
||||
lemma toList_tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → toList a.tail = (toList a).tail
|
||||
| [], _ => rfl
|
||||
| i :: l, a => by
|
||||
simp [toList]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_cons {i : I} (a : CreateAnnilateSect f (i :: l)) :
|
||||
lemma toList_cons {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) :
|
||||
(toList a) = ⟨i, a.head⟩ :: toList a.tail := by
|
||||
rfl
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_get (a : CreateAnnilateSect f l) :
|
||||
lemma toList_get (a : CreateAnnihilateSect f l) :
|
||||
(toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
|
||||
induction l with
|
||||
| nil =>
|
||||
|
|
@ -80,51 +86,54 @@ lemma toList_get (a : CreateAnnilateSect f l) :
|
|||
rw [ih]
|
||||
simp [tail]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma toList_grade (q : I → Fin 2) :
|
||||
grade (fun i => q i.fst) a.toList = 1 ↔ grade q l = 1 := by
|
||||
lemma toList_grade :
|
||||
FieldStatistic.ofList (fun i => q i.fst) a.toList = fermionic ↔
|
||||
FieldStatistic.ofList q l = fermionic := by
|
||||
induction l with
|
||||
| nil =>
|
||||
simp [toList]
|
||||
| cons i r ih =>
|
||||
simp only [grade, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
|
||||
simp only [ofList, 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) a.tail.toList = grade q r := by
|
||||
by_cases h : grade q r = 1
|
||||
have h1 : ofList (fun i => q i.fst) a.tail.toList = ofList q r := by
|
||||
by_cases h : ofList q r = fermionic
|
||||
· simp_all
|
||||
· have h0 : grade q r = 0 := by
|
||||
omega
|
||||
· have h0 : ofList q r = bosonic := (neq_fermionic_iff_eq_bosonic (ofList q r)).mp h
|
||||
rw [h0] at ih'
|
||||
simp only [Fin.isValue, zero_ne_one, iff_false] at ih'
|
||||
have h0' : grade (fun i => q i.fst) a.tail.toList = 0 := by
|
||||
simp only [List.tail_cons, tail, Fin.isValue]
|
||||
omega
|
||||
simp only [reduceCtorEq, iff_false, neq_fermionic_iff_eq_bosonic] at ih'
|
||||
have h0' : ofList (fun i => q i.fst) a.tail.toList = bosonic := ih'
|
||||
rw [h0, h0']
|
||||
rw [h1]
|
||||
|
||||
@[simp]
|
||||
lemma toList_grade_take {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) : (r : List I) → (a : CreateAnnilateSect f r) → (n : ℕ) →
|
||||
grade (fun i => q i.fst) (List.take n a.toList) = grade q (List.take n r)
|
||||
lemma toList_grade_take (q : 𝓕 → FieldStatistic) :
|
||||
(r : List 𝓕) → (a : CreateAnnihilateSect f r) → (n : ℕ) →
|
||||
ofList (fun i => q i.fst) (List.take n a.toList) = ofList q (List.take n r)
|
||||
| [], _, _ => by
|
||||
simp [toList]
|
||||
| i :: r, a, 0 => by
|
||||
simp
|
||||
| i :: r, a, Nat.succ n => by
|
||||
simp only [grade, Fin.isValue]
|
||||
simp only [ofList, Fin.isValue]
|
||||
rw [toList_grade_take q r a.tail n]
|
||||
|
||||
/-- The equivalence between `CreateAnnilateSect f l` and
|
||||
`f (l.get n) × CreateAnnilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
|
||||
end toList_basic
|
||||
|
||||
section toList_erase
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} {l : List 𝓕}
|
||||
|
||||
/-- The equivalence between `CreateAnnihilateSect f l` and
|
||||
`f (l.get n) × CreateAnnihilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
|
||||
from `l`. -/
|
||||
def extractEquiv {I : Type} {f : I → Type} {l : List I}
|
||||
(n : Fin l.length) : CreateAnnilateSect f l ≃
|
||||
f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
|
||||
def extractEquiv (n : Fin l.length) : CreateAnnihilateSect f l ≃
|
||||
f (l.get n) × CreateAnnihilateSect f (l.eraseIdx n) := by
|
||||
match l with
|
||||
| [] => exact Fin.elim0 n
|
||||
| l0 :: l =>
|
||||
let e1 : CreateAnnilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
|
||||
let e1 : CreateAnnihilateSect f ((l0 :: l).eraseIdx n) ≃
|
||||
Π i, f ((l0 :: l).get (n.succAbove i)) :=
|
||||
Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
|
||||
fun x => Equiv.cast (congrArg f (by
|
||||
rw [HepLean.List.eraseIdx_get]
|
||||
|
|
@ -153,16 +162,16 @@ def extractEquiv {I : Type} {f : I → Type} {l : List I}
|
|||
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]))
|
||||
exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)
|
||||
|
||||
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type}
|
||||
{l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreateAnnilateSect f (l.eraseIdx n)) :
|
||||
lemma extractEquiv_symm_toList_get_same (n : Fin l.length) (a0 : f (l.get n))
|
||||
(a : CreateAnnihilateSect f (l.eraseIdx n)) :
|
||||
((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
|
||||
match l with
|
||||
| [] => exact Fin.elim0 n
|
||||
| l0 :: l =>
|
||||
trans (((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
|
||||
trans (((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
|
||||
· simp only [List.length_cons, List.get_eq_getElem, Fin.coe_cast]
|
||||
rfl
|
||||
rw [CreateAnnilateSect.toList_get]
|
||||
rw [CreateAnnihilateSect.toList_get]
|
||||
simp only [List.get_eq_getElem, List.length_cons, extractEquiv, RelIso.coe_fn_toEquiv,
|
||||
Fin.castOrderIso_apply, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.prodCongr_symm,
|
||||
Equiv.refl_symm, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_apply, id_eq,
|
||||
|
|
@ -173,12 +182,12 @@ lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type}
|
|||
simp only [Fin.insertNth_apply_same]
|
||||
|
||||
/-- The section obtained by dropping the `n`th field. -/
|
||||
def eraseIdx (n : Fin l.length) : CreateAnnilateSect f (l.eraseIdx n) :=
|
||||
def eraseIdx (a : CreateAnnihilateSect f l) (n : Fin l.length) :
|
||||
CreateAnnihilateSect f (l.eraseIdx n) :=
|
||||
(extractEquiv n a).2
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)) :
|
||||
lemma eraseIdx_zero_tail {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) :
|
||||
(eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
|
||||
a.tail := by
|
||||
simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
|
||||
|
|
@ -187,9 +196,8 @@ lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)
|
|||
Equiv.cast_refl, Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
|
||||
rfl
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
|
||||
lemma eraseIdx_succ_head {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnihilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
|
||||
rw [eraseIdx, extractEquiv]
|
||||
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
|
||||
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
|
||||
|
|
@ -209,9 +217,8 @@ lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
|
|||
congr
|
||||
simp [Fin.ext_iff]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnilateSect f (i :: l)) :
|
||||
lemma eraseIdx_succ_tail {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnihilateSect f (i :: l)) :
|
||||
(eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
|
||||
match l with
|
||||
| [] =>
|
||||
|
|
@ -272,8 +279,7 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
|
|||
omega
|
||||
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
|
||||
lemma eraseIdx_toList : {l : List 𝓕} → {n : Fin l.length} → (a : CreateAnnihilateSect f l) →
|
||||
(eraseIdx a n).toList = a.toList.eraseIdx n
|
||||
| [], n, _ => Fin.elim0 n
|
||||
| r0 :: r, ⟨0, h⟩, a => by
|
||||
|
|
@ -287,7 +293,7 @@ lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnil
|
|||
rw [eraseIdx_succ_tail]
|
||||
|
||||
lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
|
||||
{l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnilateSect f (l.eraseIdx n)) :
|
||||
{l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnihilateSect f (l.eraseIdx n)) :
|
||||
((extractEquiv n).symm (a0, a)).eraseIdx n = a := by
|
||||
match l with
|
||||
| [] => exact Fin.elim0 n
|
||||
|
|
@ -295,22 +301,25 @@ lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
|
|||
rw [eraseIdx, extractEquiv]
|
||||
simp
|
||||
|
||||
lemma toList_koszulSignInsert {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(l : List I) (a : CreateAnnilateSect f l) (x : (i : I) × f i) :
|
||||
koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
|
||||
koszulSignInsert le1 q x.1 l := by
|
||||
end toList_erase
|
||||
|
||||
section toList_sign_conditions
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
{l : List 𝓕} (a : CreateAnnihilateSect f l)
|
||||
|
||||
lemma toList_koszulSignInsert (x : (i : 𝓕) × f i) :
|
||||
koszulSignInsert (fun i => q i.fst) (fun i j => le i.fst j.fst) x a.toList =
|
||||
koszulSignInsert q le x.1 l := by
|
||||
induction l with
|
||||
| nil => simp [koszulSignInsert]
|
||||
| cons b l ih =>
|
||||
simp only [koszulSignInsert, List.tail_cons, Fin.isValue]
|
||||
rw [ih]
|
||||
|
||||
lemma toList_koszulSign {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(l : List I) (a : CreateAnnilateSect f l) :
|
||||
koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
|
||||
koszulSign le1 q l := by
|
||||
lemma toList_koszulSign :
|
||||
koszulSign (fun i => q i.fst) (fun i j => le i.fst j.fst) a.toList =
|
||||
koszulSign q le l := by
|
||||
induction l with
|
||||
| nil => simp [koszulSign]
|
||||
| cons i l ih =>
|
||||
|
|
@ -319,11 +328,9 @@ lemma toList_koszulSign {I : Type} {f : I → Type}
|
|||
congr 1
|
||||
rw [toList_koszulSignInsert]
|
||||
|
||||
lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1](l : List I)
|
||||
(a : CreateAnnilateSect f l) :
|
||||
insertionSortEquiv (fun i j => le1 i.fst j.fst) a.toList =
|
||||
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le1 l).trans
|
||||
lemma insertionSortEquiv_toList :
|
||||
insertionSortEquiv (fun i j => le i.fst j.fst) a.toList =
|
||||
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le l).trans
|
||||
(Fin.castOrderIso (by simp)).toEquiv) := by
|
||||
induction l with
|
||||
| nil =>
|
||||
|
|
@ -341,13 +348,13 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
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
|
||||
List.map (fun i => i.1) (List.orderedInsert (fun i j => le i.fst j.fst) i l') =
|
||||
List.orderedInsert le i.1 (List.map (fun i => i.1) l') := by
|
||||
induction l' with
|
||||
| nil =>
|
||||
simp [HepLean.List.orderedInsertEquiv]
|
||||
| cons j l' ih' =>
|
||||
by_cases hij : (fun i j => le1 i.fst j.fst) i j
|
||||
by_cases hij : (fun i j => le i.fst j.fst) i j
|
||||
· rw [List.orderedInsert_of_le]
|
||||
· erw [List.orderedInsert_of_le]
|
||||
· simp
|
||||
|
|
@ -357,8 +364,8 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
simp only [↓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
|
||||
List.map (fun i => i.1) (List.insertionSort (fun i j => le i.fst j.fst) l') =
|
||||
List.insertionSort le (List.map (fun i => i.1) l') := by
|
||||
induction l' with
|
||||
| nil =>
|
||||
simp [HepLean.List.orderedInsertEquiv]
|
||||
|
|
@ -370,10 +377,10 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
rw [HepLean.List.orderedInsertEquiv_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) a.tail.toList)) =
|
||||
List.insertionSort le1 l := by
|
||||
have h3 : (List.insertionSort le (List.map (fun i => i.1) a.tail.toList)) =
|
||||
List.insertionSort le l := by
|
||||
congr
|
||||
have h3' (l : List I) (a : CreateAnnilateSect f l) :
|
||||
have h3' (l : List 𝓕) (a : CreateAnnihilateSect f l) :
|
||||
List.map (fun i => i.1) a.toList = l := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
|
|
@ -390,18 +397,17 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
|
||||
/-- Given a section for `l` the corresponding section
|
||||
for `List.insertionSort le1 l`. -/
|
||||
def sort (le1 : I → I → Prop) [DecidableRel le1] :
|
||||
CreateAnnilateSect f (List.insertionSort le1 l) :=
|
||||
Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
|
||||
def sort :
|
||||
CreateAnnihilateSect f (List.insertionSort le l) :=
|
||||
Equiv.piCongr (HepLean.List.insertionSortEquiv le l) (fun i => (Equiv.cast (by
|
||||
congr 1
|
||||
rw [← HepLean.List.insertionSortEquiv_get]
|
||||
simp))) a
|
||||
|
||||
lemma sort_toList {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreateAnnilateSect f l) :
|
||||
(a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
|
||||
let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) a.toList
|
||||
let l2 := (a.sort le1).toList
|
||||
lemma sort_toList :
|
||||
(a.sort le).toList = List.insertionSort (fun i j => le i.fst j.fst) a.toList := by
|
||||
let l1 := List.insertionSort (fun i j => le i.fst j.fst) a.toList
|
||||
let l2 := (a.sort le).toList
|
||||
symm
|
||||
change l1 = l2
|
||||
have hlen : l1.length = l2.length := by
|
||||
|
|
@ -415,7 +421,7 @@ lemma sort_toList {I : Type} {f : I → Type}
|
|||
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)
|
||||
· have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le) l) (Fin.cast (by simp) i)
|
||||
rw [← h1]
|
||||
simp
|
||||
· simp only [List.get_eq_getElem, sort, Equiv.piCongr, Equiv.trans_apply, Fin.coe_cast,
|
||||
|
|
@ -426,6 +432,7 @@ lemma sort_toList {I : Type} {f : I → Type}
|
|||
rw [hget]
|
||||
simp
|
||||
|
||||
end CreateAnnilateSect
|
||||
end toList_sign_conditions
|
||||
end CreateAnnihilateSect
|
||||
|
||||
end Wick
|
||||
|
|
@ -16,18 +16,20 @@ import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
|
|||
namespace Wick
|
||||
|
||||
noncomputable section
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
/-- 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))
|
||||
def koszulOrderMonoidAlgebra :
|
||||
MonoidAlgebra ℂ (FreeMonoid 𝓕) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid 𝓕) :=
|
||||
Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid 𝓕)) ℂ (List 𝓕)
|
||||
(fun i => Finsupp.lsingle (R := ℂ) (List.insertionSort le i) (koszulSign q le 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
|
||||
lemma koszulOrderMonoidAlgebra_ofList (i : List 𝓕) :
|
||||
koszulOrderMonoidAlgebra q le (MonoidAlgebra.of ℂ (FreeMonoid 𝓕) i) =
|
||||
(koszulSign q le i) • (MonoidAlgebra.of ℂ (FreeMonoid 𝓕) (List.insertionSort le i)) := by
|
||||
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
|
||||
MonoidAlgebra.smul_single', mul_one]
|
||||
rw [MonoidAlgebra.ext_iff]
|
||||
|
|
@ -37,10 +39,9 @@ lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [Decidab
|
|||
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
|
||||
lemma koszulOrderMonoidAlgebra_single (l : FreeMonoid 𝓕) (x : ℂ) :
|
||||
koszulOrderMonoidAlgebra q le (MonoidAlgebra.single l x)
|
||||
= (koszulSign q le l) • (MonoidAlgebra.single (List.insertionSort le l) x) := by
|
||||
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
|
||||
rw [MonoidAlgebra.ext_iff]
|
||||
intro x'
|
||||
|
|
@ -52,15 +53,13 @@ lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [Decidab
|
|||
|
||||
/-- 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 :=
|
||||
def koszulOrder : FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
|
||||
∘ₗ koszulOrderMonoidAlgebra r q
|
||||
∘ₗ koszulOrderMonoidAlgebra q le
|
||||
∘ₗ 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
|
||||
lemma koszulOrder_ι (i : 𝓕) : koszulOrder q le (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]
|
||||
|
|
@ -75,18 +74,16 @@ lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I
|
|||
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))
|
||||
lemma koszulOrder_single (l : FreeMonoid 𝓕) :
|
||||
koszulOrder q le (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
|
||||
= FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
|
||||
(MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
|
||||
(MonoidAlgebra.single (List.insertionSort le l) (koszulSign q le 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
|
||||
lemma koszulOrder_ι_pair (i j : 𝓕) : koszulOrder q le (FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j) =
|
||||
if le i j then FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j else
|
||||
(koszulSign q le [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,
|
||||
|
|
@ -97,11 +94,11 @@ lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q
|
|||
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
|
||||
by_cases hr : le 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
|
||||
have hKS : koszulSign q le [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)
|
||||
|
|
@ -114,9 +111,8 @@ lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q
|
|||
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))
|
||||
lemma koszulOrder_one : koszulOrder q le 1 = 1 := by
|
||||
trans koszulOrder q le (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
|
||||
congr
|
||||
· simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
|
||||
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
|
||||
|
|
@ -124,16 +120,15 @@ lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I
|
|||
· 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 := {
|
||||
lemma mul_koszulOrder_le (i : 𝓕) (A : FreeAlgebra ℂ 𝓕) (hi : ∀ j, le i j) :
|
||||
FreeAlgebra.ι ℂ i * koszulOrder q le A = koszulOrder q le (FreeAlgebra.ι ℂ i * A) := by
|
||||
let f : FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 := {
|
||||
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 : ℂ) :
|
||||
change (f ∘ₗ koszulOrder q le) A = (koszulOrder q le ∘ₗ f) _
|
||||
have f_single (l : FreeMonoid 𝓕) (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]
|
||||
|
|
@ -146,8 +141,8 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
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) :=
|
||||
have h1 : f ∘ₗ koszulOrder q le = koszulOrder q le ∘ₗ f := by
|
||||
let e : FreeAlgebra ℂ 𝓕 ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid 𝓕) :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
|
||||
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
|
||||
apply MonoidAlgebra.lhom_ext'
|
||||
|
|
@ -162,30 +157,29 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
rw [koszulOrder_single]
|
||||
congr 2
|
||||
· simp only [List.insertionSort]
|
||||
have hi (l : List I) : i :: l = List.orderedInsert r i l := by
|
||||
have hi (l : List 𝓕) : i :: l = List.orderedInsert le i l := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons j l ih =>
|
||||
refine (List.orderedInsert_of_le r l (hi j)).symm
|
||||
refine (List.orderedInsert_of_le le l (hi j)).symm
|
||||
exact hi _
|
||||
· congr 1
|
||||
rw [koszulSign]
|
||||
have h1 (l : List I) : koszulSignInsert r q i l = 1 := by
|
||||
exact koszulSignInsert_le_forall r q i l hi
|
||||
have h1 (l : List 𝓕) : koszulSignInsert q le i l = 1 := by
|
||||
exact koszulSignInsert_le_forall q le i l hi
|
||||
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 := {
|
||||
lemma koszulOrder_mul_ge (i : 𝓕) (A : FreeAlgebra ℂ 𝓕) (hi : ∀ j, le j i) :
|
||||
koszulOrder q le A * FreeAlgebra.ι ℂ i = koszulOrder q le (A * FreeAlgebra.ι ℂ i) := by
|
||||
let f : FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 := {
|
||||
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 : ℂ) :
|
||||
change (f ∘ₗ koszulOrder q le) A = (koszulOrder q le ∘ₗ f) A
|
||||
have f_single (l : FreeMonoid 𝓕) (x : ℂ) :
|
||||
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
|
||||
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
|
||||
(MonoidAlgebra.single (l.toList ++ [i]) x)) := by
|
||||
|
|
@ -199,8 +193,8 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
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) :=
|
||||
have h1 : f ∘ₗ koszulOrder q le = koszulOrder q le ∘ₗ f := by
|
||||
let e : FreeAlgebra ℂ 𝓕 ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid 𝓕) :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
|
||||
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
|
||||
apply MonoidAlgebra.lhom_ext'
|
||||
|
|
@ -214,20 +208,21 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
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
|
||||
· change (List.insertionSort le l) ++ [i] = List.insertionSort le (l.toList ++ [i])
|
||||
have hoi (l : List 𝓕) (j : 𝓕) : List.orderedInsert le j (l ++ [i]) =
|
||||
List.orderedInsert le 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
|
||||
by_cases hr : le 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
|
||||
have hI (l : List 𝓕) : (List.insertionSort le l) ++ [i] =
|
||||
List.insertionSort le (l ++ [i]) := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons j l ih =>
|
||||
|
|
@ -236,7 +231,7 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
rw [hoi]
|
||||
rw [hI]
|
||||
rfl
|
||||
· have hI (l : List I) : koszulSign r q l = koszulSign r q (l ++ [i]) := by
|
||||
· have hI (l : List 𝓕) : koszulSign q le l = koszulSign q le (l ++ [i]) := by
|
||||
induction l with
|
||||
| nil => simp [koszulSign, koszulSignInsert]
|
||||
| cons j l ih =>
|
||||
|
|
@ -244,7 +239,7 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
|
|||
rw [ih]
|
||||
simp only [mul_eq_mul_right_iff]
|
||||
apply Or.inl
|
||||
rw [koszulSignInsert_ge_forall_append r q l j i hi]
|
||||
rw [koszulSignInsert_ge_forall_append q le l j i hi]
|
||||
rw [hI]
|
||||
rfl
|
||||
rw [h1]
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ 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.CreateAnnilateSection
|
||||
import HepLean.PerturbationTheory.Wick.CreateAnnihilateSection
|
||||
import HepLean.PerturbationTheory.Wick.KoszulOrder
|
||||
/-!
|
||||
|
||||
|
|
@ -13,65 +13,67 @@ import HepLean.PerturbationTheory.Wick.KoszulOrder
|
|||
|
||||
namespace Wick
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
noncomputable section
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
/-- The element of the free algebra `FreeAlgebra ℂ I` associated with a `List I`. -/
|
||||
def ofList {I : Type} (l : List I) (x : ℂ) : FreeAlgebra ℂ I :=
|
||||
def ofList (l : List 𝓕) (x : ℂ) : FreeAlgebra ℂ 𝓕 :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
|
||||
|
||||
lemma ofList_pair {I : Type} (l r : List I) (x y : ℂ) :
|
||||
lemma ofList_pair (l r : List 𝓕) (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 : ℂ) :
|
||||
lemma ofList_triple (la lb lc : List 𝓕) (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 : ℂ) :
|
||||
lemma ofList_triple_assoc (la lb lc : List 𝓕) (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 : ℂ) :
|
||||
lemma ofList_cons_eq_ofList (l : List 𝓕) (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) :
|
||||
lemma ofList_singleton (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 : ℂ) :
|
||||
lemma ofList_eq_smul_one (l : List 𝓕) (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
|
||||
lemma ofList_empty : ofList [] 1 = (1 : FreeAlgebra ℂ 𝓕) := by
|
||||
simp only [ofList, EmbeddingLike.map_eq_one_iff]
|
||||
rfl
|
||||
|
||||
lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra ℂ I) := by
|
||||
lemma ofList_empty' : ofList [] x = x • (1 : FreeAlgebra ℂ 𝓕) := 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
|
||||
lemma koszulOrder_ofList
|
||||
(l : List 𝓕) (x : ℂ) :
|
||||
koszulOrder q le (ofList l x) = (koszulSign q le l) • ofList (List.insertionSort le l) x := by
|
||||
rw [ofList]
|
||||
rw [koszulOrder_single]
|
||||
change ofList (List.insertionSort r l) _ = _
|
||||
change ofList (List.insertionSort le l) _ = _
|
||||
rw [ofList_eq_smul_one]
|
||||
conv_rhs => rw [ofList_eq_smul_one]
|
||||
rw [smul_smul]
|
||||
|
||||
lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r]
|
||||
(q : I → Fin 2) (l : List I) (x : ℂ) :
|
||||
ofList (List.insertionSort r l) x = (koszulSign r q l) • koszulOrder r q (ofList l x) := by
|
||||
lemma ofList_insertionSort_eq_koszulOrder (l : List 𝓕) (x : ℂ) :
|
||||
ofList (List.insertionSort le l) x = (koszulSign q le l) • koszulOrder q le (ofList l x) := by
|
||||
rw [koszulOrder_ofList]
|
||||
rw [smul_smul]
|
||||
rw [koszulSign_mul_self]
|
||||
|
|
@ -80,11 +82,11 @@ lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [Dec
|
|||
/-- The map of algebras from `FreeAlgebra ℂ I` to `FreeAlgebra ℂ (Σ i, f i)` taking
|
||||
the monomial `i` to the sum of elements in `(Σ i, f i)` above `i`, i.e. the sum of the fiber
|
||||
above `i`. -/
|
||||
def sumFiber {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
|
||||
FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
|
||||
def sumFiber (f : 𝓕 → Type) [∀ i, Fintype (f i)] :
|
||||
FreeAlgebra ℂ 𝓕 →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
|
||||
FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
|
||||
|
||||
lemma sumFiber_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
|
||||
lemma sumFiber_ι (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕) :
|
||||
sumFiber f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
|
||||
simp [sumFiber]
|
||||
|
||||
|
|
@ -94,38 +96,38 @@ lemma sumFiber_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
|
|||
For example, in terms of creation and annihlation opperators,
|
||||
`[φ₁, φ₂, φ₃]` gets taken to `(φ₁⁰ + φ₁¹)(φ₂⁰ + φ₂¹)(φ₃⁰ + φ₃¹)`.
|
||||
-/
|
||||
def ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ℂ) :
|
||||
def ofListLift (f : 𝓕 → Type) [∀ i, Fintype (f i)] (l : List 𝓕) (x : ℂ) :
|
||||
FreeAlgebra ℂ (Σ i, f i) :=
|
||||
sumFiber f (ofList l x)
|
||||
|
||||
lemma ofListLift_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
|
||||
lemma ofListLift_empty (f : 𝓕 → Type) [∀ i, Fintype (f i)] :
|
||||
ofListLift f [] 1 = 1 := by
|
||||
simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
|
||||
rw [ofList_empty]
|
||||
exact map_one (sumFiber f)
|
||||
|
||||
lemma ofListLift_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
|
||||
lemma ofListLift_empty_smul (f : 𝓕 → Type) [∀ i, Fintype (f i)] (x : ℂ) :
|
||||
ofListLift f [] x = x • 1 := by
|
||||
simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
|
||||
rw [ofList_eq_smul_one]
|
||||
rw [ofList_empty]
|
||||
simp
|
||||
|
||||
lemma ofListLift_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
|
||||
lemma ofListLift_cons (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕) (r : List 𝓕) (x : ℂ) :
|
||||
ofListLift f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩) * (ofListLift f r x) := by
|
||||
rw [ofListLift, ofList_cons_eq_ofList, ofList_singleton, map_mul]
|
||||
conv_lhs => lhs; rw [sumFiber]
|
||||
rw [ofListLift]
|
||||
simp
|
||||
|
||||
lemma ofListLift_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (x : ℂ) :
|
||||
lemma ofListLift_singleton (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕) (x : ℂ) :
|
||||
ofListLift f [i] x = ∑ j : f i, x • FreeAlgebra.ι ℂ ⟨i, j⟩ := by
|
||||
simp only [ofListLift]
|
||||
rw [ofList_eq_smul_one, ofList_singleton, map_smul]
|
||||
rw [sumFiber_ι]
|
||||
rw [Finset.smul_sum]
|
||||
|
||||
lemma ofListLift_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
|
||||
lemma ofListLift_singleton_one (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕) :
|
||||
ofListLift f [i] 1 = ∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩ := by
|
||||
simp only [ofListLift]
|
||||
rw [ofList_eq_smul_one, ofList_singleton, map_smul]
|
||||
|
|
@ -133,22 +135,22 @@ lemma ofListLift_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)
|
|||
rw [Finset.smul_sum]
|
||||
simp
|
||||
|
||||
lemma ofListLift_cons_eq_ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)
|
||||
(r : List I) (x : ℂ) :
|
||||
lemma ofListLift_cons_eq_ofListLift (f : 𝓕 → Type) [∀ i, Fintype (f i)] (i : 𝓕)
|
||||
(r : List 𝓕) (x : ℂ) :
|
||||
ofListLift f (i :: r) x = ofListLift f [i] 1 * ofListLift f r x := by
|
||||
rw [ofListLift_cons, ofListLift_singleton]
|
||||
simp only [one_smul]
|
||||
|
||||
lemma ofListLift_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
|
||||
(l : List I) → ofListLift f l x = ∑ (a : CreateAnnilateSect f l), ofList a.toList x
|
||||
lemma ofListLift_expand (f : 𝓕 → Type) [∀ i, Fintype (f i)] (x : ℂ) :
|
||||
(l : List 𝓕) → ofListLift f l x = ∑ (a : CreateAnnihilateSect f l), ofList a.toList x
|
||||
| [] => by
|
||||
simp only [ofListLift, CreateAnnilateSect, List.length_nil, List.get_eq_getElem,
|
||||
Finset.univ_unique, CreateAnnilateSect.toList, Finset.sum_const, Finset.card_singleton,
|
||||
simp only [ofListLift, CreateAnnihilateSect, List.length_nil, List.get_eq_getElem,
|
||||
Finset.univ_unique, CreateAnnihilateSect.toList, 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 [ofListLift_cons, ofListLift_expand f x l]
|
||||
conv_rhs => rw [← (CreateAnnilateSect.extractEquiv
|
||||
conv_rhs => rw [← (CreateAnnihilateSect.extractEquiv
|
||||
⟨0, by exact Nat.zero_lt_succ l.length⟩).symm.sum_comp (α := FreeAlgebra ℂ _)]
|
||||
erw [Finset.sum_product]
|
||||
rw [Finset.sum_mul]
|
||||
|
|
@ -163,11 +165,10 @@ lemma ofListLift_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x :
|
|||
rw [← ofList_singleton, ← ofList_pair, one_mul]
|
||||
rfl
|
||||
|
||||
lemma koszulOrder_ofListLift {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) (ofListLift f l x) =
|
||||
sumFiber f (koszulOrder le1 q (ofList l x)) := by
|
||||
lemma koszulOrder_ofListLift {f : 𝓕 → Type} [∀ i, Fintype (f i)]
|
||||
(l : List 𝓕) (x : ℂ) :
|
||||
koszulOrder (fun i => q i.fst) (fun i j => le i.1 j.1) (ofListLift f l x) =
|
||||
sumFiber f (koszulOrder q le (ofList l x)) := by
|
||||
rw [koszulOrder_ofList]
|
||||
rw [map_smul]
|
||||
change _ = _ • ofListLift _ _ _
|
||||
|
|
@ -177,27 +178,26 @@ lemma koszulOrder_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
rhs
|
||||
intro a
|
||||
rw [koszulOrder_ofList]
|
||||
rw [CreateAnnilateSect.toList_koszulSign]
|
||||
rw [CreateAnnihilateSect.toList_koszulSign]
|
||||
rw [← Finset.smul_sum]
|
||||
apply congrArg
|
||||
conv_lhs =>
|
||||
rhs
|
||||
intro n
|
||||
rw [← CreateAnnilateSect.sort_toList]
|
||||
rw [← CreateAnnihilateSect.sort_toList]
|
||||
rw [ofListLift_expand]
|
||||
refine Fintype.sum_equiv
|
||||
((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
|
||||
((HepLean.List.insertionSortEquiv le l).piCongr fun i => Equiv.cast ?_) _ _ ?_
|
||||
congr 1
|
||||
· rw [← HepLean.List.insertionSortEquiv_get]
|
||||
simp
|
||||
· intro x
|
||||
rfl
|
||||
|
||||
lemma koszulOrder_ofListLift_eq_ofListLift {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)
|
||||
lemma koszulOrder_ofListLift_eq_ofListLift {f : 𝓕 → Type} [∀ i, Fintype (f i)]
|
||||
(l : List 𝓕) (x : ℂ) : koszulOrder (fun i => q i.fst) (fun i j => le i.1 j.1)
|
||||
(ofListLift f l x) =
|
||||
koszulSign le1 q l • ofListLift f (List.insertionSort le1 l) x := by
|
||||
koszulSign q le l • ofListLift f (List.insertionSort le l) x := by
|
||||
rw [koszulOrder_ofListLift, koszulOrder_ofList, map_smul]
|
||||
rfl
|
||||
|
||||
|
|
|
|||
|
|
@ -6,17 +6,19 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.PerturbationTheory.Wick.SuperCommute
|
||||
/-!
|
||||
|
||||
# Koszul signs and ordering for lists and algebras
|
||||
# Operator map
|
||||
|
||||
See e.g.
|
||||
- https://pcteserver.mi.infn.it/~molinari/NOTES/WICK23.pdf
|
||||
-/
|
||||
|
||||
namespace Wick
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- A map from the free algebra of fields `FreeAlgebra ℂ I` to an algebra `A`, to be
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type}
|
||||
|
||||
/-- A map from the free algebra of fields `FreeAlgebra ℂ 𝓕` to an algebra `A`, to be
|
||||
thought of as the operator algebra is said to be an operator map if
|
||||
all super commutors of fields land in the center of `A`,
|
||||
if two fields are of a different grade then their super commutor lands on zero,
|
||||
|
|
@ -24,21 +26,23 @@ noncomputable section
|
|||
is zero.
|
||||
This can be thought as as a condtion on the operator algebra `A` as much as it can
|
||||
on `F`. -/
|
||||
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A] (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A) : Prop where
|
||||
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
|
||||
[DecidableRel le] (F : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A) : Prop where
|
||||
superCommute_mem_center : ∀ i j, F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) ∈
|
||||
Subalgebra.center ℂ A
|
||||
superCommute_diff_grade_zero : ∀ i j, q i ≠ q j →
|
||||
F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) = 0
|
||||
superCommute_ordered_zero : ∀ i j, ∀ a b,
|
||||
F (koszulOrder le1 q (a * superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) * b)) = 0
|
||||
F (koszulOrder q le (a * superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) * b)) = 0
|
||||
|
||||
namespace OperatorMap
|
||||
|
||||
variable {A : Type} [Semiring A] [Algebra ℂ A] {q : I → Fin 2} {le1 : I → I → Prop}
|
||||
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A)
|
||||
variable {A : Type} [Semiring A] [Algebra ℂ A]
|
||||
{q : 𝓕 → FieldStatistic} {le : 𝓕 → 𝓕 → Prop}
|
||||
[DecidableRel le] (F : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A)
|
||||
|
||||
lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
|
||||
lemma superCommute_ofList_singleton_ι_center [OperatorMap q le F] (i j : 𝓕) :
|
||||
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
|
||||
|
|
@ -49,22 +53,22 @@ lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
|
|||
rfl
|
||||
rw [h1]
|
||||
refine Subalgebra.smul_mem (Subalgebra.center ℂ A) ?_ xa
|
||||
exact superCommute_mem_center (le1 := le1) i j
|
||||
exact superCommute_mem_center (le := le) i j
|
||||
|
||||
end OperatorMap
|
||||
|
||||
lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
|
||||
(le1 : I → I → Prop) [DecidableRel le1]
|
||||
(lb : List I) (xa xb : ℂ) (n : ℕ)
|
||||
(hn : n < lb.length) {A : Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ I →ₐ[ℂ] A)
|
||||
[OperatorMap q le1 f] (i : I) :
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
lemma superCommuteSplit_operatorMap (lb : List 𝓕) (xa xb : ℂ) (n : ℕ)
|
||||
(hn : n < lb.length) {A : Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A)
|
||||
[OperatorMap q le f] (i : 𝓕) :
|
||||
f (superCommuteSplit 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 :=
|
||||
OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) f i (lb.get ⟨n, hn⟩)
|
||||
OperatorMap.superCommute_ofList_singleton_ι_center (le := le) f i (lb.get ⟨n, hn⟩)
|
||||
rw [Subalgebra.mem_center_iff] at hn
|
||||
rw [superCommuteSplit, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
|
||||
← map_mul, ← ofList_pair]
|
||||
|
|
@ -72,12 +76,12 @@ lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
|
|||
· exact Eq.symm (List.eraseIdx_eq_take_drop_succ lb n)
|
||||
· exact one_mul xb
|
||||
|
||||
lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (c : (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
|
||||
lemma superCommuteLiftSplit_operatorMap {f : 𝓕 → Type} [∀ i, Fintype (f i)]
|
||||
(c : (Σ i, f i)) (r : List 𝓕) (x y : ℂ) (n : ℕ)
|
||||
(hn : n < r.length)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
|
||||
[OperatorMap (fun i => q i.1) le1 F] :
|
||||
[OperatorMap (fun i => q i.1) le F] :
|
||||
F (superCommuteLiftSplit q [c] r x y n hn) = superCommuteLiftCoef q [c] (List.take n r) •
|
||||
(F (superCommute (fun i => q i.1) (ofList [c] x)
|
||||
(sumFiber f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
|
||||
|
|
@ -92,7 +96,7 @@ lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fint
|
|||
rw [map_sum, map_sum]
|
||||
refine Subalgebra.sum_mem _ ?_
|
||||
intro n
|
||||
exact fun a => OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) F c _
|
||||
exact fun a => OperatorMap.superCommute_ofList_singleton_ι_center (le := le) F c _
|
||||
rw [Subalgebra.mem_center_iff] at h1
|
||||
rw [h1, mul_assoc, ← map_mul]
|
||||
congr
|
||||
|
|
@ -102,30 +106,27 @@ lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fint
|
|||
congr
|
||||
exact Eq.symm (List.eraseIdx_eq_take_drop_succ r n)
|
||||
|
||||
lemma superCommute_koszulOrder_le_ofList {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (x : ℂ)
|
||||
(le1 :I → I → Prop) [DecidableRel le1] [IsTotal I le1] [IsTrans I le1]
|
||||
(i : I)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ A) [OperatorMap q le1 F] :
|
||||
F ((superCommute q (FreeAlgebra.ι ℂ i) (koszulOrder le1 q (ofList r x)))) =
|
||||
lemma superCommute_koszulOrder_le_ofList [IsTotal 𝓕 le] [IsTrans 𝓕 le] (r : List 𝓕) (x : ℂ)
|
||||
(i : 𝓕) {A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ A) [OperatorMap q le F] :
|
||||
F ((superCommute q (FreeAlgebra.ι ℂ i) (koszulOrder q le (ofList r x)))) =
|
||||
∑ n : Fin r.length, (superCommuteCoef q [r.get n] (r.take n)) •
|
||||
(F (((superCommute q) (ofList [i] 1)) (FreeAlgebra.ι ℂ (r.get n))) *
|
||||
F ((koszulOrder le1 q) (ofList (r.eraseIdx ↑n) x))) := by
|
||||
F ((koszulOrder q le) (ofList (r.eraseIdx ↑n) x))) := by
|
||||
rw [koszulOrder_ofList, map_smul, map_smul, ← ofList_singleton, superCommute_ofList_sum]
|
||||
rw [map_sum, ← (HepLean.List.insertionSortEquiv le1 r).sum_comp]
|
||||
rw [map_sum, ← (HepLean.List.insertionSortEquiv le r).sum_comp]
|
||||
conv_lhs =>
|
||||
enter [2, 2]
|
||||
intro n
|
||||
rw [superCommuteSplit_operatorMap (le1 := le1)]
|
||||
rw [superCommuteSplit_operatorMap (le := le)]
|
||||
enter [1, 2, 2, 2]
|
||||
change ((List.insertionSort le1 r).get ∘ (HepLean.List.insertionSortEquiv le1 r)) n
|
||||
change ((List.insertionSort le r).get ∘ (HepLean.List.insertionSortEquiv le r)) n
|
||||
rw [HepLean.List.insertionSort_get_comp_insertionSortEquiv]
|
||||
conv_lhs =>
|
||||
enter [2, 2]
|
||||
intro n
|
||||
rw [HepLean.List.eraseIdx_insertionSort_fin le1 r n]
|
||||
rw [ofList_insertionSort_eq_koszulOrder le1 q]
|
||||
rw [HepLean.List.eraseIdx_insertionSort_fin le r n]
|
||||
rw [ofList_insertionSort_eq_koszulOrder q le]
|
||||
rw [Finset.smul_sum]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
|
|
@ -134,7 +135,7 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
|
|||
congr
|
||||
funext n
|
||||
by_cases hq : q i ≠ q (r.get n)
|
||||
· have hn := OperatorMap.superCommute_diff_grade_zero (q := q) (F := F) le1 i (r.get n) hq
|
||||
· have hn := OperatorMap.superCommute_diff_grade_zero (q := q) (F := F) le i (r.get n) hq
|
||||
conv_lhs =>
|
||||
enter [2, 1]
|
||||
rw [ofList_singleton, hn]
|
||||
|
|
@ -143,18 +144,16 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
|
|||
rw [ofList_singleton, hn]
|
||||
simp
|
||||
· congr 1
|
||||
trans staticWickCoef q le1 r i n
|
||||
trans staticWickCoef q le r i n
|
||||
· rw [staticWickCoef, mul_assoc]
|
||||
refine staticWickCoef_eq_get q le1 r i n ?_
|
||||
refine staticWickCoef_eq_get q le r i n ?_
|
||||
simpa using hq
|
||||
|
||||
lemma koszulOrder_of_le_all_ofList {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (x : ℂ) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(i : I)
|
||||
lemma koszulOrder_of_le_all_ofList (r : List 𝓕) (x : ℂ) (i : 𝓕)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ A) [OperatorMap q le1 F] :
|
||||
F (koszulOrder le1 q (ofList r x * FreeAlgebra.ι ℂ i))
|
||||
= superCommuteCoef q [i] r • F (koszulOrder le1 q (FreeAlgebra.ι ℂ i * ofList r x)) := by
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ A) [OperatorMap q le F] :
|
||||
F (koszulOrder q le (ofList r x * FreeAlgebra.ι ℂ i))
|
||||
= superCommuteCoef q [i] r • F (koszulOrder q le (FreeAlgebra.ι ℂ i * ofList r x)) := by
|
||||
conv_lhs =>
|
||||
enter [2, 2]
|
||||
rw [← ofList_singleton]
|
||||
|
|
@ -182,14 +181,13 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
|
|||
simp only [smul_zero, Finset.sum_const_zero, add_zero]
|
||||
rw [ofList_singleton]
|
||||
|
||||
lemma le_all_mul_koszulOrder_ofList {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (x : ℂ) (le1 : I → I→ Prop) [DecidableRel le1]
|
||||
(i : I) (hi : ∀ (j : I), le1 j i)
|
||||
lemma le_all_mul_koszulOrder_ofList (r : List 𝓕) (x : ℂ)
|
||||
(i : 𝓕) (hi : ∀ (j : 𝓕), le j i)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ A) [OperatorMap q le1 F] :
|
||||
F (FreeAlgebra.ι ℂ i * koszulOrder le1 q (ofList r x)) =
|
||||
F ((koszulOrder le1 q) (FreeAlgebra.ι ℂ i * ofList r x)) +
|
||||
F (((superCommute q) (ofList [i] 1)) ((koszulOrder le1 q) (ofList r x))) := by
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ A) [OperatorMap q le F] :
|
||||
F (FreeAlgebra.ι ℂ i * koszulOrder q le (ofList r x)) =
|
||||
F ((koszulOrder q le) (FreeAlgebra.ι ℂ i * ofList r x)) +
|
||||
F (((superCommute q) (ofList [i] 1)) ((koszulOrder q le) (ofList r x))) := by
|
||||
rw [koszulOrder_ofList, Algebra.mul_smul_comm, map_smul, ← ofList_singleton,
|
||||
ofList_ofList_superCommute q, map_add, smul_add, ← map_smul]
|
||||
conv_lhs =>
|
||||
|
|
@ -199,20 +197,19 @@ lemma le_all_mul_koszulOrder_ofList {I : Type}
|
|||
rw [koszulOrder_mul_ge, map_smul]
|
||||
congr
|
||||
· rw [koszulOrder_of_le_all_ofList]
|
||||
rw [superCommuteCoef_perm_snd q [i] (List.insertionSort le1 r) r
|
||||
(List.perm_insertionSort le1 r)]
|
||||
rw [superCommuteCoef_perm_snd q [i] (List.insertionSort le r) r
|
||||
(List.perm_insertionSort le r)]
|
||||
rw [smul_smul]
|
||||
rw [superCommuteCoef_mul_self]
|
||||
simp [ofList_singleton]
|
||||
· rw [map_smul, map_smul]
|
||||
· exact fun j => hi j
|
||||
|
||||
/-- In the expansions of `F (FreeAlgebra.ι ℂ i * koszulOrder le1 q (ofList r x))`
|
||||
the ter multiplying `F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x))`. -/
|
||||
def superCommuteCenterOrder {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (i : I)
|
||||
/-- In the expansions of `F (FreeAlgebra.ι ℂ i * koszulOrder q le (ofList r x))`
|
||||
the ter multiplying `F ((koszulOrder q le) (ofList (optionEraseZ r i n) x))`. -/
|
||||
def superCommuteCenterOrder (r : List 𝓕) (i : 𝓕)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ[ℂ] A)
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A)
|
||||
(n : Option (Fin r.length)) : A :=
|
||||
match n with
|
||||
| none => 1
|
||||
|
|
@ -220,24 +217,21 @@ def superCommuteCenterOrder {I : Type}
|
|||
(FreeAlgebra.ι ℂ (r.get n)))
|
||||
|
||||
@[simp]
|
||||
lemma superCommuteCenterOrder_none {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (i : I)
|
||||
lemma superCommuteCenterOrder_none (r : List 𝓕) (i : 𝓕)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ[ℂ] A) :
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A) :
|
||||
superCommuteCenterOrder q r i F none = 1 := by
|
||||
simp [superCommuteCenterOrder]
|
||||
|
||||
open HepLean.List
|
||||
|
||||
lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (x : ℂ) (le1 : I → I→ Prop) [DecidableRel le1]
|
||||
[IsTotal I le1] [IsTrans I le1]
|
||||
(i : I) (hi : ∀ (j : I), le1 j i)
|
||||
lemma le_all_mul_koszulOrder_ofList_expand [IsTotal 𝓕 le] [IsTrans 𝓕 le] (r : List 𝓕) (x : ℂ)
|
||||
(i : 𝓕) (hi : ∀ (j : 𝓕), le j i)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ I →ₐ[ℂ] A) [OperatorMap q le1 F] :
|
||||
F (FreeAlgebra.ι ℂ i * koszulOrder le1 q (ofList r x)) =
|
||||
(F : FreeAlgebra ℂ 𝓕 →ₐ[ℂ] A) [OperatorMap q le F] :
|
||||
F (FreeAlgebra.ι ℂ i * koszulOrder q le (ofList r x)) =
|
||||
∑ n, superCommuteCenterOrder q r i F n *
|
||||
F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x)) := by
|
||||
F ((koszulOrder q le) (ofList (optionEraseZ r i n) x)) := by
|
||||
rw [le_all_mul_koszulOrder_ofList]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
|
|
@ -253,17 +247,18 @@ lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
|
|||
rfl
|
||||
exact fun j => hi j
|
||||
|
||||
lemma le_all_mul_koszulOrder_ofListLift_expand {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]
|
||||
[IsTotal (Σ i, f i) le1] [IsTrans (Σ i, f i) le1]
|
||||
(i : (Σ i, f i)) (hi : ∀ (j : (Σ i, f i)), le1 j i)
|
||||
lemma le_all_mul_koszulOrder_ofListLift_expand {f : 𝓕 → Type} [∀ i, Fintype (f i)]
|
||||
(r : List 𝓕) (x : ℂ)
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
[IsTotal (Σ i, f i) le] [IsTrans (Σ i, f i) le]
|
||||
(i : (Σ i, f i)) (hi : ∀ (j : (Σ i, f i)), le j i)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
|
||||
F (ofList [i] 1 * koszulOrder le1 (fun i => q i.1) (ofListLift f r x)) =
|
||||
F ((koszulOrder le1 fun i => q i.fst) (ofList [i] 1 * ofListLift f r x)) +
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F] :
|
||||
F (ofList [i] 1 * koszulOrder (fun i => q i.1) le (ofListLift f r x)) =
|
||||
F ((koszulOrder (fun i => q i.fst) le) (ofList [i] 1 * ofListLift f r x)) +
|
||||
∑ n : (Fin r.length), superCommuteCoef q [r.get n] (List.take (↑n) r) •
|
||||
F (((superCommute fun i => q i.fst) (ofList [i] 1)) (ofListLift f [r.get n] 1)) *
|
||||
F ((koszulOrder le1 fun i => q i.fst) (ofListLift f (r.eraseIdx ↑n) x)) := by
|
||||
F ((koszulOrder (fun i => q i.fst) le) (ofListLift f (r.eraseIdx ↑n) x)) := by
|
||||
match r with
|
||||
| [] =>
|
||||
simp only [map_mul, List.length_nil, Finset.univ_eq_empty, List.get_eq_getElem, List.take_nil,
|
||||
|
|
@ -273,9 +268,9 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
|
|||
rw [ofList_singleton, koszulOrder_ι]
|
||||
| r0 :: r =>
|
||||
rw [ofListLift_expand, map_sum, Finset.mul_sum, map_sum]
|
||||
let e1 (a : CreateAnnilateSect f (r0 :: r)) :
|
||||
let e1 (a : CreateAnnihilateSect f (r0 :: r)) :
|
||||
Option (Fin a.toList.length) ≃ Option (Fin (r0 :: r).length) :=
|
||||
Equiv.optionCongr (Fin.castOrderIso (CreateAnnilateSect.toList_length a)).toEquiv
|
||||
Equiv.optionCongr (Fin.castOrderIso (CreateAnnihilateSect.toList_length a)).toEquiv
|
||||
conv_lhs =>
|
||||
rhs
|
||||
intro a
|
||||
|
|
@ -297,25 +292,25 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
|
|||
rw [ofList_cons_eq_ofList]
|
||||
· congr
|
||||
funext n
|
||||
rw [← (CreateAnnilateSect.extractEquiv n).symm.sum_comp]
|
||||
rw [← (CreateAnnihilateSect.extractEquiv n).symm.sum_comp]
|
||||
simp only [List.get_eq_getElem, List.length_cons, Equiv.optionCongr_symm, OrderIso.toEquiv_symm,
|
||||
Fin.symm_castOrderIso, Equiv.optionCongr_apply, RelIso.coe_fn_toEquiv, Option.map_some',
|
||||
Fin.castOrderIso_apply, Algebra.smul_mul_assoc, e1]
|
||||
erw [Finset.sum_product]
|
||||
have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
|
||||
have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnihilateSect f ((r0 :: r).eraseIdx ↑n)) :
|
||||
superCommuteCenterOrder (fun i => q i.fst)
|
||||
((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
|
||||
((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList i F
|
||||
(some (Fin.cast (by simp) n)) =
|
||||
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
|
||||
F (((superCommute fun i => q i.fst) (ofList [i] 1))
|
||||
(FreeAlgebra.ι ℂ ⟨(r0 :: r).get n, a0⟩)) := by
|
||||
simp only [superCommuteCenterOrder, List.get_eq_getElem, List.length_cons, Fin.coe_cast]
|
||||
erw [CreateAnnilateSect.extractEquiv_symm_toList_get_same]
|
||||
erw [CreateAnnihilateSect.extractEquiv_symm_toList_get_same]
|
||||
have hsc : superCommuteCoef (fun i => q i.fst) [⟨(r0 :: r).get n, a0⟩]
|
||||
(List.take (↑n) ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
|
||||
(List.take (↑n) ((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList) =
|
||||
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
|
||||
simp only [superCommuteCoef, List.get_eq_getElem, List.length_cons, Fin.isValue,
|
||||
CreateAnnilateSect.toList_grade_take]
|
||||
CreateAnnihilateSect.toList_grade_take]
|
||||
rfl
|
||||
erw [hsc]
|
||||
rfl
|
||||
|
|
@ -329,18 +324,15 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
|
|||
rhs
|
||||
intro a0
|
||||
rw [← Finset.mul_sum]
|
||||
|
||||
conv_lhs =>
|
||||
rhs
|
||||
intro a0
|
||||
enter [2, 2]
|
||||
intro a
|
||||
simp [optionEraseZ]
|
||||
rhs
|
||||
rhs
|
||||
lhs
|
||||
rw [← CreateAnnilateSect.eraseIdx_toList]
|
||||
erw [CreateAnnilateSect.extractEquiv_symm_eraseIdx]
|
||||
enter [2, 2, 1]
|
||||
rw [← CreateAnnihilateSect.eraseIdx_toList]
|
||||
erw [CreateAnnihilateSect.extractEquiv_symm_eraseIdx]
|
||||
rw [← Finset.sum_mul]
|
||||
conv_lhs =>
|
||||
lhs
|
||||
|
|
|
|||
|
|
@ -1,102 +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
|
||||
/-!
|
||||
|
||||
# Koszul sign insert
|
||||
|
||||
-/
|
||||
|
||||
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
|
||||
|
|
@ -7,17 +7,21 @@ import HepLean.Mathematics.List
|
|||
import HepLean.PerturbationTheory.Wick.Signs.SuperCommuteCoef
|
||||
/-!
|
||||
|
||||
# Koszul signs and ordering for lists and algebras
|
||||
# Insert sign
|
||||
|
||||
-/
|
||||
|
||||
namespace Wick
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
/-- The sign associated with inserting `r0` into `r` at the position `n`.
|
||||
That is the sign associated with commuting `r0` with `List.take n r`. -/
|
||||
def insertSign {I : Type} (q : I → Fin 2) (n : ℕ) (r0 : I) (r : List I) : ℂ :=
|
||||
superCommuteCoef q [r0] (List.take n r)
|
||||
section
|
||||
/-!
|
||||
|
||||
## Basic properties of lists
|
||||
|
||||
To be replaced with Mathlib or Lean definitions when/where appropraite.
|
||||
-/
|
||||
|
||||
lemma take_insert_same {I : Type} (i : I) :
|
||||
(n : ℕ) → (r : List I) →
|
||||
|
|
@ -28,12 +32,6 @@ lemma take_insert_same {I : Type} (i : I) :
|
|||
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
|
||||
exact take_insert_same i n as
|
||||
|
||||
lemma insertSign_insert {I : Type} (q : I → Fin 2) (n : ℕ)
|
||||
(r0 : I) (r : List I) : insertSign q n r0 r = insertSign q n r0 (List.insertIdx n r0 r) := by
|
||||
simp only [insertSign]
|
||||
congr 1
|
||||
rw [take_insert_same]
|
||||
|
||||
lemma take_eraseIdx_same {I : Type} :
|
||||
(n : ℕ) → (r : List I) →
|
||||
List.take n (List.eraseIdx r n) = List.take n r
|
||||
|
|
@ -43,22 +41,6 @@ lemma take_eraseIdx_same {I : Type} :
|
|||
simp only [List.eraseIdx_cons_succ, List.take_succ_cons, List.cons.injEq, true_and]
|
||||
exact take_eraseIdx_same n as
|
||||
|
||||
lemma insertSign_eraseIdx {I : Type} (q : I → Fin 2) (n : ℕ)
|
||||
(r0 : I) (r : List I) : insertSign q n r0 (r.eraseIdx n) = insertSign q n r0 r := by
|
||||
simp only [insertSign]
|
||||
congr 1
|
||||
rw [take_eraseIdx_same]
|
||||
|
||||
lemma insertSign_zero {I : Type} (q : I → Fin 2) (r0 : I) (r : List I) :
|
||||
insertSign q 0 r0 r = 1 := by
|
||||
simp [insertSign, superCommuteCoef]
|
||||
|
||||
lemma insertSign_succ_cons {I : Type} (q : I → Fin 2) (n : ℕ)
|
||||
(r0 r1 : I) (r : List I) : insertSign q (n + 1) r0 (r1 :: r) =
|
||||
superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
|
||||
simp only [insertSign, List.take_succ_cons]
|
||||
rw [superCommuteCoef_cons]
|
||||
|
||||
lemma take_insert_gt {I : Type} (i : I) :
|
||||
(n m : ℕ) → (h : n < m) → (r : List I) →
|
||||
List.take n (List.insertIdx m i r) = List.take n r
|
||||
|
|
@ -69,13 +51,6 @@ lemma take_insert_gt {I : Type} (i : I) :
|
|||
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
|
||||
refine take_insert_gt i n m (Nat.succ_lt_succ_iff.mp h) as
|
||||
|
||||
lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : ℕ)
|
||||
(r0 r1 : I) (r : List I) (hn : n < m) :
|
||||
insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
|
||||
rw [insertSign, insertSign]
|
||||
congr 1
|
||||
exact take_insert_gt r1 n m hn r
|
||||
|
||||
lemma take_insert_let {I : Type} (i : I) :
|
||||
(n m : ℕ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
|
||||
(List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)
|
||||
|
|
@ -91,20 +66,64 @@ lemma take_insert_let {I : Type} (i : I) :
|
|||
refine List.Perm.cons a ?_
|
||||
exact take_insert_let i n m (Nat.le_of_succ_le_succ h) as (Nat.le_of_succ_le_succ hm)
|
||||
|
||||
lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : ℕ)
|
||||
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
|
||||
end
|
||||
|
||||
/-!
|
||||
|
||||
## Insert sign
|
||||
|
||||
-/
|
||||
|
||||
section InsertSign
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic)
|
||||
|
||||
/-- The sign associated with inserting `r0` into `r` at the position `n`.
|
||||
That is the sign associated with commuting `r0` with `List.take n r`. -/
|
||||
def insertSign (n : ℕ) (r0 : 𝓕) (r : List 𝓕) : ℂ :=
|
||||
superCommuteCoef q [r0] (List.take n r)
|
||||
|
||||
lemma insertSign_insert (n : ℕ) (r0 : 𝓕) (r : List 𝓕) :
|
||||
insertSign q n r0 r = insertSign q n r0 (List.insertIdx n r0 r) := by
|
||||
simp only [insertSign]
|
||||
congr 1
|
||||
rw [take_insert_same]
|
||||
|
||||
lemma insertSign_eraseIdx (n : ℕ) (r0 : 𝓕) (r : List 𝓕) :
|
||||
insertSign q n r0 (r.eraseIdx n) = insertSign q n r0 r := by
|
||||
simp only [insertSign]
|
||||
congr 1
|
||||
rw [take_eraseIdx_same]
|
||||
|
||||
lemma insertSign_zero (r0 : 𝓕) (r : List 𝓕) : insertSign q 0 r0 r = 1 := by
|
||||
simp [insertSign, superCommuteCoef]
|
||||
|
||||
lemma insertSign_succ_cons (n : ℕ) (r0 r1 : 𝓕) (r : List 𝓕) : insertSign q (n + 1) r0 (r1 :: r) =
|
||||
superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
|
||||
simp only [insertSign, List.take_succ_cons]
|
||||
rw [superCommuteCoef_cons]
|
||||
|
||||
lemma insertSign_insert_gt (n m : ℕ) (r0 r1 : 𝓕) (r : List 𝓕) (hn : n < m) :
|
||||
insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
|
||||
rw [insertSign, insertSign]
|
||||
congr 1
|
||||
exact take_insert_gt r1 n m hn r
|
||||
|
||||
lemma insertSign_insert_lt_eq_insertSort (n m : ℕ) (r0 r1 : 𝓕) (r : List 𝓕) (hn : m ≤ n)
|
||||
(hm : m ≤ r.length) :
|
||||
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = insertSign q (n + 1) r0 (r1 :: r) := by
|
||||
rw [insertSign, insertSign]
|
||||
apply superCommuteCoef_perm_snd
|
||||
simp only [List.take_succ_cons]
|
||||
refine take_insert_let r1 n m hn r hm
|
||||
|
||||
lemma insertSign_insert_lt {I : Type} (q : I → Fin 2) (n m : ℕ)
|
||||
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
|
||||
lemma insertSign_insert_lt (n m : ℕ) (r0 r1 : 𝓕) (r : List 𝓕) (hn : m ≤ n) (hm : m ≤ r.length) :
|
||||
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] *
|
||||
insertSign q n r0 r := by
|
||||
rw [insertSign_insert_lt_eq_insertSort, insertSign_succ_cons]
|
||||
exact hn
|
||||
exact hm
|
||||
|
||||
end InsertSign
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -9,61 +9,62 @@ import Mathlib.Analysis.Complex.Basic
|
|||
import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
|
||||
/-!
|
||||
|
||||
# Koszul sign insert
|
||||
# Koszul sign
|
||||
|
||||
-/
|
||||
|
||||
namespace Wick
|
||||
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
/-- 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 → ℂ
|
||||
def koszulSign (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] :
|
||||
List 𝓕 → ℂ
|
||||
| [] => 1
|
||||
| a :: l => koszulSignInsert r q a l * koszulSign r q l
|
||||
| a :: l => koszulSignInsert q le a l * koszulSign q le l
|
||||
|
||||
lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(l : List I) : koszulSign r q l * koszulSign r q l = 1 := by
|
||||
lemma koszulSign_mul_self (l : List 𝓕) : koszulSign q le l * koszulSign q le l = 1 := by
|
||||
induction l with
|
||||
| nil => simp [koszulSign]
|
||||
| cons a l ih =>
|
||||
simp only [koszulSign]
|
||||
trans (koszulSignInsert r q a l * koszulSignInsert r q a l) *
|
||||
(koszulSign r q l * koszulSign r q l)
|
||||
trans (koszulSignInsert q le a l * koszulSignInsert q le a l) *
|
||||
(koszulSign q le l * koszulSign q le l)
|
||||
ring
|
||||
rw [ih]
|
||||
rw [koszulSignInsert_mul_self, mul_one]
|
||||
|
||||
@[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
|
||||
lemma koszulSign_freeMonoid_of (i : 𝓕) : koszulSign q le (FreeMonoid.of i) = 1 := by
|
||||
change koszulSign q le [i] = 1
|
||||
simp only [koszulSign, mul_one]
|
||||
rfl
|
||||
|
||||
lemma koszulSignInsert_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
|
||||
[DecidableRel le1] (r0 : I) :
|
||||
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
|
||||
koszulSignInsert le1 q r0 (r.eraseIdx n) = koszulSignInsert le1 q r0 r
|
||||
lemma koszulSignInsert_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic)
|
||||
(le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (r0 : 𝓕) :
|
||||
(r : List 𝓕) → (n : Fin r.length) → (heq : q (r.get n) = bosonic) →
|
||||
koszulSignInsert q le r0 (r.eraseIdx n) = koszulSignInsert q le r0 r
|
||||
| [], _, _ => by
|
||||
simp
|
||||
| r1 :: r, ⟨0, h⟩, hr => by
|
||||
simp only [List.eraseIdx_zero, List.tail_cons]
|
||||
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
|
||||
List.getElem_cons_zero, Fin.isValue] at hr
|
||||
List.getElem_cons_zero] at hr
|
||||
rw [koszulSignInsert]
|
||||
simp [hr]
|
||||
| r1 :: r, ⟨n + 1, h⟩, hr => by
|
||||
simp only [List.eraseIdx_cons_succ]
|
||||
rw [koszulSignInsert, koszulSignInsert]
|
||||
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
|
||||
rw [koszulSignInsert_erase_boson q le r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
|
||||
|
||||
lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
|
||||
[DecidableRel le1] :
|
||||
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
|
||||
koszulSign le1 q (r.eraseIdx n) = koszulSign le1 q r
|
||||
lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
|
||||
[DecidableRel le] :
|
||||
(r : List 𝓕) → (n : Fin r.length) → (heq : q (r.get n) = bosonic) →
|
||||
koszulSign q le (r.eraseIdx n) = koszulSign q le r
|
||||
| [], _ => by
|
||||
simp
|
||||
| r0 :: r, ⟨0, h⟩ => by
|
||||
|
|
@ -77,20 +78,17 @@ lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop
|
|||
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
|
||||
List.eraseIdx_cons_succ]
|
||||
intro h'
|
||||
rw [koszulSign, koszulSign]
|
||||
rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
|
||||
rw [koszulSign, koszulSign, koszulSign_erase_boson q le r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
|
||||
congr 1
|
||||
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
|
||||
rw [koszulSignInsert_erase_boson q le r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
|
||||
exact h'
|
||||
|
||||
lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
|
||||
koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
|
||||
* koszulSign le1 q r
|
||||
* insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
|
||||
lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (i : 𝓕) :
|
||||
(r : List 𝓕) → (n : ℕ) → (hn : n ≤ r.length) →
|
||||
koszulSign q le (List.insertIdx n i r) = insertSign q n i r * koszulSign q le r *
|
||||
insertSign q (insertionSortEquiv le (List.insertIdx n i r) ⟨n, by
|
||||
rw [List.length_insertIdx _ _ hn]
|
||||
omega⟩) i
|
||||
(List.insertionSort le1 (List.insertIdx n i r))
|
||||
omega⟩) i (List.insertionSort le (List.insertIdx n i r))
|
||||
| [], 0, h => by
|
||||
simp [koszulSign, insertSign, superCommuteCoef, koszulSignInsert]
|
||||
| [], n + 1, h => by
|
||||
|
|
@ -98,7 +96,7 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
| r0 :: r, 0, h => by
|
||||
simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
|
||||
rw [koszulSign]
|
||||
trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
|
||||
trans koszulSign q le (r0 :: r) * koszulSignInsert q le i (r0 :: r)
|
||||
ring
|
||||
simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
|
||||
orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, HepLean.Fin.equivCons_trans,
|
||||
|
|
@ -112,9 +110,9 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
conv_rhs =>
|
||||
rhs
|
||||
rw [← insertSign_insert]
|
||||
change insertSign q (↑(orderedInsertPos le1 ((List.insertionSort le1 (r0 :: r))) i)) i
|
||||
(List.insertionSort le1 (r0 :: r))
|
||||
rw [← koszulSignInsert_eq_insertSign q le1]
|
||||
change insertSign q (↑(orderedInsertPos le ((List.insertionSort le (r0 :: r))) i)) i
|
||||
(List.insertionSort le (r0 :: r))
|
||||
rw [← koszulSignInsert_eq_insertSign q le]
|
||||
rw [insertSign_zero]
|
||||
simp
|
||||
| r0 :: r, n + 1, h => by
|
||||
|
|
@ -142,21 +140,21 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
conv_rhs =>
|
||||
rw [mul_assoc, mul_assoc]
|
||||
congr 1
|
||||
let rs := (List.insertionSort le1 (List.insertIdx n i r))
|
||||
let rs := (List.insertionSort le (List.insertIdx n i r))
|
||||
have hnsL : n < (List.insertIdx n i r).length := by
|
||||
rw [List.length_insertIdx _ _]
|
||||
simp only [List.length_cons, add_le_add_iff_right] at h
|
||||
omega
|
||||
exact Nat.le_of_lt_succ h
|
||||
let ni : Fin rs.length := (insertionSortEquiv le1 (List.insertIdx n i r))
|
||||
let ni : Fin rs.length := (insertionSortEquiv le (List.insertIdx n i r))
|
||||
⟨n, hnsL⟩
|
||||
let nro : Fin (rs.length + 1) :=
|
||||
⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
|
||||
⟨↑(orderedInsertPos le rs r0), orderedInsertPos_lt_length le rs r0⟩
|
||||
rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
|
||||
trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
|
||||
trans koszulSignInsert q le r0 r * (koszulSignCons q le r0 i *insertSign q ni i rs)
|
||||
· simp only [rs, ni]
|
||||
ring
|
||||
trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
|
||||
trans koszulSignInsert q le r0 r * (superCommuteCoef q [i] [r0] *
|
||||
insertSign q (nro.succAbove ni) i (List.insertIdx nro r0 rs))
|
||||
swap
|
||||
· simp only [rs, nro, ni]
|
||||
|
|
@ -168,15 +166,15 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
rw [← insertionSortEquiv_get]
|
||||
simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
|
||||
simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
|
||||
have hc1 : ni.castSucc < nro → ¬ le1 r0 i := by
|
||||
have hc1 : ni.castSucc < nro → ¬ le r0 i := by
|
||||
intro hninro
|
||||
rw [← hns]
|
||||
exact lt_orderedInsertPos_rel le1 r0 rs ni hninro
|
||||
have hc2 : ¬ ni.castSucc < nro → le1 r0 i := by
|
||||
exact lt_orderedInsertPos_rel le r0 rs ni hninro
|
||||
have hc2 : ¬ ni.castSucc < nro → le r0 i := by
|
||||
intro hninro
|
||||
rw [← hns]
|
||||
refine gt_orderedInsertPos_rel le1 r0 rs ?_ ni hninro
|
||||
exact List.sorted_insertionSort le1 (List.insertIdx n i r)
|
||||
refine gt_orderedInsertPos_rel le r0 rs ?_ ni hninro
|
||||
exact List.sorted_insertionSort le (List.insertIdx n i r)
|
||||
by_cases hn : ni.castSucc < nro
|
||||
· simp only [hn, ↓reduceIte, Fin.coe_castSucc]
|
||||
rw [insertSign_insert_gt]
|
||||
|
|
@ -187,14 +185,12 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
simp only [hc1 hn, ↓reduceIte]
|
||||
rw [superCommuteCoef_comm]
|
||||
· simp only [hn, ↓reduceIte, Fin.val_succ]
|
||||
rw [insertSign_insert_lt]
|
||||
rw [← mul_assoc]
|
||||
rw [insertSign_insert_lt, ← mul_assoc]
|
||||
congr 1
|
||||
rw [superCommuteCoef_mul_self]
|
||||
rw [koszulSignCons]
|
||||
rw [superCommuteCoef_mul_self, koszulSignCons]
|
||||
simp only [hc2 hn, ↓reduceIte]
|
||||
exact Nat.le_of_not_lt hn
|
||||
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 rs r0)
|
||||
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs r0)
|
||||
· exact Nat.le_of_lt_succ h
|
||||
· exact Nat.le_of_lt_succ h
|
||||
|
||||
|
|
|
|||
|
|
@ -16,43 +16,48 @@ import HepLean.PerturbationTheory.Wick.Signs.InsertSign
|
|||
namespace Wick
|
||||
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
/-- 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 → ℂ
|
||||
def koszulSignInsert {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
|
||||
[DecidableRel le] (a : 𝓕) : List 𝓕 → ℂ
|
||||
| [] => 1
|
||||
| b :: l => if r a b then koszulSignInsert r q a l else
|
||||
if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
|
||||
| b :: l => if le a b then koszulSignInsert q le a l else
|
||||
if q a = fermionic ∧ q b = fermionic then - koszulSignInsert q le a l else
|
||||
koszulSignInsert q le 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
|
||||
lemma koszulSignInsert_boson (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
(a : 𝓕) (ha : q a = bosonic) : (l : List 𝓕) → koszulSignInsert q le a l = 1
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| b :: l => by
|
||||
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
|
||||
rw [koszulSignInsert_boson r q a ha l, ha]
|
||||
simp only [Fin.isValue, zero_ne_one, false_and, ↓reduceIte, ite_self]
|
||||
rw [koszulSignInsert_boson q le a ha l, ha]
|
||||
simp only [reduceCtorEq, false_and, ↓reduceIte, ite_self]
|
||||
|
||||
@[simp]
|
||||
lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(a : I) : (l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
|
||||
lemma koszulSignInsert_mul_self (a : 𝓕) :
|
||||
(l : List 𝓕) → koszulSignInsert q le a l * koszulSignInsert q le a l = 1
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| b :: l => by
|
||||
simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
|
||||
by_cases hr : r a b
|
||||
by_cases hr : le a b
|
||||
· simp only [hr, ↓reduceIte]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
· simp only [hr, ↓reduceIte, Fin.isValue]
|
||||
by_cases hq : q a = 1 ∧ q b = 1
|
||||
· simp only [hq, Fin.isValue, and_self, ↓reduceIte, neg_neg]
|
||||
· simp only [hr, ↓reduceIte]
|
||||
by_cases hq : q a = fermionic ∧ q b = fermionic
|
||||
· simp only [hq, and_self, ↓reduceIte, neg_neg]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
· simp only [Fin.isValue, hq, ↓reduceIte]
|
||||
· simp only [hq, ↓reduceIte]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
|
||||
lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(a : I) (l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
|
||||
lemma koszulSignInsert_le_forall (a : 𝓕) (l : List 𝓕) (hi : ∀ b, le a b) :
|
||||
koszulSignInsert q le a l = 1 := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons j l ih =>
|
||||
|
|
@ -62,29 +67,25 @@ lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel
|
|||
intro h
|
||||
exact False.elim (h (hi j))
|
||||
|
||||
lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
|
||||
(q : I → Fin 2) (l : List I) (j i : I) (hi : ∀ j, r j i) :
|
||||
koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
|
||||
lemma koszulSignInsert_ge_forall_append (l : List 𝓕) (j i : 𝓕) (hi : ∀ j, le j i) :
|
||||
koszulSignInsert q le j l = koszulSignInsert q le 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 [ih]
|
||||
· rw [if_neg hr, if_neg hr]
|
||||
rw [ih]
|
||||
by_cases hr : le j b
|
||||
· rw [if_pos hr, if_pos hr, ih]
|
||||
· rw [if_neg hr, if_neg hr, ih]
|
||||
|
||||
lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r0 : I) : (r : List I) →
|
||||
koszulSignInsert le1 q r0 r =
|
||||
koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
|
||||
lemma koszulSignInsert_eq_filter (r0 : 𝓕) : (r : List 𝓕) →
|
||||
koszulSignInsert q le r0 r =
|
||||
koszulSignInsert q le r0 (List.filter (fun i => decide (¬ le r0 i)) r)
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| r1 :: r => by
|
||||
dsimp only [koszulSignInsert, Fin.isValue]
|
||||
simp only [Fin.isValue, List.filter, decide_not]
|
||||
by_cases h : le1 r0 r1
|
||||
by_cases h : le r0 r1
|
||||
· simp only [h, ↓reduceIte, decide_True, Bool.not_true]
|
||||
rw [koszulSignInsert_eq_filter]
|
||||
congr
|
||||
|
|
@ -97,73 +98,68 @@ lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I →
|
|||
simp only [decide_not]
|
||||
simp
|
||||
|
||||
lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
[IsTotal I le1] (r0 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
|
||||
lemma koszulSignInsert_eq_cons [IsTotal 𝓕 le] (r0 : 𝓕) (r : List 𝓕) :
|
||||
koszulSignInsert q le r0 r = koszulSignInsert q le r0 (r0 :: r) := by
|
||||
simp only [koszulSignInsert, Fin.isValue, and_self]
|
||||
have h1 : le1 r0 r0 := by
|
||||
simpa using IsTotal.total (r := le1) r0 r0
|
||||
have h1 : le r0 r0 := by
|
||||
simpa using IsTotal.total (r := le) r0 r0
|
||||
simp [h1]
|
||||
|
||||
lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
|
||||
grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
|
||||
lemma koszulSignInsert_eq_grade (r0 : 𝓕) (r : List 𝓕) :
|
||||
koszulSignInsert q le r0 r = if ofList q [r0] = fermionic ∧
|
||||
ofList q (List.filter (fun i => decide (¬ le r0 i)) r) = fermionic then -1 else 1 := by
|
||||
induction r with
|
||||
| nil =>
|
||||
simp [koszulSignInsert]
|
||||
| cons r1 r ih =>
|
||||
rw [koszulSignInsert_eq_filter]
|
||||
by_cases hr1 : ¬ le1 r0 r1
|
||||
by_cases hr1 : ¬ le r0 r1
|
||||
· rw [List.filter_cons_of_pos]
|
||||
· dsimp only [koszulSignInsert, Fin.isValue, decide_not]
|
||||
rw [if_neg hr1]
|
||||
dsimp only [Fin.isValue, grade, ite_eq_right_iff, zero_ne_one, imp_false, decide_not]
|
||||
simp only [Fin.isValue, decide_not, ite_eq_right_iff, zero_ne_one, imp_false]
|
||||
have ha (a b c : Fin 2) : (if a = 1 ∧ b = 1 then -if ¬a = 0 ∧
|
||||
c = 1 then -1 else (1 : ℂ)
|
||||
else if ¬a = 0 ∧ c = 1 then -1 else 1) =
|
||||
if ¬a = 0 ∧ ¬b = c then -1 else 1 := by
|
||||
dsimp only [Fin.isValue, ofList, ite_eq_right_iff, zero_ne_one, imp_false, decide_not]
|
||||
simp only [decide_not, ite_eq_right_iff, reduceCtorEq, imp_false]
|
||||
have ha (a b c : FieldStatistic) : (if a = fermionic ∧ b = fermionic then -if ¬a = bosonic ∧
|
||||
c = fermionic then -1 else (1 : ℂ)
|
||||
else if ¬a = bosonic ∧ c = fermionic then -1 else 1) =
|
||||
if ¬a = bosonic ∧ ¬b = c then -1 else 1 := by
|
||||
fin_cases a <;> fin_cases b <;> fin_cases c
|
||||
any_goals rfl
|
||||
simp
|
||||
rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r))]
|
||||
rw [← ha (q r0) (q r1) (ofList q (List.filter (fun a => !decide (le r0 a)) r))]
|
||||
congr
|
||||
· rw [koszulSignInsert_eq_filter] at ih
|
||||
simpa [grade] using ih
|
||||
simpa [ofList] using ih
|
||||
· rw [koszulSignInsert_eq_filter] at ih
|
||||
simpa [grade] using ih
|
||||
simpa [ofList] using ih
|
||||
· simp [hr1]
|
||||
· rw [List.filter_cons_of_neg]
|
||||
simp only [decide_not, Fin.isValue]
|
||||
rw [koszulSignInsert_eq_filter] at ih
|
||||
simpa [grade] using ih
|
||||
simpa [ofList] using ih
|
||||
simpa using hr1
|
||||
|
||||
lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
|
||||
(a : I) [DecidableRel le1] (h : r.Perm r') :
|
||||
koszulSignInsert le1 q a r = koszulSignInsert le1 q a r' := by
|
||||
lemma koszulSignInsert_eq_perm (r r' : List 𝓕) (a : 𝓕) (h : r.Perm r') :
|
||||
koszulSignInsert q le a r = koszulSignInsert q le a r' := by
|
||||
rw [koszulSignInsert_eq_grade]
|
||||
rw [koszulSignInsert_eq_grade]
|
||||
congr 1
|
||||
simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
|
||||
intro h'
|
||||
have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
|
||||
grade q (List.filter (fun i => !decide (le1 a i)) r') := by
|
||||
rw [grade_count, grade_count]
|
||||
rw [List.countP_filter, List.countP_filter]
|
||||
rw [h.countP_eq]
|
||||
have hg : ofList q (List.filter (fun i => !decide (le a i)) r) =
|
||||
ofList q (List.filter (fun i => !decide (le a i)) r') := by
|
||||
apply ofList_perm
|
||||
exact List.Perm.filter (fun i => !decide (le a i)) h
|
||||
rw [hg]
|
||||
|
||||
lemma koszulSignInsert_eq_sort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r : List I)
|
||||
(a : I) [DecidableRel le1] :
|
||||
koszulSignInsert le1 q a r = koszulSignInsert le1 q a (List.insertionSort le1 r) := by
|
||||
lemma koszulSignInsert_eq_sort (r : List 𝓕) (a : 𝓕) :
|
||||
koszulSignInsert q le a r = koszulSignInsert q le a (List.insertionSort le r) := by
|
||||
apply koszulSignInsert_eq_perm
|
||||
exact List.Perm.symm (List.perm_insertionSort le1 r)
|
||||
exact List.Perm.symm (List.perm_insertionSort le r)
|
||||
|
||||
lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 r = insertSign q (orderedInsertPos le1 (List.insertionSort le1 r) r0)
|
||||
r0 (List.insertionSort le1 r) := by
|
||||
lemma koszulSignInsert_eq_insertSign [IsTotal 𝓕 le] [IsTrans 𝓕 le] (r0 : 𝓕) (r : List 𝓕) :
|
||||
koszulSignInsert q le r0 r = insertSign q (orderedInsertPos le (List.insertionSort le r) r0)
|
||||
r0 (List.insertionSort le r) := by
|
||||
rw [koszulSignInsert_eq_cons, koszulSignInsert_eq_sort, koszulSignInsert_eq_filter,
|
||||
koszulSignInsert_eq_grade, insertSign, superCommuteCoef]
|
||||
congr
|
||||
|
|
@ -171,9 +167,9 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
|
|||
rw [List.insertionSort]
|
||||
nth_rewrite 1 [List.orderedInsert_eq_take_drop]
|
||||
rw [List.filter_append]
|
||||
have h1 : List.filter (fun a => decide ¬le1 r0 a)
|
||||
(List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
|
||||
= (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
|
||||
have h1 : List.filter (fun a => decide ¬le r0 a)
|
||||
(List.takeWhile (fun b => decide ¬le r0 b) (List.insertionSort le r))
|
||||
= (List.takeWhile (fun b => decide ¬le r0 b) (List.insertionSort le r)) := by
|
||||
induction r with
|
||||
| nil => simp
|
||||
| cons r1 r ih =>
|
||||
|
|
@ -184,15 +180,15 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
|
|||
simp_all
|
||||
rw [h1]
|
||||
rw [List.filter_cons]
|
||||
simp only [decide_not, (IsTotal.to_isRefl le1).refl r0, not_true_eq_false, decide_False,
|
||||
simp only [decide_not, (IsTotal.to_isRefl le).refl r0, not_true_eq_false, decide_False,
|
||||
Bool.false_eq_true, ↓reduceIte]
|
||||
rw [orderedInsertPos_take]
|
||||
simp only [decide_not, List.append_right_eq_self, List.filter_eq_nil_iff, Bool.not_eq_eq_eq_not,
|
||||
Bool.not_true, decide_eq_false_iff_not, Decidable.not_not]
|
||||
intro a ha
|
||||
refine List.Sorted.rel_of_mem_take_of_mem_drop
|
||||
(k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1)
|
||||
(List.sorted_insertionSort le1 (r0 :: r)) ?_ ?_
|
||||
(k := (orderedInsertPos le (List.insertionSort le r) r0).1 + 1)
|
||||
(List.sorted_insertionSort le (r0 :: r)) ?_ ?_
|
||||
· simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
|
||||
rw [List.take_append_eq_append_take]
|
||||
rw [List.take_of_length_le]
|
||||
|
|
@ -204,40 +200,36 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
|
|||
· simpa [orderedInsertPos] using ha
|
||||
· simp [orderedInsertPos]
|
||||
|
||||
lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(i j : I) (r : List I) (n : ℕ) (hn : n ≤ r.length) :
|
||||
koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
|
||||
lemma koszulSignInsert_insertIdx (i j : 𝓕) (r : List 𝓕) (n : ℕ) (hn : n ≤ r.length) :
|
||||
koszulSignInsert q le j (List.insertIdx n i r) = koszulSignInsert q le j (i :: r) := by
|
||||
apply koszulSignInsert_eq_perm
|
||||
exact List.perm_insertIdx i r hn
|
||||
|
||||
/-- The difference in `koszulSignInsert` on inserting `r0` into `r` compared to
|
||||
into `r1 :: r` for any `r`. -/
|
||||
def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
|
||||
ℂ :=
|
||||
if le1 r0 r1 then 1 else
|
||||
if q r0 = 1 ∧ q r1 = 1 then -1 else 1
|
||||
def koszulSignCons (r0 r1 : 𝓕) : ℂ :=
|
||||
if le r0 r1 then 1 else
|
||||
if q r0 = fermionic ∧ q r1 = fermionic then -1 else 1
|
||||
|
||||
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
|
||||
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
|
||||
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
|
||||
lemma koszulSignCons_eq_superComuteCoef (r0 r1 : 𝓕) : koszulSignCons q le r0 r1 =
|
||||
if le r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
|
||||
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, ofList, ite_eq_right_iff, zero_ne_one,
|
||||
imp_false]
|
||||
congr 1
|
||||
by_cases h0 : q r0 = 1
|
||||
· by_cases h1 : q r1 = 1
|
||||
by_cases h0 : q r0 = fermionic
|
||||
· by_cases h1 : q r1 = fermionic
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
· have h1 : q r1 = bosonic := (neq_fermionic_iff_eq_bosonic (q r1)).mp h1
|
||||
simp [h0, h1]
|
||||
· have h0 : q r0 = 0 := by omega
|
||||
by_cases h1 : q r1 = 1
|
||||
· have h0 : q r0 = bosonic := (neq_fermionic_iff_eq_bosonic (q r0)).mp h0
|
||||
by_cases h1 : q r1 = fermionic
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
· have h1 : q r1 = bosonic := (neq_fermionic_iff_eq_bosonic (q r1)).mp h1
|
||||
simp [h0, h1]
|
||||
|
||||
lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r0 r1 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 (r1 :: r) = (koszulSignCons q le1 r0 r1) *
|
||||
koszulSignInsert le1 q r0 r := by
|
||||
lemma koszulSignInsert_cons (r0 r1 : 𝓕) (r : List 𝓕) :
|
||||
koszulSignInsert q le r0 (r1 :: r) = (koszulSignCons q le r0 r1) *
|
||||
koszulSignInsert q le r0 r := by
|
||||
simp [koszulSignInsert, koszulSignCons]
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ import Mathlib.Analysis.Complex.Basic
|
|||
import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
|
||||
/-!
|
||||
|
||||
# Koszul sign insert
|
||||
# Static wick coefficent
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -17,28 +17,29 @@ namespace Wick
|
|||
|
||||
open HepLean.List
|
||||
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le :𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
|
||||
/-- The sign that appears in the static version of Wicks theorem.
|
||||
This is actually equal to `superCommuteCoef q [r.get n] (r.take n)`, something
|
||||
which will be proved in a lemma. -/
|
||||
def staticWickCoef {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
|
||||
koszulSign le1 q r *
|
||||
superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
|
||||
(List.insertionSort le1 r)) *
|
||||
koszulSign le1 q (r.eraseIdx ↑n)
|
||||
def staticWickCoef (r : List 𝓕) (i : 𝓕) (n : Fin r.length) : ℂ :=
|
||||
koszulSign q le r *
|
||||
superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le r) n))
|
||||
(List.insertionSort le r)) *
|
||||
koszulSign q le (r.eraseIdx ↑n)
|
||||
|
||||
lemma staticWickCoef_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] (i : I) (n : Fin r.length)
|
||||
lemma staticWickCoef_eq_q (r : List 𝓕) (i : 𝓕) (n : Fin r.length)
|
||||
(hq : q i = q (r.get n)) :
|
||||
staticWickCoef q le1 r i n =
|
||||
koszulSign le1 q r *
|
||||
superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le1 r n))
|
||||
(List.insertionSort le1 r)) *
|
||||
koszulSign le1 q (r.eraseIdx ↑n) := by
|
||||
simp [staticWickCoef, superCommuteCoef, grade, hq]
|
||||
staticWickCoef q le r i n =
|
||||
koszulSign q le r *
|
||||
superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le r n))
|
||||
(List.insertionSort le r)) *
|
||||
koszulSign q le (r.eraseIdx ↑n) := by
|
||||
simp [staticWickCoef, superCommuteCoef, ofList, hq]
|
||||
|
||||
lemma insertIdx_eraseIdx {I : Type} :
|
||||
(n : ℕ) → (r : List I) → (hn : n < r.length) →
|
||||
lemma insertIdx_eraseIdx {I : Type} : (n : ℕ) → (r : List I) → (hn : n < r.length) →
|
||||
List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
|
||||
| n, [], hn => by
|
||||
simp at hn
|
||||
|
|
@ -49,10 +50,9 @@ lemma insertIdx_eraseIdx {I : Type} :
|
|||
List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
|
||||
exact insertIdx_eraseIdx n r _
|
||||
|
||||
lemma staticWickCoef_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
|
||||
lemma staticWickCoef_eq_get [IsTotal 𝓕 le] [IsTrans 𝓕 le] (r : List 𝓕) (i : 𝓕) (n : Fin r.length)
|
||||
(heq : q i = q (r.get n)) :
|
||||
staticWickCoef q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
|
||||
staticWickCoef q le r i n = superCommuteCoef q [r.get n] (r.take n) := by
|
||||
rw [staticWickCoef_eq_q]
|
||||
let r' := r.eraseIdx ↑n
|
||||
have hr : List.insertIdx n (r.get n) (r.eraseIdx n) = r := by
|
||||
|
|
@ -61,7 +61,7 @@ lemma staticWickCoef_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
|
|||
lhs
|
||||
lhs
|
||||
rw [← hr]
|
||||
rw [koszulSign_insertIdx q le1 (r.get n) ((r.eraseIdx ↑n)) n (by
|
||||
rw [koszulSign_insertIdx q le (r.get n) ((r.eraseIdx ↑n)) n (by
|
||||
rw [List.length_eraseIdx]
|
||||
simp only [Fin.is_lt, ↓reduceIte]
|
||||
omega)]
|
||||
|
|
|
|||
|
|
@ -3,25 +3,29 @@ 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.Mathematics.List
|
||||
import HepLean.PerturbationTheory.Wick.Signs.Grade
|
||||
import HepLean.PerturbationTheory.FieldStatistics
|
||||
/-!
|
||||
|
||||
# Koszul signs and ordering for lists and algebras
|
||||
# Super commutation coefficent.
|
||||
|
||||
This is a complex number which is `-1` when commuting two fermionic operators and `1` otherwise.
|
||||
|
||||
-/
|
||||
|
||||
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]
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ 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.Contraction
|
||||
import HepLean.PerturbationTheory.Wick.Contractions
|
||||
/-!
|
||||
|
||||
# Static Wick's theorem
|
||||
|
|
@ -15,35 +15,33 @@ namespace Wick
|
|||
noncomputable section
|
||||
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] (q : 𝓕 → FieldStatistic)
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
|
||||
lemma static_wick_nil {A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
|
||||
(S : Contractions.Splitting f le1) :
|
||||
(S : Contractions.Splitting f le) :
|
||||
F (ofListLift f [] 1) = ∑ c : Contractions [],
|
||||
c.toCenterTerm f q le1 F S *
|
||||
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
|
||||
c.toCenterTerm f q le F S *
|
||||
F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
|
||||
rw [← Contractions.nilEquiv.symm.sum_comp]
|
||||
simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
|
||||
Finset.sum_const, Finset.card_singleton, one_smul]
|
||||
dsimp [Contractions.normalize, Contractions.toCenterTerm]
|
||||
simp [ofListLift_empty]
|
||||
|
||||
lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
[IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List I) (a : I)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
|
||||
(S : Contractions.Splitting f le1)
|
||||
lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕) (a : 𝓕)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
|
||||
(S : Contractions.Splitting f le)
|
||||
(ih : F (ofListLift f r 1) =
|
||||
∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst)
|
||||
∑ c : Contractions r, c.toCenterTerm f q le F S * F (koszulOrder (fun i => q i.fst) le
|
||||
(ofListLift f c.normalize 1))) :
|
||||
F (ofListLift f (a :: r) 1) = ∑ c : Contractions (a :: r),
|
||||
c.toCenterTerm f q le1 F S *
|
||||
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
|
||||
c.toCenterTerm f q le F S *
|
||||
F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
|
||||
rw [ofListLift_cons_eq_ofListLift, map_mul, ih, Finset.mul_sum,
|
||||
← Contractions.consEquiv.symm.sum_comp]
|
||||
erw [Finset.sum_sigma]
|
||||
|
|
@ -51,33 +49,26 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
funext c
|
||||
have hb := S.h𝓑 a
|
||||
rw [← mul_assoc]
|
||||
have hi := c.toCenterTerm_center f q le1 F S
|
||||
have hi := c.toCenterTerm_center f q le F S
|
||||
rw [Subalgebra.mem_center_iff] at hi
|
||||
rw [hi, mul_assoc, ← map_mul, hb, add_mul, map_add]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
lhs
|
||||
rw [ofList_eq_smul_one]
|
||||
rw [Algebra.smul_mul_assoc]
|
||||
rw [ofList_singleton]
|
||||
enter [2, 1]
|
||||
rw [ofList_eq_smul_one, Algebra.smul_mul_assoc, ofList_singleton]
|
||||
rw [mul_koszulOrder_le]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
lhs
|
||||
enter [2, 1]
|
||||
rw [← map_smul, ← Algebra.smul_mul_assoc]
|
||||
rw [← ofList_singleton, ← ofList_eq_smul_one]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
rhs
|
||||
enter [2, 2]
|
||||
rw [ofList_eq_smul_one, Algebra.smul_mul_assoc, map_smul]
|
||||
rw [le_all_mul_koszulOrder_ofListLift_expand]
|
||||
conv_lhs =>
|
||||
rhs
|
||||
rhs
|
||||
enter [2, 2]
|
||||
rw [smul_add, Finset.smul_sum]
|
||||
rw [← map_smul, ← map_smul, ← Algebra.smul_mul_assoc, ← ofList_eq_smul_one]
|
||||
rhs
|
||||
rhs
|
||||
enter [2, 2]
|
||||
intro n
|
||||
rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂,
|
||||
← ofList_eq_smul_one]
|
||||
|
|
@ -92,18 +83,15 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
exact S.h𝓑p a
|
||||
exact S.h𝓑n a
|
||||
|
||||
theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
|
||||
[IsTotal ((i : I) × f i) le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List I)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
|
||||
(S : Contractions.Splitting f le1) :
|
||||
F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le1 F S *
|
||||
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
|
||||
theorem static_wick_theorem [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
|
||||
(S : Contractions.Splitting f le) :
|
||||
F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le F S *
|
||||
F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
|
||||
induction r with
|
||||
| nil => exact static_wick_nil q le1 F S
|
||||
| cons a r ih => exact static_wick_cons q le1 r a F S ih
|
||||
| nil => exact static_wick_nil q le F S
|
||||
| cons a r ih => exact static_wick_cons q le r a F S ih
|
||||
|
||||
end
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -13,17 +13,20 @@ import HepLean.PerturbationTheory.Wick.OfList
|
|||
namespace Wick
|
||||
|
||||
noncomputable section
|
||||
open FieldStatistic
|
||||
|
||||
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic)
|
||||
|
||||
/-- Given a grading `q : I → Fin 2` and a list `l : List I` the super-commutor on the free algebra
|
||||
`FreeAlgebra ℂ I` corresponding to commuting with `l`
|
||||
as a linear map from `MonoidAlgebra ℂ (FreeMonoid I)` (the module of lists in `I`)
|
||||
to itself. -/
|
||||
def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
|
||||
MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
|
||||
Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid I)) ℂ (List I)
|
||||
def superCommuteMonoidAlgebra (l : List 𝓕) :
|
||||
MonoidAlgebra ℂ (FreeMonoid 𝓕) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid 𝓕) :=
|
||||
Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid 𝓕)) ℂ (List 𝓕)
|
||||
(fun r =>
|
||||
Finsupp.lsingle (R := ℂ) (l ++ r) 1 +
|
||||
if grade q l = 1 ∧ grade q r = 1 then
|
||||
if FieldStatistic.ofList q l = fermionic ∧ FieldStatistic.ofList q r = fermionic then
|
||||
Finsupp.lsingle (R := ℂ) (r ++ l) 1
|
||||
else
|
||||
- Finsupp.lsingle (R := ℂ) (r ++ l) 1)
|
||||
|
|
@ -31,17 +34,17 @@ def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
|
|||
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra ℂ I`
|
||||
as a linear map from `MonoidAlgebra ℂ (FreeMonoid I)` (the module of lists in `I`)
|
||||
to `FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I`. -/
|
||||
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 =>
|
||||
def superCommuteAlgebra :
|
||||
MonoidAlgebra ℂ (FreeMonoid 𝓕) →ₗ[ℂ] FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 :=
|
||||
Finsupp.lift (FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕) ℂ (List 𝓕) fun l =>
|
||||
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
|
||||
∘ₗ superCommuteMonoidAlgebra q l
|
||||
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap)
|
||||
|
||||
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra ℂ I`
|
||||
as a bi-linear map. -/
|
||||
def superCommute {I : Type} (q : I → Fin 2) :
|
||||
FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
|
||||
def superCommute :
|
||||
FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 :=
|
||||
superCommuteAlgebra q
|
||||
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
|
||||
|
||||
|
|
@ -51,10 +54,10 @@ lemma equivMonoidAlgebraFreeMonoid_freeAlgebra {I : Type} (i : I) :
|
|||
simp [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.single]
|
||||
|
||||
@[simp]
|
||||
lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
|
||||
lemma superCommute_ι (i j : 𝓕) :
|
||||
superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j) =
|
||||
FreeAlgebra.ι ℂ i * FreeAlgebra.ι ℂ j +
|
||||
if q i = 1 ∧ q j = 1 then
|
||||
if q i = fermionic ∧ q j = fermionic then
|
||||
FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i
|
||||
else
|
||||
- FreeAlgebra.ι ℂ j * FreeAlgebra.ι ℂ i := by
|
||||
|
|
@ -62,7 +65,7 @@ lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
|
|||
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,
|
||||
simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, ofList_freeMonoid,
|
||||
zero_smul, Finsupp.sum_single_index, one_smul, LinearMap.coe_comp, Function.comp_apply,
|
||||
AlgEquiv.toLinearMap_apply, equivMonoidAlgebraFreeMonoid_freeAlgebra]
|
||||
conv_lhs =>
|
||||
|
|
@ -70,10 +73,10 @@ lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
|
|||
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,
|
||||
Finsupp.single_zero, Finsupp.sum_single_index, ofList_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
|
||||
by_cases hq : q i = fermionic ∧ q j = fermionic
|
||||
· rw [if_pos hq, if_pos hq]
|
||||
simp only [MonoidAlgebra.lift_single, one_smul]
|
||||
obtain ⟨left, right⟩ := hq
|
||||
|
|
@ -82,9 +85,10 @@ lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
|
|||
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 : ℂ) :
|
||||
lemma superCommute_ofList_ofList (l r : List 𝓕) (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 (l ++ r) (x * y) + (if FieldStatistic.ofList q l = fermionic ∧
|
||||
FieldStatistic.ofList q r = fermionic 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,
|
||||
|
|
@ -99,8 +103,8 @@ lemma superCommute_ofList_ofList {I : Type} (q : I → Fin 2) (l r : List I) (x
|
|||
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]
|
||||
by_cases hg : FieldStatistic.ofList q l = fermionic ∧ FieldStatistic.ofList q r = fermionic
|
||||
· simp only [hg, and_self, ↓reduceIte]
|
||||
congr
|
||||
· rw [← map_smul]
|
||||
congr
|
||||
|
|
@ -120,19 +124,19 @@ lemma superCommute_ofList_ofList {I : Type} (q : I → Fin 2) (l r : List I) (x
|
|||
exact MonoidAlgebra.smul_single' x (r ++ l) y
|
||||
|
||||
@[simp]
|
||||
lemma superCommute_zero {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
|
||||
lemma superCommute_zero (a : FreeAlgebra ℂ 𝓕) :
|
||||
superCommute q a 0 = 0 := by
|
||||
simp [superCommute]
|
||||
|
||||
@[simp]
|
||||
lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
|
||||
lemma superCommute_one (a : FreeAlgebra ℂ 𝓕) :
|
||||
superCommute q a 1 = 0 := by
|
||||
let f : FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I := (LinearMap.flip (superCommute q)) 1
|
||||
let f : FreeAlgebra ℂ 𝓕 →ₗ[ℂ] FreeAlgebra ℂ 𝓕 := (LinearMap.flip (superCommute q)) 1
|
||||
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1) =
|
||||
(1 : FreeAlgebra ℂ I) := by
|
||||
(1 : FreeAlgebra ℂ 𝓕) := by
|
||||
simp_all only [EmbeddingLike.map_eq_one_iff]
|
||||
rfl
|
||||
have f_single (l : FreeMonoid I) (x : ℂ) :
|
||||
have f_single (l : FreeMonoid 𝓕) (x : ℂ) :
|
||||
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
|
||||
= 0 := by
|
||||
simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
|
||||
|
|
@ -149,7 +153,7 @@ lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
|
|||
erw [Finsupp.lift_apply]
|
||||
simp
|
||||
have hf : f = 0 := by
|
||||
let e : FreeAlgebra ℂ I ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
|
||||
let e : FreeAlgebra ℂ 𝓕 ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid 𝓕) :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
|
||||
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
|
||||
apply MonoidAlgebra.lhom_ext'
|
||||
|
|
@ -163,39 +167,39 @@ lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra ℂ I) :
|
|||
rw [hf]
|
||||
simp
|
||||
|
||||
lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (xa xb xc : ℂ) :
|
||||
lemma superCommute_ofList_mul (la lb lc : List 𝓕) (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,
|
||||
simp only [superCommute_ofList_ofList, Fin.isValue, ofList_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,
|
||||
simp only [superCommute_ofList_ofList, Fin.isValue, ofList_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
|
||||
by_cases hla : FieldStatistic.ofList q la = fermionic
|
||||
· simp only [hla, Fin.isValue, true_and, ite_not, ite_smul, neg_smul, one_smul]
|
||||
by_cases hlb : grade q lb = 1
|
||||
by_cases hlb : FieldStatistic.ofList q lb = fermionic
|
||||
· simp only [hlb, Fin.isValue, ↓reduceIte]
|
||||
by_cases hlc : grade q lc = 1
|
||||
· simp only [Fin.isValue, hlc, ↓reduceIte]
|
||||
by_cases hlc : FieldStatistic.ofList q lc = fermionic
|
||||
· simp only [hlc, reduceCtorEq, imp_false, not_true_eq_false, ↓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]
|
||||
· have hc : FieldStatistic.ofList q lc = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q lc)).mp hlc
|
||||
simp only [hc, fermionic_not_eq_bonsic, reduceCtorEq, imp_self, ↓reduceIte]
|
||||
simp only [mul_assoc, add_mul, mul_add, mul_neg, neg_add_rev, neg_neg]
|
||||
abel
|
||||
· have hb : grade q lb = 0 := by
|
||||
omega
|
||||
· have hb : FieldStatistic.ofList q lb = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q lb)).mp hlb
|
||||
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]
|
||||
by_cases hlc : FieldStatistic.ofList q lc = fermionic
|
||||
· simp only [hlc, reduceCtorEq, imp_self, ↓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]
|
||||
· have hc : FieldStatistic.ofList q lc = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q lc)).mp hlc
|
||||
simp only [hc, reduceCtorEq, imp_false, not_true_eq_false, ↓reduceIte]
|
||||
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,
|
||||
|
|
@ -207,14 +211,14 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
|
|||
E.g. in the commutator
|
||||
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
|
||||
and for `n=1` is `b [a, c]`. -/
|
||||
def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
|
||||
(hn : n < lb.length) : FreeAlgebra ℂ I :=
|
||||
def superCommuteSplit (la lb : List 𝓕) (xa xb : ℂ) (n : ℕ)
|
||||
(hn : n < lb.length) : FreeAlgebra ℂ 𝓕 :=
|
||||
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) :
|
||||
lemma superCommute_ofList_cons (la lb : List 𝓕) (xa xb : ℂ) (b1 : 𝓕) :
|
||||
superCommute q (ofList la xa) (ofList (b1 :: lb) xb) =
|
||||
superCommute q (ofList la xa) (FreeAlgebra.ι ℂ b1) * ofList lb xb +
|
||||
superCommuteCoef q la [b1] •
|
||||
|
|
@ -224,13 +228,13 @@ lemma superCommute_ofList_cons {I : Type} (q : I → Fin 2) (la lb : List I) (xa
|
|||
congr
|
||||
· exact ofList_singleton b1
|
||||
|
||||
lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
|
||||
lemma superCommute_ofList_sum (la lb : List 𝓕) (xa xb : ℂ) :
|
||||
superCommute q (ofList la xa) (ofList lb xb) =
|
||||
∑ (n : Fin lb.length), superCommuteSplit 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,
|
||||
simp only [superCommute_ofList_ofList, List.append_nil, FieldStatistic.ofList_empty,
|
||||
reduceCtorEq, and_false, ↓reduceIte, List.nil_append, List.length_nil, Finset.univ_eq_empty,
|
||||
Finset.sum_empty]
|
||||
ring_nf
|
||||
abel
|
||||
|
|
@ -240,7 +244,7 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
|
|||
superCommuteSplit q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
|
||||
simp [superCommuteSplit, superCommuteCoef_empty, ofList_empty]
|
||||
rw [h0]
|
||||
have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ I) : ∑ n, f n = f ⟨0,
|
||||
have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ 𝓕) : ∑ 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]
|
||||
|
|
@ -257,36 +261,39 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
|
|||
· 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 superCommute_ofList_ofList_superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I)
|
||||
lemma superCommute_ofList_ofList_superCommuteCoef (la lb : List 𝓕)
|
||||
(xa xb : ℂ) : superCommute q (ofList la xa) (ofList lb xb) =
|
||||
ofList la xa * ofList lb xb - superCommuteCoef q la lb • ofList lb xb * ofList la xa := by
|
||||
rw [superCommute_ofList_ofList, superCommuteCoef]
|
||||
by_cases hq : grade q la = 1 ∧ grade q lb = 1
|
||||
by_cases hq : FieldStatistic.ofList q la = fermionic ∧ FieldStatistic.ofList q lb = fermionic
|
||||
· simp [hq, ofList_pair]
|
||||
· simp only [ofList_pair, Fin.isValue, hq, ↓reduceIte, one_smul]
|
||||
abel
|
||||
|
||||
lemma ofList_ofList_superCommute {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
|
||||
lemma ofList_ofList_superCommute (la lb : List 𝓕) (xa xb : ℂ) :
|
||||
ofList la xa * ofList lb xb = superCommuteCoef q la lb • ofList lb xb * ofList la xa
|
||||
+ superCommute q (ofList la xa) (ofList lb xb) := by
|
||||
rw [superCommute_ofList_ofList_superCommuteCoef]
|
||||
abel
|
||||
|
||||
lemma ofListLift_ofList_superCommute' {I : Type}
|
||||
(q : I → Fin 2) (l : List I) (r : List I) (x y : ℂ) :
|
||||
ofList r y * ofList l x = superCommuteCoef q l r • (ofList l x * ofList r y)
|
||||
lemma ofListLift_ofList_superCommute' (l : List 𝓕) (r : List 𝓕) (x y : ℂ) :
|
||||
ofList r y * ofList l x = superCommuteCoef q l r • (ofList l x * ofList r y)
|
||||
- superCommuteCoef q l r • superCommute q (ofList l x) (ofList r y) := by
|
||||
nth_rewrite 2 [ofList_ofList_superCommute q]
|
||||
rw [superCommuteCoef]
|
||||
by_cases hq : grade q l = 1 ∧ grade q r = 1
|
||||
by_cases hq : FieldStatistic.ofList q l = fermionic ∧ FieldStatistic.ofList q r = fermionic
|
||||
· simp [hq, superCommuteCoef]
|
||||
· simp [hq]
|
||||
|
||||
lemma superCommute_ofList_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
section lift
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] (q : 𝓕 → FieldStatistic)
|
||||
|
||||
lemma superCommute_ofList_ofListLift (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) :
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
|
||||
ofList l x * ofListLift f r y +
|
||||
(if grade (fun i => q i.1) l = 1 ∧ grade q r = 1 then
|
||||
(if FieldStatistic.ofList (fun i => q i.1) l = fermionic ∧
|
||||
FieldStatistic.ofList q r = fermionic then
|
||||
ofListLift f r y * ofList l x else - ofListLift f r y * ofList l x) := by
|
||||
conv_lhs => rw [ofListLift_expand]
|
||||
rw [map_sum]
|
||||
|
|
@ -314,56 +321,55 @@ lemma superCommute_ofList_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype
|
|||
· rw [ofList_pair]
|
||||
simp only [neg_mul]
|
||||
|
||||
lemma superCommute_ofList_ofListLift_superCommuteLiftCoef {I : Type} {f : I → Type}
|
||||
[∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
lemma superCommute_ofList_ofListLift_superCommuteLiftCoef
|
||||
(l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) :
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
|
||||
ofList l x * ofListLift f r y - superCommuteLiftCoef q l r • ofListLift f r y * ofList l x := by
|
||||
rw [superCommute_ofList_ofListLift, superCommuteLiftCoef]
|
||||
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
|
||||
by_cases hq : FieldStatistic.ofList (fun i => q i.fst) l = fermionic ∧
|
||||
FieldStatistic.ofList q r = fermionic
|
||||
· simp [hq]
|
||||
· simp only [Fin.isValue, hq, ↓reduceIte, neg_mul, one_smul]
|
||||
abel
|
||||
|
||||
lemma ofList_ofListLift_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
lemma ofList_ofListLift_superCommute (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) :
|
||||
ofList l x * ofListLift f r y = superCommuteLiftCoef q l r • ofListLift f r y * ofList l x
|
||||
+ superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
|
||||
rw [superCommute_ofList_ofListLift_superCommuteLiftCoef]
|
||||
abel
|
||||
|
||||
lemma ofListLift_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 : ℂ) :
|
||||
ofListLift f r y * ofList l x = superCommuteLiftCoef q l r • (ofList l x * ofListLift f r y)
|
||||
lemma ofListLift_ofList_superCommute (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) :
|
||||
ofListLift f r y * ofList l x = superCommuteLiftCoef q l r • (ofList l x * ofListLift f r y)
|
||||
- superCommuteLiftCoef q l r •
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
|
||||
rw [ofList_ofListLift_superCommute, superCommuteLiftCoef]
|
||||
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
|
||||
by_cases hq : FieldStatistic.ofList (fun i => q i.fst) l = fermionic ∧
|
||||
FieldStatistic.ofList q r = fermionic
|
||||
· simp [hq]
|
||||
· simp [hq]
|
||||
|
||||
lemma superCommuteLiftCoef_append {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
|
||||
omit [(i : 𝓕) → Fintype (f i)] in
|
||||
lemma superCommuteLiftCoef_append (l : List (Σ i, f i)) (r1 r2 : List 𝓕) :
|
||||
superCommuteLiftCoef q l (r1 ++ r2) =
|
||||
superCommuteLiftCoef q l r1 * superCommuteLiftCoef q l r2 := by
|
||||
simp only [superCommuteLiftCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
|
||||
simp only [superCommuteLiftCoef, Fin.isValue, ofList_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
|
||||
by_cases hla : FieldStatistic.ofList (fun i => q i.1) l = fermionic
|
||||
· by_cases hlb : FieldStatistic.ofList q r1 = fermionic
|
||||
· by_cases hlc : FieldStatistic.ofList q r2 = fermionic
|
||||
· simp [hlc, hlb, hla]
|
||||
· have hc : grade q r2 = 0 := by
|
||||
omega
|
||||
· have hc : FieldStatistic.ofList q r2 = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q r2)).mp hlc
|
||||
simp [hc, hlb, hla]
|
||||
· have hb : grade q r1 = 0 := by
|
||||
omega
|
||||
by_cases hlc : grade q r2 = 1
|
||||
· have hb : FieldStatistic.ofList q r1 = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q r1)).mp hlb
|
||||
by_cases hlc : FieldStatistic.ofList q r2 = fermionic
|
||||
· simp [hlc, hb]
|
||||
· have hc : grade q r2 = 0 := by
|
||||
omega
|
||||
· have hc : FieldStatistic.ofList q r2 = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList q r2)).mp hlc
|
||||
simp [hc, hb]
|
||||
· have ha : grade (fun i => q i.1) l = 0 := by
|
||||
omega
|
||||
· have ha : FieldStatistic.ofList (fun i => q i.1) l = bosonic := by
|
||||
exact (neq_fermionic_iff_eq_bosonic (FieldStatistic.ofList (fun i => q i.fst) l)).mp hla
|
||||
simp [ha]
|
||||
|
||||
/-- Given two lists `l : List (Σ i, f i)` and `r : List I`, on
|
||||
|
|
@ -372,16 +378,14 @@ lemma superCommuteLiftCoef_append {I : Type} {f : I → Type}
|
|||
E.g. in the commutator
|
||||
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
|
||||
and for `n=1` is `b [a, c]`. -/
|
||||
def superCommuteLiftSplit {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
|
||||
def superCommuteLiftSplit (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) (n : ℕ)
|
||||
(hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
|
||||
superCommuteLiftCoef q l (List.take n r) •
|
||||
(ofListLift f (List.take n r) 1 *
|
||||
superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))
|
||||
* ofListLift f (List.drop (n + 1) r) y)
|
||||
|
||||
lemma superCommute_ofList_ofListLift_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) :
|
||||
lemma superCommute_ofList_ofListLift_cons (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) (b1 : 𝓕) :
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f (b1 :: r) y) =
|
||||
superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι ℂ b1))
|
||||
* ofListLift f r y + superCommuteLiftCoef q l [b1] •
|
||||
|
|
@ -392,7 +396,7 @@ lemma superCommute_ofList_ofListLift_cons {I : Type} {f : I → Type} [∀ i, Fi
|
|||
rw [ofListLift_expand]
|
||||
rw [Finset.mul_sum]
|
||||
rw [map_sum]
|
||||
trans ∑ (n : CreateAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
|
||||
trans ∑ (n : CreateAnnihilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
|
||||
((FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
|
||||
· apply congrArg
|
||||
funext n
|
||||
|
|
@ -430,13 +434,12 @@ lemma superCommute_ofList_ofListLift_cons {I : Type} {f : I → Type} [∀ i, Fi
|
|||
rw [ofList_singleton]
|
||||
simp
|
||||
|
||||
lemma superCommute_ofList_ofListLift_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
lemma superCommute_ofList_ofListLift_sum (l : List (Σ i, f i)) (r : List 𝓕) (x y : ℂ) :
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
|
||||
∑ (n : Fin r.length), superCommuteLiftSplit q l r x y n n.prop := by
|
||||
induction r with
|
||||
| nil =>
|
||||
simp only [superCommute_ofList_ofListLift, Fin.isValue, grade_empty, zero_ne_one, and_false,
|
||||
simp only [superCommute_ofList_ofListLift, Fin.isValue, ofList_empty, zero_ne_one, and_false,
|
||||
↓reduceIte, neg_mul, List.length_nil, Finset.univ_eq_empty, Finset.sum_empty]
|
||||
rw [ofListLift, ofList_empty']
|
||||
simp
|
||||
|
|
@ -447,7 +450,7 @@ lemma superCommute_ofList_ofListLift_sum {I : Type} {f : I → Type} [∀ i, Fin
|
|||
superCommuteLiftSplit q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
|
||||
simp [superCommuteLiftSplit, superCommuteLiftCoef_empty, ofListLift_empty]
|
||||
rw [h0]
|
||||
have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n = g ⟨0,
|
||||
have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((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]
|
||||
|
|
@ -470,5 +473,6 @@ lemma superCommute_ofList_ofListLift_sum {I : Type} {f : I → Type} [∀ i, Fin
|
|||
congr
|
||||
rw [← ofList_pair, one_mul]
|
||||
rfl
|
||||
end lift
|
||||
end
|
||||
end Wick
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue