From 91071156204fcb1aa2a3c872ca5a318881f184fa Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 29 Jan 2025 15:08:43 +0000 Subject: [PATCH] feat: Add SuperCommute for FieldOpAlgebra --- .../Algebras/CrAnAlgebra/Grading.lean | 102 +++++++- .../Algebras/CrAnAlgebra/SuperCommute.lean | 47 ++++ .../Algebras/FieldOpAlgebra/Basic.lean | 236 ++++++++++++++++++ .../Algebras/FieldOpAlgebra/SuperCommute.lean | 114 +++++++++ .../Algebras/FieldOpAlgebra/TimeOrder.lean | 218 +++++++++++++++- 5 files changed, 708 insertions(+), 9 deletions(-) create mode 100644 HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean index f5a34ef..00c4f43 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Grading.lean @@ -37,6 +37,11 @@ lemma ofCrAnList_bosonic_or_fermionic (φs : List 𝓕.CrAnStates) : · right exact ofCrAnList_mem_statisticSubmodule_of φs fermionic (by simpa using h) +lemma ofCrAnState_bosonic_or_fermionic (φ : 𝓕.CrAnStates) : + ofCrAnState φ ∈ statisticSubmodule bosonic ∨ ofCrAnState φ ∈ statisticSubmodule fermionic := by + rw [← ofCrAnList_singleton] + exact ofCrAnList_bosonic_or_fermionic [φ] + /-- The projection of an element of `CrAnAlgebra` onto it's bosonic part. -/ def bosonicProj : 𝓕.CrAnAlgebra →ₗ[ℂ] statisticSubmodule (𝓕 := 𝓕) bosonic := Basis.constr ofCrAnListBasis ℂ fun φs => @@ -183,6 +188,7 @@ lemma bosonicProj_add_fermionicProj (a : 𝓕.CrAnAlgebra) : · simp [h] · simp [h] + lemma coeAddMonoidHom_apply_eq_bosonic_plus_fermionic (a : DirectSum FieldStatistic (fun i => (statisticSubmodule (𝓕 := 𝓕) i))) : DirectSum.coeAddMonoidHom statisticSubmodule a = a.1 bosonic + a.1 fermionic := by @@ -229,7 +235,7 @@ lemma directSum_eq_bosonic_plus_fermionic conv_lhs => rw [hx, hy] abel -instance : GradedAlgebra (A := 𝓕.CrAnAlgebra) statisticSubmodule where +instance crAnAlgebraGrade : GradedAlgebra (A := 𝓕.CrAnAlgebra) statisticSubmodule where one_mem := by simp only [statisticSubmodule] refine Submodule.mem_span.mpr fun p a => a ?_ @@ -296,6 +302,100 @@ lemma eq_zero_of_bosonic_and_fermionic {a : 𝓕.CrAnAlgebra} rw [ha, hb] at hc simpa using hc +lemma bosonicProj_mul (a b : 𝓕.CrAnAlgebra) : + (a * b).bosonicProj.1 = a.bosonicProj.1 * b.bosonicProj.1 + + a.fermionicProj.1 * b.fermionicProj.1 := by + conv_lhs => + rw [← bosonicProj_add_fermionicProj a] + rw [← bosonicProj_add_fermionicProj b] + simp [mul_add, add_mul] + rw [bosonicProj_of_mem_bosonic] + conv_lhs => + left + right + rw [bosonicProj_of_mem_fermionic _ + (by + have h1 : fermionic = fermionic + bosonic := by simp + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + conv_lhs => + right + left + rw [bosonicProj_of_mem_fermionic _ + (by + have h1 : fermionic = bosonic + fermionic := by simp + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + conv_lhs => + right + right + rw [bosonicProj_of_mem_bosonic _ + (by + have h1 : bosonic = fermionic + fermionic := by simp; rfl + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + simp + · have h1 : bosonic = bosonic + bosonic := by simp; rfl + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp + +lemma fermionicProj_mul (a b : 𝓕.CrAnAlgebra) : + (a * b).fermionicProj.1 = a.bosonicProj.1 * b.fermionicProj.1 + + a.fermionicProj.1 * b.bosonicProj.1 := by + conv_lhs => + rw [← bosonicProj_add_fermionicProj a] + rw [← bosonicProj_add_fermionicProj b] + simp [mul_add, add_mul] + conv_lhs => + left + left + rw [fermionicProj_of_mem_bosonic _ + (by + have h1 : bosonic = bosonic + bosonic := by simp; rfl + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + conv_lhs => + left + right + rw [fermionicProj_of_mem_fermionic _ + (by + have h1 : fermionic = fermionic + bosonic := by simp + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + conv_lhs => + right + left + rw [fermionicProj_of_mem_fermionic _ + (by + have h1 : fermionic = bosonic + fermionic := by simp + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + conv_lhs => + right + right + rw [fermionicProj_of_mem_bosonic _ + (by + have h1 : bosonic = fermionic + fermionic := by simp; rfl + conv_lhs => rw [h1] + apply crAnAlgebraGrade.mul_mem + simp + simp)] + simp + abel end diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean index ce9e4a6..f5ceffc 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean @@ -688,6 +688,18 @@ lemma superCommute_fermionic_fermionic_symm {a b : 𝓕.CrAnAlgebra} rw [superCommute_fermionic_fermionic hb ha] abel +lemma superCommute_expand_bosonicProj_fermionicProj (a b : 𝓕.CrAnAlgebra) : + [a, b]ₛca = bosonicProj a * bosonicProj b - bosonicProj b * bosonicProj a + + bosonicProj a * fermionicProj b - fermionicProj b * bosonicProj a + + fermionicProj a * bosonicProj b - bosonicProj b * fermionicProj a + + fermionicProj a * fermionicProj b + fermionicProj b * fermionicProj a := by + conv_lhs => rw [← bosonicProj_add_fermionicProj a, ← bosonicProj_add_fermionicProj b] + simp + rw [superCommute_bonsonic (by simp), superCommute_bosonic_fermionic (by simp) (by simp), + superCommute_fermionic_bonsonic (by simp) (by simp), + superCommute_fermionic_fermionic (by simp) (by simp)] + abel + lemma superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic (φs φs' : List 𝓕.CrAnStates) : [ofCrAnList φs, ofCrAnList φs']ₛca ∈ statisticSubmodule bosonic ∨ [ofCrAnList φs, ofCrAnList φs']ₛca ∈ statisticSubmodule fermionic := by @@ -725,6 +737,41 @@ lemma superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic (φs φs' : List apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h1) apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h2) +lemma superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic (φ φ' : 𝓕.CrAnStates) : + [ofCrAnState φ, ofCrAnState φ']ₛca ∈ statisticSubmodule bosonic ∨ + [ofCrAnState φ, ofCrAnState φ']ₛca ∈ statisticSubmodule fermionic := by + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton] + exact superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic [φ] [φ'] + +lemma superCommute_superCommute_ofCrAnState_bosonic_or_fermionic (φ1 φ2 φ3 : 𝓕.CrAnStates) : + [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca ∈ statisticSubmodule bosonic ∨ + [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca ∈ statisticSubmodule fermionic := by + rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φ2 φ3 with hs | hs + <;> rcases ofCrAnState_bosonic_or_fermionic φ1 with h1 | h1 + · left + have h : bosonic = bosonic + bosonic := by + simp only [add_eq_mul, instCommGroup, mul_self] + rfl + rw [h] + apply superCommute_grade h1 hs + · right + have h : fermionic = fermionic + bosonic := by + simp only [add_eq_mul, instCommGroup, mul_self] + rfl + rw [h] + apply superCommute_grade h1 hs + · right + have h : fermionic = bosonic + fermionic := by + simp only [add_eq_mul, instCommGroup, mul_self] + rfl + rw [h] + apply superCommute_grade h1 hs + · left + have h : bosonic = fermionic + fermionic := by + simp only [add_eq_mul, instCommGroup, mul_self] + rfl + rw [h] + apply superCommute_grade h1 hs lemma superCommute_bosonic_ofCrAnList_eq_sum (a : 𝓕.CrAnAlgebra) (φs : List 𝓕.CrAnStates) (ha : a ∈ statisticSubmodule bosonic) : diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean index aa71461..10993f0 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean @@ -191,5 +191,241 @@ lemma ι_superCommute_ofCrAnState_ofCrAnState_mem_center (φ ψ : 𝓕.CrAnState rw [← h0] abel +/-! + +## The kernal of ι +-/ + +lemma ι_eq_zero_iff_mem_ideal (x : CrAnAlgebra 𝓕) : + ι x = 0 ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by + rw [ι_apply] + change ⟦x⟧ = ⟦0⟧ ↔ _ + simp only [ringConGen, Quotient.eq] + rw [TwoSidedIdeal.mem_iff] + simp only + rfl + +lemma bosonicProj_mem_fieldOpIdealSet_or_zero (x : CrAnAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpIdealSet) : + x.bosonicProj.1 ∈ 𝓕.fieldOpIdealSet ∨ x.bosonicProj = 0 := by + have hx' := hx + simp [fieldOpIdealSet] at hx + rcases hx with ⟨φ1, φ2, φ3, rfl⟩ | ⟨φc, φc', hφc, hφc', rfl⟩ | ⟨φa, φa', hφa, hφa', rfl⟩ | + ⟨φ, φ', hdiff, rfl⟩ + · rcases superCommute_superCommute_ofCrAnState_bosonic_or_fermionic φ1 φ2 φ3 with h | h + · left + rw [bosonicProj_of_mem_bosonic _ h] + simpa using hx' + · right + rw [bosonicProj_of_mem_fermionic _ h] + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φc φc' with h | h + · left + rw [bosonicProj_of_mem_bosonic _ h] + simpa using hx' + · right + rw [bosonicProj_of_mem_fermionic _ h] + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φa φa' with h | h + · left + rw [bosonicProj_of_mem_bosonic _ h] + simpa using hx' + · right + rw [bosonicProj_of_mem_fermionic _ h] + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φ φ' with h | h + · left + rw [bosonicProj_of_mem_bosonic _ h] + simpa using hx' + · right + rw [bosonicProj_of_mem_fermionic _ h] + + +lemma fermionicProj_mem_fieldOpIdealSet_or_zero (x : CrAnAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpIdealSet) : + x.fermionicProj.1 ∈ 𝓕.fieldOpIdealSet ∨ x.fermionicProj = 0 := by + have hx' := hx + simp [fieldOpIdealSet] at hx + rcases hx with ⟨φ1, φ2, φ3, rfl⟩ | ⟨φc, φc', hφc, hφc', rfl⟩ | ⟨φa, φa', hφa, hφa', rfl⟩ | + ⟨φ, φ', hdiff, rfl⟩ + · rcases superCommute_superCommute_ofCrAnState_bosonic_or_fermionic φ1 φ2 φ3 with h | h + · right + rw [fermionicProj_of_mem_bosonic _ h] + · left + rw [fermionicProj_of_mem_fermionic _ h] + simpa using hx' + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φc φc' with h | h + · right + rw [fermionicProj_of_mem_bosonic _ h] + · left + rw [fermionicProj_of_mem_fermionic _ h] + simpa using hx' + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φa φa' with h | h + · right + rw [fermionicProj_of_mem_bosonic _ h] + · left + rw [fermionicProj_of_mem_fermionic _ h] + simpa using hx' + · rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic φ φ' with h | h + · right + rw [fermionicProj_of_mem_bosonic _ h] + · left + rw [fermionicProj_of_mem_fermionic _ h] + simpa using hx' + +lemma bosonicProj_mem_ideal (x : CrAnAlgebra 𝓕) (hx : x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : + x.bosonicProj.1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at hx + let p {k : Set 𝓕.CrAnAlgebra} (a : CrAnAlgebra 𝓕) (h : a ∈ AddSubgroup.closure k) : Prop := + a.bosonicProj.1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet + change p x hx + apply AddSubgroup.closure_induction + · intro x hx + simp [p] + obtain ⟨a, ha, b, hb, rfl⟩ := Set.mem_mul.mp hx + obtain ⟨d, hd, y, hy, rfl⟩ := Set.mem_mul.mp ha + rw [bosonicProj_mul, bosonicProj_mul, fermionicProj_mul] + simp [mul_add, add_mul] + rcases fermionicProj_mem_fieldOpIdealSet_or_zero y hy with hfy | hfy + <;> rcases bosonicProj_mem_fieldOpIdealSet_or_zero y hy with hby | hby + · apply TwoSidedIdeal.add_mem + apply TwoSidedIdeal.add_mem + · /- boson, boson, boson mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(bosonicProj d) * ↑(bosonicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use bosonicProj d + simp + use (bosonicProj y).1 + simp [hby] + · use ↑(bosonicProj b) + simp + · /- fermion, fermion, boson mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(fermionicProj d) * ↑(fermionicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use fermionicProj d + simp + use (fermionicProj y).1 + simp [hby, hfy] + · use ↑(bosonicProj b) + simp + apply TwoSidedIdeal.add_mem + · /- boson, fermion, fermion mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(bosonicProj d) * ↑(fermionicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use bosonicProj d + simp + use (fermionicProj y).1 + simp [hby, hfy] + · use ↑(fermionicProj b) + simp + · /- fermion, boson, fermion mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(fermionicProj d) * ↑(bosonicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use fermionicProj d + simp + use (bosonicProj y).1 + simp [hby, hfy] + · use ↑(fermionicProj b) + simp + · simp [hby] + apply TwoSidedIdeal.add_mem + · /- fermion, fermion, boson mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(fermionicProj d) * ↑(fermionicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use fermionicProj d + simp + use (fermionicProj y).1 + simp [hby, hfy] + · use ↑(bosonicProj b) + simp + · /- boson, fermion, fermion mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(bosonicProj d) * ↑(fermionicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use bosonicProj d + simp + use (fermionicProj y).1 + simp [hby, hfy] + · use ↑(fermionicProj b) + simp + · simp [hfy] + apply TwoSidedIdeal.add_mem + · /- boson, boson, boson mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(bosonicProj d) * ↑(bosonicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use bosonicProj d + simp + use (bosonicProj y).1 + simp [hby] + · use ↑(bosonicProj b) + simp + · /- fermion, boson, fermion mem-/ + rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] + refine Set.mem_of_mem_of_subset ?_ AddSubgroup.subset_closure + apply Set.mem_mul.mpr + use ↑(fermionicProj d) * ↑(bosonicProj y) + apply And.intro + · apply Set.mem_mul.mpr + use fermionicProj d + simp + use (bosonicProj y).1 + simp [hby, hfy] + · use ↑(fermionicProj b) + simp + · simp [hfy, hby] + · simp [p] + · intro x y hx hy hpx hpy + simp_all [p] + apply TwoSidedIdeal.add_mem + exact hpx + exact hpy + · intro x hx + simp [p] + +lemma fermionicProj_mem_ideal (x : CrAnAlgebra 𝓕) (hx : x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : + x.fermionicProj.1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by + have hb := bosonicProj_mem_ideal x hx + rw [← ι_eq_zero_iff_mem_ideal] at hx hb ⊢ + rw [← bosonicProj_add_fermionicProj x] at hx + simp at hx + simp_all + +lemma ι_eq_zero_iff_ι_bosonicProj_fermonicProj_zero (x : CrAnAlgebra 𝓕) : + ι x = 0 ↔ ι x.bosonicProj.1 = 0 ∧ ι x.fermionicProj.1 = 0 := by + apply Iff.intro + · intro h + rw [@ι_eq_zero_iff_mem_ideal] at h ⊢ + rw [ι_eq_zero_iff_mem_ideal] + apply And.intro + · exact bosonicProj_mem_ideal x h + · exact fermionicProj_mem_ideal x h + · intro h + rw [← bosonicProj_add_fermionicProj x] + simp_all + + + end FieldOpAlgebra end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean new file mode 100644 index 0000000..e555977 --- /dev/null +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2025 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.Algebras.CrAnAlgebra.TimeOrder +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic +/-! + +# SuperCommute on Field operator algebra + +-/ + +namespace FieldSpecification +open CrAnAlgebra +open HepLean.List +open FieldStatistic + +namespace FieldOpAlgebra +variable {𝓕 : FieldSpecification} + +lemma ι_superCommute_eq_zero_of_ι_right_zero (a b : 𝓕.CrAnAlgebra) (h : ι b = 0) : + ι [a, b]ₛca = 0 := by + rw [superCommute_expand_bosonicProj_fermionicProj] + rw [ι_eq_zero_iff_ι_bosonicProj_fermonicProj_zero] at h + simp_all + +lemma ι_superCommute_eq_zero_of_ι_left_zero (a b : 𝓕.CrAnAlgebra) (h : ι a = 0) : + ι [a, b]ₛca = 0 := by + rw [superCommute_expand_bosonicProj_fermionicProj] + rw [ι_eq_zero_iff_ι_bosonicProj_fermonicProj_zero] at h + simp_all + +/-! + +## Defining normal order for `FiedOpAlgebra`. + +-/ + +lemma ι_superCommute_right_zero_of_mem_ideal (a b : 𝓕.CrAnAlgebra) + (h : b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι [a, b]ₛca = 0 := by + apply ι_superCommute_eq_zero_of_ι_right_zero + exact (ι_eq_zero_iff_mem_ideal b).mpr h + +lemma ι_superCommute_eq_of_equiv_right (a b1 b2 : 𝓕.CrAnAlgebra) (h : b1 ≈ b2) : + ι [a, b1]ₛca = ι [a, b2]ₛca := by + rw [equiv_iff_sub_mem_ideal] at h + rw [LinearMap.sub_mem_ker_iff.mp] + simp only [LinearMap.mem_ker, ← map_sub] + exact ι_superCommute_right_zero_of_mem_ideal a (b1 - b2) h + +noncomputable def superCommuteRight (a : 𝓕.CrAnAlgebra) : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where + toFun := Quotient.lift (ι.toLinearMap ∘ₗ CrAnAlgebra.superCommute a) (ι_superCommute_eq_of_equiv_right a) + map_add' x y := by + obtain ⟨x, hx⟩ := ι_surjective x + obtain ⟨y, hy⟩ := ι_surjective y + subst hx hy + rw [← map_add, ι_apply, ι_apply, ι_apply] + rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk] + simp + map_smul' c y := by + obtain ⟨y, hy⟩ := ι_surjective y + subst hy + rw [← map_smul, ι_apply, ι_apply] + simp + +lemma superCommuteRight_apply_ι (a b : 𝓕.CrAnAlgebra) : superCommuteRight a (ι b) = ι [a, b]ₛca := by + rfl + +lemma superCommuteRight_apply_quot (a b : 𝓕.CrAnAlgebra) : superCommuteRight a ⟦b⟧= ι [a, b]ₛca := by + rfl + +lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.CrAnAlgebra) (h : a1 ≈ a2) : + superCommuteRight a1 = superCommuteRight a2 := by + rw [equiv_iff_sub_mem_ideal] at h + ext b + obtain ⟨b, rfl⟩ := ι_surjective b + have ha1b1 : (superCommuteRight (a1 - a2)) (ι b) = 0 := by + rw [superCommuteRight_apply_ι] + apply ι_superCommute_eq_zero_of_ι_left_zero + exact (ι_eq_zero_iff_mem_ideal (a1 - a2)).mpr h + simp_all [superCommuteRight_apply_ι] + trans ι ((superCommute a2) b) + 0 + rw [← ha1b1] + simp + simp + +noncomputable def superCommute : FieldOpAlgebra 𝓕 →ₗ[ℂ] + FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where + toFun := Quotient.lift superCommuteRight superCommuteRight_eq_of_equiv + map_add' x y := by + obtain ⟨x, rfl⟩ := ι_surjective x + obtain ⟨y, rfl⟩ := ι_surjective y + ext b + obtain ⟨b, rfl⟩ := ι_surjective b + rw [← map_add, ι_apply, ι_apply, ι_apply, ι_apply] + rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk] + simp + rw [superCommuteRight_apply_quot, superCommuteRight_apply_quot, superCommuteRight_apply_quot] + simp + map_smul' c y := by + obtain ⟨y, rfl⟩ := ι_surjective y + ext b + obtain ⟨b, rfl⟩ := ι_surjective b + rw [← map_smul, ι_apply, ι_apply, ι_apply] + simp + rw [superCommuteRight_apply_quot, superCommuteRight_apply_quot] + simp + +lemma ι_superCommute (a b : 𝓕.CrAnAlgebra) : ι [a, b]ₛca = superCommute (ι a) (ι b) := by + rfl + +end FieldOpAlgebra +end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean index 6db44c8..16b1e76 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean @@ -19,7 +19,164 @@ open FieldStatistic namespace FieldOpAlgebra variable {𝓕 : FieldSpecification} -lemma ι_timeOrder_superCommute_time {φ ψ : 𝓕.CrAnStates} +lemma ι_timeOrder_superCommute_superCommute_eq_time_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates} + (φs1 φs2 : List 𝓕.CrAnStates) (h : + crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ + crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ + crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2): + ι 𝓣ᶠ(ofCrAnList φs1 * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * ofCrAnList φs2) + = 0 := by + let l1 := + (List.takeWhile (fun c => ¬ crAnTimeOrderRel φ1 c) ((φs1 ++ φs2).insertionSort crAnTimeOrderRel)) + ++ (List.filter (fun c => crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1) φs1) + let l2 := (List.filter (fun c => crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1) φs2) + ++ (List.filter (fun c => crAnTimeOrderRel φ1 c ∧ ¬ crAnTimeOrderRel c φ1) ((φs1 ++ φs2).insertionSort crAnTimeOrderRel)) + have h123 : ι 𝓣ᶠ(ofCrAnList (φs1 ++ φ1 :: φ2 :: φ3 :: φs2)) = + crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) + • (ι (ofCrAnList l1) * ι (ofCrAnList [φ1, φ2, φ3]) * ι (ofCrAnList l2)):= by + have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ1, φ2, φ3] φs2 + (by simp_all) + rw [timeOrder_ofCrAnList, show φs1 ++ φ1 :: φ2 :: φ3 :: φs2 = φs1 ++ [φ1, φ2, φ3] ++ φs2 by simp, + crAnTimeOrderList, h1] + simp only [List.append_assoc, List.singleton_append, decide_not, + Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc] + have h132 : ι 𝓣ᶠ(ofCrAnList (φs1 ++ φ1 :: φ3 :: φ2 :: φs2)) = + crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) + • (ι (ofCrAnList l1) * ι (ofCrAnList [φ1, φ3, φ2]) * ι (ofCrAnList l2)):= by + have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ1, φ3, φ2] φs2 + (by simp_all) + rw [timeOrder_ofCrAnList, show φs1 ++ φ1 :: φ3 :: φ2 :: φs2 = φs1 ++ [φ1, φ3, φ2] ++ φs2 by simp, + crAnTimeOrderList, h1] + simp only [List.singleton_append, decide_not, + Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc] + congr 1 + have hp : List.Perm [φ1, φ3, φ2] [φ1, φ2, φ3] := by + refine List.Perm.cons φ1 ?_ + exact List.Perm.swap φ2 φ3 [] + rw [crAnTimeOrderSign, Wick.koszulSign_perm_eq _ _ φ1 _ _ _ _ _ hp, ← crAnTimeOrderSign] + · simp + · intro φ4 hφ4 + simp at hφ4 + rcases hφ4 with hφ4 | hφ4 | hφ4 + all_goals + subst hφ4 + simp_all + have hp231 : List.Perm [φ2, φ3, φ1] [φ1, φ2, φ3] := by + refine List.Perm.trans (l₂ := [φ2, φ1, φ3]) ?_ ?_ + refine List.Perm.cons φ2 (List.Perm.swap φ1 φ3 []) + exact List.Perm.swap φ1 φ2 [φ3] + have h231 : ι 𝓣ᶠ(ofCrAnList (φs1 ++ φ2 :: φ3 :: φ1 :: φs2)) = + crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) + • (ι (ofCrAnList l1) * ι (ofCrAnList [φ2, φ3, φ1]) * ι (ofCrAnList l2)):= by + have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ2, φ3, φ1] φs2 + (by simp_all) + rw [timeOrder_ofCrAnList, show φs1 ++ φ2 :: φ3 :: φ1 :: φs2 = φs1 ++ [φ2, φ3, φ1] ++ φs2 by simp, + crAnTimeOrderList, h1] + simp only [List.singleton_append, decide_not, + Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc] + congr 1 + rw [crAnTimeOrderSign, Wick.koszulSign_perm_eq _ _ φ1 _ _ _ _ _ hp231, ← crAnTimeOrderSign] + · simp + · intro φ4 hφ4 + simp at hφ4 + rcases hφ4 with hφ4 | hφ4 | hφ4 + all_goals + subst hφ4 + simp_all + have h321 : ι 𝓣ᶠ(ofCrAnList (φs1 ++ φ3 :: φ2 :: φ1 :: φs2)) = + crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) + • (ι (ofCrAnList l1) * ι (ofCrAnList [φ3, φ2, φ1]) * ι (ofCrAnList l2)):= by + have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ3, φ2, φ1] φs2 + (by simp_all) + rw [timeOrder_ofCrAnList, show φs1 ++ φ3 :: φ2 :: φ1 :: φs2 = φs1 ++ [φ3, φ2, φ1] ++ φs2 by simp, + crAnTimeOrderList, h1] + simp only [List.singleton_append, decide_not, + Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc] + congr 1 + have hp : List.Perm [φ3, φ2, φ1] [φ1, φ2, φ3] := by + refine List.Perm.trans ?_ hp231 + exact List.Perm.swap φ2 φ3 [φ1] + rw [crAnTimeOrderSign, Wick.koszulSign_perm_eq _ _ φ1 _ _ _ _ _ hp, ← crAnTimeOrderSign] + · simp + · intro φ4 hφ4 + simp at hφ4 + rcases hφ4 with hφ4 | hφ4 | hφ4 + all_goals + subst hφ4 + simp_all + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_singleton] + rw [superCommute_ofCrAnList_ofCrAnList] + simp + rw [superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList] + simp [mul_sub, sub_mul, ← ofCrAnList_append] + rw [h123, h132, h231, h321] + simp [smul_smul] + rw [mul_comm, ← smul_smul, mul_comm, ← smul_smul] + rw [← smul_sub, ← smul_sub, smul_smul, mul_comm, ← smul_smul, ← smul_sub] + simp + right + rw [← smul_mul_assoc, ← mul_smul_comm, mul_assoc] + + rw [← smul_mul_assoc, ← mul_smul_comm] + rw [smul_sub] + rw [← smul_mul_assoc, ← mul_smul_comm] + rw [← smul_mul_assoc, ← mul_smul_comm] + repeat rw [mul_assoc] + rw [← mul_sub, ← mul_sub, ← mul_sub] + rw [← sub_mul, ← sub_mul, ← sub_mul] + trans ι (ofCrAnList l1) * ι [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * ι (ofCrAnList l2) + rw [mul_assoc] + congr + rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, ← ofCrAnList_singleton] + rw [superCommute_ofCrAnList_ofCrAnList] + simp + rw [superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList] + simp [smul_sub] + simp_all + +lemma ι_timeOrder_superCommute_superCommute_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates} + (φs1 φs2 : List 𝓕.CrAnStates): + ι 𝓣ᶠ(ofCrAnList φs1 * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * ofCrAnList φs2) + = 0 := by + by_cases h : + crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ + crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ + crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2 + · exact ι_timeOrder_superCommute_superCommute_eq_time_ofCrAnList φs1 φs2 h + · rw [timeOrder_timeOrder_mid] + rw [timeOrder_superCommute_ofCrAnState_superCommute_all_not_crAnTimeOrderRel _ _ _ h] + simp + +@[simp] +lemma ι_timeOrder_superCommute_superCommute {φ1 φ2 φ3 : 𝓕.CrAnStates} (a b : 𝓕.CrAnAlgebra): + ι 𝓣ᶠ(a * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * b) = 0 := by + let pb (b : 𝓕.CrAnAlgebra) (hc : b ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) : + Prop := ι 𝓣ᶠ(a * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * b) = 0 + change pb b (Basis.mem_span _ b) + apply Submodule.span_induction + · intro x hx + obtain ⟨φs, rfl⟩ := hx + simp [pb] + let pa (a : 𝓕.CrAnAlgebra) (hc : a ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) : + Prop := ι 𝓣ᶠ(a * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * ofCrAnList φs) = 0 + change pa a (Basis.mem_span _ a) + apply Submodule.span_induction + · intro x hx + obtain ⟨φs', rfl⟩ := hx + simp [pa] + exact ι_timeOrder_superCommute_superCommute_ofCrAnList φs' φs + · simp [pa] + · intro x y hx hy hpx hpy + simp_all [pa,mul_add, add_mul] + · intro x hx hpx + simp_all [pa, hpx] + · simp [pb] + · intro x y hx hy hpx hpy + simp_all [pb,mul_add, add_mul] + · intro x hx hpx + simp_all [pb, hpx] + +lemma ι_timeOrder_superCommute_eq_time {φ ψ : 𝓕.CrAnStates} (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.CrAnAlgebra) : ι 𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca * b) = ι ([ofCrAnState φ, ofCrAnState ψ]ₛca * 𝓣ᶠ(a * b)) := by @@ -110,6 +267,25 @@ lemma ι_timeOrder_superCommute_time {φ ψ : 𝓕.CrAnStates} · intro x hx hpx simp_all [pb, hpx] + +lemma ι_timeOrder_superCommute_neq_time {φ ψ : 𝓕.CrAnStates} + (hφψ : ¬ (crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) (a b : 𝓕.CrAnAlgebra) : + ι 𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca * b) = 0 := by + rw [timeOrder_timeOrder_mid] + have hφψ : ¬ (crAnTimeOrderRel φ ψ) ∨ ¬ (crAnTimeOrderRel ψ φ) := by + exact Decidable.not_and_iff_or_not.mp hφψ + rcases hφψ with hφψ | hφψ + · rw [timeOrder_superCommute_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel ] + have ht := IsTotal.total (r := crAnTimeOrderRel) φ ψ + simp_all + simp_all + · rw [superCommute_ofCrAnState_ofCrAnState_symm] + simp + rw [timeOrder_superCommute_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel ] + simp + simp_all + + /-! ## Defining normal order for `FiedOpAlgebra`. @@ -130,16 +306,42 @@ lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra) match hc with | Or.inl hc => obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc - sorry + simp | Or.inr (Or.inl hc) => - obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc - sorry + obtain ⟨φa, hφa, φb, hφb, rfl⟩ := hc + by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa) + · rw [ι_timeOrder_superCommute_eq_time] + simp + rw [ι_superCommute_of_create_create] + simp + · exact hφa + · exact hφb + · exact heqt.1 + · exact heqt.2 + · rw [ι_timeOrder_superCommute_neq_time heqt] | Or.inr (Or.inr (Or.inl hc)) => - obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc - sorry + obtain ⟨φa, hφa, φb, hφb, rfl⟩ := hc + by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa) + · rw [ι_timeOrder_superCommute_eq_time] + simp + rw [ι_superCommute_of_annihilate_annihilate] + simp + · exact hφa + · exact hφb + · exact heqt.1 + · exact heqt.2 + · rw [ι_timeOrder_superCommute_neq_time heqt] | Or.inr (Or.inr (Or.inr hc)) => - obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc - sorry + obtain ⟨φa, φb, hdiff, rfl⟩ := hc + by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa) + · rw [ι_timeOrder_superCommute_eq_time] + simp + rw [ι_superCommute_of_diff_statistic] + simp + · exact hdiff + · exact heqt.1 + · exact heqt.2 + · rw [ι_timeOrder_superCommute_neq_time heqt] · simp [p] · intro x y hx hy simp only [map_add, p]