Imports
/-
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
-/
module
public import Physlib.QFT.PerturbationTheory.WickAlgebra.BasicSuperCommute on Field operator algebra
@[expose] public sectionlemma ι_superCommuteF_eq_zero_of_ι_right_zero (a b : 𝓕.FieldOpFreeAlgebra) (h : ι b = 0) :
ι [a, b]ₛF = 0 := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι b = 0⊢ ι ((superCommuteF a) b) = 0
𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι b = 0h1:ι ↑(bosonicProjF b) = 0h2:ι ↑(fermionicProjF b) = 0⊢ ι ((superCommuteF a) b) = 0
All goals completed! 🐙lemma ι_superCommuteF_eq_zero_of_ι_left_zero (a b : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) :
ι [a, b]ₛF = 0 := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι a = 0⊢ ι ((superCommuteF a) b) = 0
𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:ι a = 0h1:ι ↑(bosonicProjF a) = 0h2:ι ↑(fermionicProjF a) = 0⊢ ι ((superCommuteF a) b) = 0
All goals completed! 🐙
Defining normal order for FiedOpAlgebra.
lemma ι_superCommuteF_right_zero_of_mem_ideal (a b : 𝓕.FieldOpFreeAlgebra)
(h : b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι [a, b]ₛF = 0 :=
ι_superCommuteF_eq_zero_of_ι_right_zero a b ((ι_eq_zero_iff_mem_ideal b).mpr h)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab1:𝓕.FieldOpFreeAlgebrab2:𝓕.FieldOpFreeAlgebrah:b1 ≈ b2⊢ ι ((superCommuteF a) (b1 - b2)) = 0
All goals completed! 🐙lemma superCommuteRight_apply_ι (a b : 𝓕.FieldOpFreeAlgebra) :
superCommuteRight a (ι b) = ι [a, b]ₛF := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ (superCommuteRight a) (ι b) = ι ((superCommuteF a) b) All goals completed! 🐙lemma superCommuteRight_apply_quot (a b : 𝓕.FieldOpFreeAlgebra) :
superCommuteRight a ⟦b⟧= ι [a, b]ₛF := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ (superCommuteRight a) ⟦b⟧ = ι ((superCommuteF a) b) All goals completed! 🐙lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 ≈ a2) :
superCommuteRight a1 = superCommuteRight a2 := 𝓕:FieldSpecificationa1:𝓕.FieldOpFreeAlgebraa2:𝓕.FieldOpFreeAlgebrah:a1 ≈ a2⊢ superCommuteRight a1 = superCommuteRight a2
𝓕:FieldSpecificationa1:𝓕.FieldOpFreeAlgebraa2:𝓕.FieldOpFreeAlgebrah:a1 ≈ a2b:𝓕.WickAlgebra⊢ (superCommuteRight a1) b = (superCommuteRight a2) b
𝓕:FieldSpecificationa1:𝓕.FieldOpFreeAlgebraa2:𝓕.FieldOpFreeAlgebrah:a1 ≈ a2b:𝓕.FieldOpFreeAlgebra⊢ (superCommuteRight a1) (ι b) = (superCommuteRight a2) (ι b)
All goals completed! 🐙@[inherit_doc superCommute]
scoped[FieldSpecification.WickAlgebra] notation "[" a "," b "]ₛ" => superCommute a blemma superCommute_eq_ι_superCommuteF (a b : 𝓕.FieldOpFreeAlgebra) :
[ι a, ι b]ₛ = ι [a, b]ₛF := rfl
Properties of superCommute.
Properties from the definition of WickAlgebra
lemma superCommute_create_create {φ φ' : 𝓕.CrAnFieldOp}
(h : 𝓕 |>ᶜ φ = .create) (h' : 𝓕 |>ᶜ φ' = .create) :
[ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 :=
ι_superCommuteF_of_create_create _ _ h h'lemma superCommute_annihilate_annihilate {φ φ' : 𝓕.CrAnFieldOp}
(h : 𝓕 |>ᶜ φ = .annihilate) (h' : 𝓕 |>ᶜ φ' = .annihilate) :
[ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 :=
ι_superCommuteF_of_annihilate_annihilate _ _ h h'lemma superCommute_diff_statistic {φ φ' : 𝓕.CrAnFieldOp} (h : (𝓕 |>ₛ φ) ≠ 𝓕 |>ₛ φ') :
[ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 :=
ι_superCommuteF_of_diff_statistic h𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.FieldOph:𝓕.crAnStatistics φ ≠ 𝓕|>ₛψ⊢ ∑ x, (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨ψ, x⟩) = 0
𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.FieldOph:𝓕.crAnStatistics φ ≠ 𝓕|>ₛψx:𝓕.fieldOpToCrAnType ψx✝:x ∈ Finset.univ⊢ 𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ⟨ψ, x⟩
All goals completed! 🐙lemma superCommute_anPart_ofFieldOpF_diff_grade_zero (φ ψ : 𝓕.FieldOp)
(h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : [anPart φ, ofFieldOp ψ]ₛ = 0 := 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) = 0
𝓕:FieldSpecificationψ:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh:(𝓕|>ₛFieldOp.inAsymp a✝) ≠ 𝓕|>ₛψ⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (ofFieldOp ψ) = 0𝓕:FieldSpecificationψ:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh:(𝓕|>ₛFieldOp.position a✝) ≠ 𝓕|>ₛψ⊢ (superCommute (anPart (FieldOp.position a✝))) (ofFieldOp ψ) = 0𝓕:FieldSpecificationψ:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh:(𝓕|>ₛFieldOp.outAsymp a✝) ≠ 𝓕|>ₛψ⊢ (superCommute (anPart (FieldOp.outAsymp a✝))) (ofFieldOp ψ) = 0
𝓕:FieldSpecificationψ:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh:(𝓕|>ₛFieldOp.inAsymp a✝) ≠ 𝓕|>ₛψ⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (ofFieldOp ψ) = 0 All goals completed! 🐙
all_goals
exact superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero _ _ (𝓕:FieldSpecificationψ:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh:(𝓕|>ₛFieldOp.outAsymp a✝) ≠ 𝓕|>ₛψ⊢ 𝓕.crAnStatistics ⟨FieldOp.outAsymp a✝, ()⟩ ≠ 𝓕|>ₛψ All goals completed! 🐙)lemma superCommute_ofCrAnOp_ofCrAnOp_mem_center (φ φ' : 𝓕.CrAnFieldOp) :
[ofCrAnOp φ, ofCrAnOp φ']ₛ ∈ Subalgebra.center ℂ (WickAlgebra 𝓕) :=
ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center φ φ'lemma superCommute_ofCrAnOp_ofCrAnOp_commute (φ φ' : 𝓕.CrAnFieldOp)
(a : WickAlgebra 𝓕) :
a * [ofCrAnOp φ, ofCrAnOp φ']ₛ = [ofCrAnOp φ, ofCrAnOp φ']ₛ * a :=
Subalgebra.mem_center_iff.mp (superCommute_ofCrAnOp_ofCrAnOp_mem_center φ φ') a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.FieldOp⊢ ∑ x, (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨φ', x⟩) ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
All goals completed! 🐙lemma superCommute_ofCrAnOp_ofFieldOp_commute (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp)
(a : WickAlgebra 𝓕) : a * [ofCrAnOp φ, ofFieldOp φ']ₛ =
[ofCrAnOp φ, ofFieldOp φ']ₛ * a :=
Subalgebra.mem_center_iff.mp (superCommute_ofCrAnOp_ofFieldOp_mem_center φ φ') alemma superCommute_anPart_ofFieldOp_mem_center (φ φ' : 𝓕.FieldOp) :
[anPart φ, ofFieldOp φ']ₛ ∈ Subalgebra.center ℂ (WickAlgebra 𝓕) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ (superCommute (anPart φ)) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.position a✝))) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝))) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra All goals completed! 🐙
all_goals All goals completed! 🐙
superCommute on different constructors.
lemma superCommute_ofCrAnList_ofCrAnList (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnList φs, ofCrAnList φs']ₛ =
ofCrAnList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList (φs' ++ φs) :=
congrArg ι (superCommuteF_ofCrAnListF_ofCrAnListF φs φs')lemma superCommute_ofCrAnOp_ofCrAnOp (φ φ' : 𝓕.CrAnFieldOp) :
[ofCrAnOp φ, ofCrAnOp φ']ₛ = ofCrAnOp φ * ofCrAnOp φ' -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnOp φ' * ofCrAnOp φ :=
congrArg ι (superCommuteF_ofCrAnOpF_ofCrAnOpF φ φ')lemma superCommute_ofCrAnList_ofFieldOpList (φcas : List 𝓕.CrAnFieldOp)
(φs : List 𝓕.FieldOp) :
[ofCrAnList φcas, ofFieldOpList φs]ₛ = ofCrAnList φcas * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnList φcas :=
congrArg ι (superCommuteF_ofCrAnListF_ofFieldOpFsList φcas φs)lemma superCommute_ofFieldOpList_ofFieldOpList (φs φs' : List 𝓕.FieldOp) :
[ofFieldOpList φs, ofFieldOpList φs']ₛ = ofFieldOpList φs * ofFieldOpList φs' -
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOpList φs :=
congrArg ι (superCommuteF_ofFieldOpListF_ofFieldOpFsList φs φs')lemma superCommute_ofFieldOp_ofFieldOpList (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
[ofFieldOp φ, ofFieldOpList φs]ₛ = ofFieldOp φ * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofFieldOp φ :=
congrArg ι (superCommuteF_ofFieldOpF_ofFieldOpFsList φ φs)lemma superCommute_ofFieldOpList_ofFieldOp (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) :
[ofFieldOpList φs, ofFieldOp φ]ₛ = ofFieldOpList φs * ofFieldOp φ -
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofFieldOp φ * ofFieldOpList φs :=
congrArg ι (superCommuteF_ofFieldOpListF_ofFieldOpF φs φ)lemma superCommute_anPart_crPart (φ φ' : 𝓕.FieldOp) :
[anPart φ, crPart φ']ₛ = anPart φ * crPart φ' -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ :=
congrArg ι (superCommuteF_anPartF_crPartF φ φ')lemma superCommute_crPart_anPart (φ φ' : 𝓕.FieldOp) :
[crPart φ, anPart φ']ₛ = crPart φ * anPart φ' -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * crPart φ :=
congrArg ι (superCommuteF_crPartF_anPartF φ φ')@[simp]
lemma superCommute_crPart_crPart (φ φ' : 𝓕.FieldOp) : [crPart φ, crPart φ']ₛ = 0 := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ (superCommute (crPart φ)) (crPart φ') = 0
𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.inAsymp a✝))) (crPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.position a✝))) (crPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝))) (crPart φ') = 0 𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.inAsymp a✝))) (crPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.position a✝))) (crPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝))) (crPart φ') = 0 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.outAsymp a✝)) = 0 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.inAsymp a✝¹))) (crPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.inAsymp a✝¹))) (crPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.inAsymp a✝¹))) (crPart (FieldOp.outAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.position a✝¹))) (crPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.position a✝¹))) (crPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.position a✝¹))) (crPart (FieldOp.outAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (crPart (FieldOp.outAsymp a✝¹))) (crPart (FieldOp.outAsymp a✝)) = 0
All goals completed! 🐙@[simp]
lemma superCommute_anPart_anPart (φ φ' : 𝓕.FieldOp) : [anPart φ, anPart φ']ₛ = 0 := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ (superCommute (anPart φ)) (anPart φ') = 0
𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (anPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.position a✝))) (anPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝))) (anPart φ') = 0 𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝))) (anPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.position a✝))) (anPart φ') = 0𝓕:FieldSpecificationφ':𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝))) (anPart φ') = 0 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.outAsymp a✝)) = 0 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝¹))) (anPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.inAsymp a✝¹))) (anPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp a✝¹))) (anPart (FieldOp.outAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.position a✝¹))) (anPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.position a✝¹))) (anPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.position a✝¹))) (anPart (FieldOp.outAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.inAsymp a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.position a✝)) = 0𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp a✝¹))) (anPart (FieldOp.outAsymp a✝)) = 0
All goals completed! 🐙lemma superCommute_crPart_ofFieldOpList (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
[crPart φ, ofFieldOpList φs]ₛ = crPart φ * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * crPart φ :=
congrArg ι (superCommuteF_crPartF_ofFieldOpListF φ φs)lemma superCommute_anPart_ofFieldOpList (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
[anPart φ, ofFieldOpList φs]ₛ = anPart φ * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * anPart φ :=
congrArg ι (superCommuteF_anPartF_ofFieldOpListF φ φs)lemma superCommute_crPart_ofFieldOp (φ φ' : 𝓕.FieldOp) :
[crPart φ, ofFieldOp φ']ₛ = crPart φ * ofFieldOp φ' -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofFieldOp φ' * crPart φ :=
congrArg ι (superCommuteF_crPartF_ofFieldOpF φ φ')lemma superCommute_anPart_ofFieldOp (φ φ' : 𝓕.FieldOp) :
[anPart φ, ofFieldOp φ']ₛ = anPart φ * ofFieldOp φ' -
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofFieldOp φ' * anPart φ :=
congrArg ι (superCommuteF_anPartF_ofFieldOpF φ φ')Mul equal superCommute
Lemmas which rewrite a multiplication of two elements of the algebra as their commuted multiplication with a sign plus the super commutator.
lemma ofCrAnList_mul_ofCrAnList_eq_superCommute (φs φs' : List 𝓕.CrAnFieldOp) :
ofCrAnList φs * ofCrAnList φs' =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnList φs
+ [ofCrAnList φs, ofCrAnList φs']ₛ := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ ofCrAnList φs * ofCrAnList φs' =
(exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') • ofCrAnList φs' * ofCrAnList φs +
(superCommute (ofCrAnList φs)) (ofCrAnList φs')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ (exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs') • ofCrAnList φs' * ofCrAnList [φ] +
(superCommute (ofCrAnList [φ])) (ofCrAnList φs') =
(exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs') • ofCrAnList φs' * ofCrAnList [φ] +
(superCommute (ofCrAnList [φ])) (ofCrAnList φs')
All goals completed! 🐙lemma ofFieldOpList_mul_ofFieldOpList_eq_superCommute (φs φs' : List 𝓕.FieldOp) :
ofFieldOpList φs * ofFieldOpList φs' =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOpList φs
+ [ofFieldOpList φs, ofFieldOpList φs']ₛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ofFieldOpList φs * ofFieldOpList φs' =
(exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofFieldOpList φs +
(superCommute (ofFieldOpList φs)) (ofFieldOpList φs')
All goals completed! 🐙lemma ofFieldOp_mul_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp) (φs' : List 𝓕.FieldOp) :
ofFieldOp φ * ofFieldOpList φs' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOp φ
+ [ofFieldOp φ, ofFieldOpList φs']ₛ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ofFieldOp φ * ofFieldOpList φs' =
(exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofFieldOp φ +
(superCommute (ofFieldOp φ)) (ofFieldOpList φs')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic [φ']) • ofFieldOpList [φ'] * ofFieldOp φ +
(superCommute (ofFieldOp φ)) (ofFieldOpList [φ']) =
(exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ofFieldOpList [φ'] * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOpList [φ'])
All goals completed! 🐙lemma ofFieldOpList_mul_ofFieldOp_eq_superCommute (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) :
ofFieldOpList φs * ofFieldOp φ = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofFieldOp φ * ofFieldOpList φs
+ [ofFieldOpList φs, ofFieldOp φ]ₛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOp⊢ ofFieldOpList φs * ofFieldOp φ =
(exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (𝓕|>ₛφ) • ofFieldOp φ * ofFieldOpList φs +
(superCommute (ofFieldOpList φs)) (ofFieldOp φ)
All goals completed! 🐙lemma ofCrAnList_mul_ofFieldOpList_eq_superCommute (φs : List 𝓕.CrAnFieldOp)
(φs' : List 𝓕.FieldOp) : ofCrAnList φs * ofFieldOpList φs' =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofCrAnList φs
+ [ofCrAnList φs, ofFieldOpList φs']ₛ := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.FieldOp⊢ ofCrAnList φs * ofFieldOpList φs' =
(exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofCrAnList φs +
(superCommute (ofCrAnList φs)) (ofFieldOpList φs')
All goals completed! 🐙lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.FieldOp) :
crPart φ * anPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * crPart φ
+ [crPart φ, anPart φ']ₛ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ crPart φ * anPart φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • anPart φ' * crPart φ + (superCommute (crPart φ)) (anPart φ')
All goals completed! 🐙lemma anPart_mul_crPart_eq_superCommute (φ φ' : 𝓕.FieldOp) :
anPart φ * crPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ
+ [anPart φ, crPart φ']ₛ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ anPart φ * crPart φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • crPart φ' * anPart φ + (superCommute (anPart φ)) (crPart φ')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ crPart φ * crPart φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • crPart φ' * crPart φ = (superCommute (crPart φ)) (crPart φ')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ anPart φ * anPart φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • anPart φ' * anPart φ = (superCommute (anPart φ)) (anPart φ')
All goals completed! 🐙Symmetry of the super commutator.
lemma superCommute_ofCrAnList_ofCrAnList_symm (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnList φs, ofCrAnList φs']ₛ =
(- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnList φs', ofCrAnList φs]ₛ :=
congrArg ι (superCommuteF_ofCrAnListF_ofCrAnListF_symm φs φs')lemma superCommute_ofCrAnOp_ofCrAnOp_symm (φ φ' : 𝓕.CrAnFieldOp) :
[ofCrAnOp φ, ofCrAnOp φ']ₛ =
(- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • [ofCrAnOp φ', ofCrAnOp φ]ₛ :=
congrArg ι (superCommuteF_ofCrAnOpF_ofCrAnOpF_symm φ φ')splitting the super commute into sums
𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ ∑ x,
ι
((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑x) φs')) •
ofCrAnListF (List.take (↑x) φs') *
(superCommuteF (ofCrAnListF φs)) (ofCrAnOpF (φs'.get x)) *
ofCrAnListF (List.drop (↑x + 1) φs')) =
∑ n,
(exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) •
ofCrAnList (List.take (↑n) φs') *
(superCommute (ι (ofCrAnListF φs))) (ofCrAnOp (φs'.get n)) *
ofCrAnList (List.drop (↑n + 1) φs')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpn:Fin φs'.lengthx✝:n ∈ Finset.univ⊢ (superCommute (ofCrAnOp φ)) (ofCrAnOp (φs'.get n)) *
(exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) •
ofCrAnList (List.take (↑n) φs') *
ofCrAnList (List.drop (↑n + 1) φs') =
(exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) •
(superCommute (ofCrAnOp φ)) (ofCrAnOp (φs'.get n)) *
ofCrAnList (φs'.eraseIdx ↑n)
All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.FieldOp⊢ ∑ x,
ι
((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs')) •
ofFieldOpListF (List.take (↑x) φs') *
(superCommuteF (ofCrAnListF φs)) (ofFieldOpF (φs'.get x)) *
ofFieldOpListF (List.drop (↑x + 1) φs')) =
∑ n,
(exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) •
ofFieldOpList (List.take (↑n) φs') *
(superCommute (ι (ofCrAnListF φs))) (ofFieldOp (φs'.get n)) *
ofFieldOpList (List.drop (↑n + 1) φs')
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs':List 𝓕.FieldOpn:Fin φs'.lengthx✝:n ∈ Finset.univ⊢ (superCommute (ofCrAnOp φ)) (ofFieldOp (φs'.get n)) *
(exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) •
ofFieldOpList (List.take (↑n) φs') *
ofFieldOpList (List.drop (↑n + 1) φs') =
(exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) •
(superCommute (ofCrAnOp φ)) (ofFieldOp (φs'.get n)) *
ofFieldOpList (φs'.eraseIdx ↑n)
All goals completed! 🐙