diff --git a/HepLean.lean b/HepLean.lean index 59847a6c..47bb4292 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -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 diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean index e3c81c5c..7f779077 100644 --- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean +++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean @@ -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) | μ ν ⊗ diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean index 12d5346b..9677db2e 100644 --- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean +++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean @@ -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 diff --git a/HepLean/PerturbationTheory/FieldStatistics.lean b/HepLean/PerturbationTheory/FieldStatistics.lean new file mode 100644 index 00000000..32b3d355 --- /dev/null +++ b/HepLean/PerturbationTheory/FieldStatistics.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/Contraction.lean b/HepLean/PerturbationTheory/Wick/Contractions.lean similarity index 74% rename from HepLean/PerturbationTheory/Wick/Contraction.lean rename to HepLean/PerturbationTheory/Wick/Contractions.lean index b8f8bb78..ca64d943 100644 --- a/HepLean/PerturbationTheory/Wick/Contraction.lean +++ b/HepLean/PerturbationTheory/Wick/Contractions.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean similarity index 71% rename from HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean rename to HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean index 7656bd7b..59936b51 100644 --- a/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean +++ b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/KoszulOrder.lean b/HepLean/PerturbationTheory/Wick/KoszulOrder.lean index 977822fc..85a5a068 100644 --- a/HepLean/PerturbationTheory/Wick/KoszulOrder.lean +++ b/HepLean/PerturbationTheory/Wick/KoszulOrder.lean @@ -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)) - -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 +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 : 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] diff --git a/HepLean/PerturbationTheory/Wick/OfList.lean b/HepLean/PerturbationTheory/Wick/OfList.lean index 000ed04c..674ae10b 100644 --- a/HepLean/PerturbationTheory/Wick/OfList.lean +++ b/HepLean/PerturbationTheory/Wick/OfList.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/OperatorMap.lean b/HepLean/PerturbationTheory/Wick/OperatorMap.lean index 1c7cf8e6..535e3660 100644 --- a/HepLean/PerturbationTheory/Wick/OperatorMap.lean +++ b/HepLean/PerturbationTheory/Wick/OperatorMap.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/Signs/Grade.lean b/HepLean/PerturbationTheory/Wick/Signs/Grade.lean deleted file mode 100644 index e1d2bb29..00000000 --- a/HepLean/PerturbationTheory/Wick/Signs/Grade.lean +++ /dev/null @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean b/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean index bf75fb59..68c70110 100644 --- a/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean +++ b/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean index 91d96544..42e2bd4f 100644 --- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean +++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean b/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean index d6ac74b2..cbac7926 100644 --- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean +++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean @@ -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] - -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) + 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 (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 - -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, +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 (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 diff --git a/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean b/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean index d6a4731b..580c5ae5 100644 --- a/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean +++ b/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean @@ -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)] diff --git a/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean b/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean index 16bece3a..b967234a 100644 --- a/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean +++ b/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean @@ -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] diff --git a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean index f129a790..a47f7d72 100644 --- a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean +++ b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean @@ -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 diff --git a/HepLean/PerturbationTheory/Wick/SuperCommute.lean b/HepLean/PerturbationTheory/Wick/SuperCommute.lean index e4b10ca8..1cae785f 100644 --- a/HepLean/PerturbationTheory/Wick/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Wick/SuperCommute.lean @@ -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