SuperCommute on Field operator algebra

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_eq_zero_of_ι_right_zero {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : ι b = 0) : ι ((FieldOpFreeAlgebra.superCommuteF a) b) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_eq_zero_of_ι_left_zero {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) : ι ((FieldOpFreeAlgebra.superCommuteF a) b) = 0

Defining normal order for FiedOpAlgebra.

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_right_zero_of_mem_ideal {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : b ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι ((FieldOpFreeAlgebra.superCommuteF a) b) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_eq_of_equiv_right {𝓕 : FieldSpecification} (a b1 b2 : 𝓕.FieldOpFreeAlgebra) (h : b1 ≈ b2) : ι ((FieldOpFreeAlgebra.superCommuteF a) b1) = ι ((FieldOpFreeAlgebra.superCommuteF a) b2)

noncomputable def FieldSpecification.WickAlgebra.superCommuteRight {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : 𝓕.WickAlgebra →ₗ[ℂ] 𝓕.WickAlgebra

The super commutator on the WickAlgebra defined as a linear map [a,_]ₛ.

Equations

• One or more equations did not get rendered due to their size.

theorem FieldSpecification.WickAlgebra.superCommuteRight_apply_ι {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) : (superCommuteRight a) (ι b) = ι ((FieldOpFreeAlgebra.superCommuteF a) b)

theorem FieldSpecification.WickAlgebra.superCommuteRight_apply_quot {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) : (superCommuteRight a) ⟦b⟧ = ι ((FieldOpFreeAlgebra.superCommuteF a) b)

theorem FieldSpecification.WickAlgebra.superCommuteRight_eq_of_equiv {𝓕 : FieldSpecification} (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 ≈ a2) : superCommuteRight a1 = superCommuteRight a2

noncomputable def FieldSpecification.WickAlgebra.superCommute {𝓕 : FieldSpecification} : 𝓕.WickAlgebra →ₗ[ℂ] 𝓕.WickAlgebra →ₗ[ℂ] 𝓕.WickAlgebra

For a field specification 𝓕, superCommute is the linear map

WickAlgebra 𝓕 →ₗ[ℂ] WickAlgebra 𝓕 →ₗ[ℂ] WickAlgebra 𝓕

defined as the descent of ι ∘ superCommuteF in both arguments. In particular for φs and φs' lists of 𝓕.CrAnFieldOp in WickAlgebra 𝓕 the following relation holds:

superCommute φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs

The notation [a, b]ₛ is used for superCommute a b.

Equations

• FieldSpecification.WickAlgebra.superCommute = { toFun := Quotient.lift FieldSpecification.WickAlgebra.superCommuteRight ⋯, map_add' := ⋯, map_smul' := ⋯ }

def FieldSpecification.WickAlgebra.«term[_,_]ₛ» : Lean.ParserDescr

For a field specification 𝓕, superCommute is the linear map

WickAlgebra 𝓕 →ₗ[ℂ] WickAlgebra 𝓕 →ₗ[ℂ] WickAlgebra 𝓕

defined as the descent of ι ∘ superCommuteF in both arguments. In particular for φs and φs' lists of 𝓕.CrAnFieldOp in WickAlgebra 𝓕 the following relation holds:

superCommute φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs

The notation [a, b]ₛ is used for superCommute a b.

Equations

• One or more equations did not get rendered due to their size.

theorem FieldSpecification.WickAlgebra.superCommute_eq_ι_superCommuteF {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) : (superCommute (ι a)) (ι b) = ι ((FieldOpFreeAlgebra.superCommuteF a) b)

Properties of superCommute.

Properties from the definition of WickAlgebra

theorem FieldSpecification.WickAlgebra.superCommute_create_create {𝓕 : FieldSpecification} {φ φ' : 𝓕.CrAnFieldOp} (h : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create) (h' : 𝓕.crAnFieldOpToCreateAnnihilate φ' = CreateAnnihilate.create) : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = 0

theorem FieldSpecification.WickAlgebra.superCommute_annihilate_annihilate {𝓕 : FieldSpecification} {φ φ' : 𝓕.CrAnFieldOp} (h : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate) (h' : 𝓕.crAnFieldOpToCreateAnnihilate φ' = CreateAnnihilate.annihilate) : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = 0

theorem FieldSpecification.WickAlgebra.superCommute_diff_statistic {𝓕 : FieldSpecification} {φ φ' : 𝓕.CrAnFieldOp} (h : 𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics φ') : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = 0

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (ψ : 𝓕.FieldOp) (h : 𝓕.crAnStatistics φ ≠ 𝓕.fieldOpStatistic ψ) : (superCommute (ofCrAnOp φ)) (ofFieldOp ψ) = 0

theorem FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : 𝓕.fieldOpStatistic φ ≠ 𝓕.fieldOpStatistic ψ) : (superCommute (anPart φ)) (ofFieldOp ψ) = 0

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_mem_center {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_commute {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) (a : 𝓕.WickAlgebra) : a * (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') * a

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_mem_center {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp) : (superCommute (ofCrAnOp φ)) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_commute {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp) (a : 𝓕.WickAlgebra) : a * (superCommute (ofCrAnOp φ)) (ofFieldOp φ') = (superCommute (ofCrAnOp φ)) (ofFieldOp φ') * a

theorem FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp_mem_center {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (anPart φ)) (ofFieldOp φ') ∈ Subalgebra.center ℂ 𝓕.WickAlgebra

superCommute on different constructors.

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommute (ofCrAnList φs)) (ofCrAnList φs') = ofCrAnList (φs ++ φs') - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnList (φs' ++ φs)

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = ofCrAnOp φ * ofCrAnOp φ' - (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') • ofCrAnOp φ' * ofCrAnOp φ

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList {𝓕 : FieldSpecification} (φcas : List 𝓕.CrAnFieldOp) (φs : List 𝓕.FieldOp) : (superCommute (ofCrAnList φcas)) (ofFieldOpList φs) = ofCrAnList φcas * ofFieldOpList φs - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φcas)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpList φs * ofCrAnList φcas

theorem FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList {𝓕 : FieldSpecification} (φs φs' : List 𝓕.FieldOp) : (superCommute (ofFieldOpList φs)) (ofFieldOpList φs') = ofFieldOpList φs * ofFieldOpList φs' - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofFieldOpList φs

theorem FieldSpecification.WickAlgebra.superCommute_ofFieldOp_ofFieldOpList {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommute (ofFieldOp φ)) (ofFieldOpList φs) = ofFieldOp φ * ofFieldOpList φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpList φs * ofFieldOp φ

theorem FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOp {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) : (superCommute (ofFieldOpList φs)) (ofFieldOp φ) = ofFieldOpList φs * ofFieldOp φ - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (𝓕.fieldOpStatistic φ) • ofFieldOp φ * ofFieldOpList φs

theorem FieldSpecification.WickAlgebra.superCommute_anPart_crPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (anPart φ)) (crPart φ') = anPart φ * crPart φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPart φ' * anPart φ

theorem FieldSpecification.WickAlgebra.superCommute_crPart_anPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (crPart φ)) (anPart φ') = crPart φ * anPart φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPart φ' * crPart φ

@[simp]

theorem FieldSpecification.WickAlgebra.superCommute_crPart_crPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (crPart φ)) (crPart φ') = 0

@[simp]

theorem FieldSpecification.WickAlgebra.superCommute_anPart_anPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (anPart φ)) (anPart φ') = 0

theorem FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOpList {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommute (crPart φ)) (ofFieldOpList φs) = crPart φ * ofFieldOpList φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpList φs * crPart φ

theorem FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpList {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommute (anPart φ)) (ofFieldOpList φs) = anPart φ * ofFieldOpList φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpList φs * anPart φ

theorem FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOp {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (crPart φ)) (ofFieldOp φ') = crPart φ * ofFieldOp φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • ofFieldOp φ' * crPart φ

theorem FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommute (anPart φ)) (ofFieldOp φ') = anPart φ * ofFieldOp φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • ofFieldOp φ' * anPart φ

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.

theorem FieldSpecification.WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : ofCrAnList φs * ofCrAnList φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnList φs' * ofCrAnList φs + (superCommute (ofCrAnList φs)) (ofCrAnList φs')

theorem FieldSpecification.WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.CrAnFieldOp) : ofCrAnOp φ * ofCrAnList φs' = (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnList φs' * ofCrAnOp φ + (superCommute (ofCrAnOp φ)) (ofCrAnList φs')

theorem FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute {𝓕 : FieldSpecification} (φs φs' : List 𝓕.FieldOp) : ofFieldOpList φs * ofFieldOpList φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofFieldOpList φs + (superCommute (ofFieldOpList φs)) (ofFieldOpList φs')

theorem FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs' : List 𝓕.FieldOp) : ofFieldOp φ * ofFieldOpList φs' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOpList φs')

theorem FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : ofFieldOp φ * ofFieldOp φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • ofFieldOp φ' * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOp φ')

theorem FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) : ofFieldOpList φs * ofFieldOp φ = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (𝓕.fieldOpStatistic φ) • ofFieldOp φ * ofFieldOpList φs + (superCommute (ofFieldOpList φs)) (ofFieldOp φ)

theorem FieldSpecification.WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : ofCrAnList φs * ofFieldOpList φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpList φs' * ofCrAnList φs + (superCommute (ofCrAnList φs)) (ofFieldOpList φs')

theorem FieldSpecification.WickAlgebra.crPart_mul_anPart_eq_superCommute {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : crPart φ * anPart φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPart φ' * crPart φ + (superCommute (crPart φ)) (anPart φ')

theorem FieldSpecification.WickAlgebra.anPart_mul_crPart_eq_superCommute {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : anPart φ * crPart φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPart φ' * anPart φ + (superCommute (anPart φ)) (crPart φ')

theorem FieldSpecification.WickAlgebra.crPart_mul_crPart_swap {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : crPart φ * crPart φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPart φ' * crPart φ

theorem FieldSpecification.WickAlgebra.anPart_mul_anPart_swap {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : anPart φ * anPart φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPart φ' * anPart φ

Symmetry of the super commutator.

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommute (ofCrAnList φs)) (ofCrAnList φs') = -(FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • (superCommute (ofCrAnList φs')) (ofCrAnList φs)

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_symm {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommute (ofCrAnOp φ)) (ofCrAnOp φ') = -(FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') • (superCommute (ofCrAnOp φ')) (ofCrAnOp φ)

splitting the super commute into sums

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommute (ofCrAnList φs)) (ofCrAnList φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑n) φs')) • ofCrAnList (List.take (↑n) φs') * (superCommute (ofCrAnList φs)) (ofCrAnOp (φs'.get n)) * ofCrAnList (List.drop (↑n + 1) φs')

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.CrAnFieldOp) : (superCommute (ofCrAnOp φ)) (ofCrAnList φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑n) φs')) • (superCommute (ofCrAnOp φ)) (ofCrAnOp (φs'.get n)) * ofCrAnList (φs'.eraseIdx ↑n)

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : (superCommute (ofCrAnList φs)) (ofFieldOpList φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) • ofFieldOpList (List.take (↑n) φs') * (superCommute (ofCrAnList φs)) (ofFieldOp (φs'.get n)) * ofFieldOpList (List.drop (↑n + 1) φs')

theorem FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : (superCommute (ofCrAnOp φ)) (ofFieldOpList φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) • (superCommute (ofCrAnOp φ)) (ofFieldOp (φs'.get n)) * ofFieldOpList (φs'.eraseIdx ↑n)