1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickAlgebra
  5. Basic
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.FieldOpFreeAlgebra.SuperCommute public import Mathlib.Algebra.RingQuot public import Mathlib.RingTheory.TwoSidedIdeal.Operations

The Wick Algebra

This is the algebra with the minimal assumptions necessary to prove Wick's theorem. It satisfies the appropriate universality conditions with respect to the operator algebra.

@[expose] public section

The set contains the super-commutators equal to zero in the operator algebra. This contains e.g. the super-commutator of two creation operators.

def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) := { x | (∃ (φ1 φ2 φ3 : 𝓕.CrAnFieldOp), x = [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF) ∨ (∃ (φc φc' : 𝓕.CrAnFieldOp) (_ : 𝓕 |>ᶜ φc = .create) (_ : 𝓕 |>ᶜ φc' = .create), x = [ofCrAnOpF φc, ofCrAnOpF φc']ₛF) ∨ (∃ (φa φa' : 𝓕.CrAnFieldOp) (_ : 𝓕 |>ᶜ φa = .annihilate) (_ : 𝓕 |>ᶜ φa' = .annihilate), x = [ofCrAnOpF φa, ofCrAnOpF φa']ₛF) ∨ (∃ (φ φ' : 𝓕.CrAnFieldOp) (_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')), x = [ofCrAnOpF φ, ofCrAnOpF φ']ₛF)}

For a field specification 𝓕, the algebra 𝓕.WickAlgebra is defined as the quotient of the free algebra 𝓕.FieldOpFreeAlgebra by the ideal generated by

    [ofCrAnOpF φc, ofCrAnOpF φc']ₛF for φc and φc' field creation operators. This corresponds to the condition that two creation operators always super-commute.

    [ofCrAnOpF φa, ofCrAnOpF φa']ₛF for φa and φa' field annihilation operators. This corresponds to the condition that two annihilation operators always super-commute.

    [ofCrAnOpF φ, ofCrAnOpF φ']ₛF for φ and φ' operators with different statistics. This corresponds to the condition that two operators with different statistics always super-commute. In other words, fermions and bosons always super-commute.

    [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF. This corresponds to the condition, when combined with the conditions above, that the super-commutator is in the center of the algebra.

def WickAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
instance : Semiring (𝓕.WickAlgebra) := inferInstanceAs <| Semiring <| (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotientinstance : Algebra ℂ (𝓕.WickAlgebra) := inferInstanceAs <| Algebra ℂ <| (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotientinstance: Ring (𝓕.WickAlgebra) := inferInstanceAs <| Ring <| (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotientinstance : Coe (𝓕.FieldOpFreeAlgebra) (𝓕.WickAlgebra) := ⟨(TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toQuotient⟩

The instance of a setoid on FieldOpFreeAlgebra from the ideal TwoSidedIdeal.

instance : Setoid (FieldOpFreeAlgebra 𝓕) := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid
𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ x ≈ y ↔ (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon x y All goals completed! 🐙𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrah:x - y ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ∃ a, x = y + a ∧ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet All goals completed! 🐙 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrah:∃ a, x = y + a ∧ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ x ≈ y 𝓕:FieldSpecificationy:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ y + a ≈ y All goals completed! 🐙

For a field specification 𝓕, ι is defined as the projection

𝓕.FieldOpFreeAlgebra →ₐ[ℂ] 𝓕.WickAlgebra

taking each element of 𝓕.FieldOpFreeAlgebra to its equivalence class in WickAlgebra 𝓕.

def ι : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] WickAlgebra 𝓕 where toFun := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.mk' map_one' := rfl map_mul' _ _ := rfl map_zero' := rfl map_add' _ _ := rfl commutes' _ := rfl
lemma ι_surjective : Function.Surjective (@ι 𝓕) := 𝓕:FieldSpecification⊢ Function.Surjective ⇑ι 𝓕:FieldSpecificationx:𝓕.WickAlgebra⊢ ∃ a, ι a = x 𝓕:FieldSpecificationx✝:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebra⊢ ∃ a, ι a = Quot.mk (⇑(TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid) x All goals completed! 🐙lemma ι_apply (x : FieldOpFreeAlgebra 𝓕) : ι x = Quotient.mk _ x := rfl𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ 𝓕.fieldOpIdealSet⊢ ⟦x⟧ = 0 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ 𝓕.fieldOpIdealSet⊢ ⟦x⟧ = ⟦0⟧ 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ 𝓕.fieldOpIdealSet⊢ RingConGen.Rel (fun a b => a - b ∈ 𝓕.fieldOpIdealSet) x 0 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ 𝓕.fieldOpIdealSet⊢ x - 0 ∈ 𝓕.fieldOpIdealSet All goals completed! 🐙lemma ι_superCommuteF_of_create_create (φc φc' : 𝓕.CrAnFieldOp) (hφc : 𝓕 |>ᶜ φc = .create) (hφc' : 𝓕 |>ᶜ φc' = .create) : ι [ofCrAnOpF φc, ofCrAnOpF φc']ₛF = 0 := 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.create⊢ ι ((superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc')) = 0 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.create⊢ (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc') ∈ 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.create⊢ (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc') ∈ {x | (∃ φ1 φ2 φ3, x = (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) ∨ (∃ φc φc', ∃ (_ : 𝓕|>ᶜφc = CreateAnnihilate.create) (_ : 𝓕|>ᶜφc' = CreateAnnihilate.create), x = (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc')) ∨ (∃ φa φa', ∃ (_ : 𝓕|>ᶜφa = CreateAnnihilate.annihilate) (_ : 𝓕|>ᶜφa' = CreateAnnihilate.annihilate), x = (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa')) ∨ ∃ φ φ', ∃ (_ : ¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φ'), x = (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ')} All goals completed! 🐙lemma ι_superCommuteF_of_annihilate_annihilate (φa φa' : 𝓕.CrAnFieldOp) (hφa : 𝓕 |>ᶜ φa = .annihilate) (hφa' : 𝓕 |>ᶜ φa' = .annihilate) : ι [ofCrAnOpF φa, ofCrAnOpF φa']ₛF = 0 := 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilate⊢ ι ((superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa')) = 0 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilate⊢ (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa') ∈ 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilate⊢ (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa') ∈ {x | (∃ φ1 φ2 φ3, x = (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) ∨ (∃ φc φc', ∃ (_ : 𝓕|>ᶜφc = CreateAnnihilate.create) (_ : 𝓕|>ᶜφc' = CreateAnnihilate.create), x = (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc')) ∨ (∃ φa φa', ∃ (_ : 𝓕|>ᶜφa = CreateAnnihilate.annihilate) (_ : 𝓕|>ᶜφa' = CreateAnnihilate.annihilate), x = (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa')) ∨ ∃ φ φ', ∃ (_ : ¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φ'), x = (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ')} All goals completed! 🐙lemma ι_superCommuteF_of_diff_statistic {φ ψ : 𝓕.CrAnFieldOp} (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF = 0 := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ⊢ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ {x | (∃ φ1 φ2 φ3, x = (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) ∨ (∃ φc φc', ∃ (_ : 𝓕|>ᶜφc = CreateAnnihilate.create) (_ : 𝓕|>ᶜφc' = CreateAnnihilate.create), x = (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φc')) ∨ (∃ φa φa', ∃ (_ : 𝓕|>ᶜφa = CreateAnnihilate.annihilate) (_ : 𝓕|>ᶜφa' = CreateAnnihilate.annihilate), x = (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF φa')) ∨ ∃ φ φ', ∃ (_ : ¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φ'), x = (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ')} All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionic⊢ ι ((superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ])) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:ofList 𝓕.crAnStatistics [φ] ≠ ofList 𝓕.crAnStatistics [ψ]⊢ ι ((superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ])) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) = 0⊢ ι ((superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ])) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:ofList 𝓕.crAnStatistics [φ] ≠ ofList 𝓕.crAnStatistics [ψ]⊢ ι ((superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ])) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:ofList 𝓕.crAnStatistics [φ] ≠ ofList 𝓕.crAnStatistics [ψ]⊢ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:ofList 𝓕.crAnStatistics [φ] ≠ ofList 𝓕.crAnStatistics [ψ]⊢ 𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph✝:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionich:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) = 0⊢ ι ((superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ])) = 0 All goals completed! 🐙lemma ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero (φ ψ : 𝓕.CrAnFieldOp) : [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF ∈ statisticSubmodule bosonic ∨ ι [ofCrAnOpF φ, ofCrAnOpF ψ]ₛF = 0 := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOp⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule bosonic⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionic⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule bosonic⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [ψ]) ∈ statisticSubmodule fermionic⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule fermionic⊢ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) ∈ statisticSubmodule bosonic ∨ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = 0 All goals completed! 🐙

Super-commutes are in the center

@[simp] lemma ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) : ι [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF = 0 := 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOp⊢ ι ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) = 0 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOp⊢ (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) ∈ 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOp⊢ (∃ φ1_1 φ2_1 φ3_1, (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) = (superCommuteF (ofCrAnOpF φ1_1)) ((superCommuteF (ofCrAnOpF φ2_1)) (ofCrAnOpF φ3_1))) ∨ (∃ φc, 𝓕|>ᶜφc = CreateAnnihilate.create ∧ ∃ x, 𝓕|>ᶜx = CreateAnnihilate.create ∧ (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) = (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF x)) ∨ (∃ φa, 𝓕|>ᶜφa = CreateAnnihilate.annihilate ∧ ∃ x, 𝓕|>ᶜx = CreateAnnihilate.annihilate ∧ (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) = (superCommuteF (ofCrAnOpF φa)) (ofCrAnOpF x)) ∨ ∃ φ φ', ¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φ' ∧ (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) = (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionich':ofCrAnListF [φ3] ∈ statisticSubmodule fermionic⊢ ι ((superCommuteF (ofCrAnListF [φ3])) ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) = 0 All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]) ∈ statisticSubmodule fermionic⊢ ι (∑ n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) • ofCrAnListF (List.take (↑n) φs) * (superCommuteF ((superCommuteF (ofCrAnListF [φ1])) (ofCrAnListF [φ2]))) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (↑n + 1) φs)) = 0 All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah1:ι.toLinearMap ∘ₗ superCommuteF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) = 0⊢ (ι.toLinearMap ∘ₗ superCommuteF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) a = 0 All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah:(superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) ∈ statisticSubmodule bosonic⊢ ι a * ι ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) - ι ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) * ι a = -ι ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) * a - a * (superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2)) All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah:(superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2) ∈ statisticSubmodule bosonic⊢ -ι ((superCommuteF ((superCommuteF (ofCrAnOpF φ1)) (ofCrAnOpF φ2))) a) = 0 All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOp⊢ ∀ (b : 𝓕.WickAlgebra), b * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * b 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.WickAlgebra⊢ a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * a 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah0:ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) - ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a = 0⊢ ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah0:ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) - ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a = 0⊢ ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a + 0𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah0:ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) - ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a = 0⊢ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a + 0 = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah0:ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) - ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a = 0⊢ ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a + 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrah0:ι a * ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) - ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a = 0⊢ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a + 0 = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι a All goals completed! 🐙

The kernel of ι

𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebra⊢ ⟦x⟧ = 0 ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebra⊢ ⟦x⟧ = ⟦0⟧ ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOphdiff:¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φ'hx':(superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') ∈ 𝓕.fieldOpIdealSeth:(superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') ∈ statisticSubmodule fermionic⊢ ↑⟨(superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ'), h⟩ ∈ 𝓕.fieldOpIdealSet All goals completed! 🐙TODO "The lemma `bosonicProjF_mem_ideal` has a proof which is really long. We should either 1) split it up into smaller lemmas or 2) Put more comments into the proof."𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetb:𝓕.FieldOpFreeAlgebrahb:b ∈ Set.univd:𝓕.FieldOpFreeAlgebrahd:d ∈ Set.univy:𝓕.FieldOpFreeAlgebrahy:y ∈ 𝓕.fieldOpIdealSetha:d * y ∈ Set.univ * 𝓕.fieldOpIdealSethx:d * y * b ∈ Set.univ * 𝓕.fieldOpIdealSet * Set.univkey:∀ {u w v : 𝓕.FieldOpFreeAlgebra}, v ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet → u * v * w ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethBy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethFy:↑(fermionicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF d) * ↑(bosonicProjF y) * ↑(bosonicProjF b) + ↑(fermionicProjF d) * ↑(fermionicProjF y) * ↑(bosonicProjF b) + (↑(bosonicProjF d) * ↑(fermionicProjF y) * ↑(fermionicProjF b) + ↑(fermionicProjF d) * ↑(bosonicProjF y) * ↑(fermionicProjF b)) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet All goals completed! 🐙 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ p 0 ⋯ 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ (ringConGen fun a b => a - b ∈ 𝓕.fieldOpIdealSet) 0 0 All goals completed! 🐙 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)) (hy : y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)), p x hx → p y hy → p (x + y) ⋯ 𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:p x hxhpy:p y hy⊢ p (x + y) ⋯ 𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethpy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF x) + ↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethpy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethpy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet 𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethpy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet All goals completed! 🐙 𝓕:FieldSpecificationx✝:𝓕.FieldOpFreeAlgebrahx✝:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hpx:↑(bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSethpy:↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ↑(bosonicProjF y) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet All goals completed! 🐙 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)), p x hx → p (-x) ⋯ 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ↑(bosonicProjF a) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSetx_1:𝓕.FieldOpFreeAlgebrahx_1:x_1 ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)a:p x_1 hx_1⊢ p (-x_1) ⋯ All goals completed! 🐙𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahx:ι (↑(bosonicProjF x) + ↑(fermionicProjF x)) = 0hb:ι ↑(bosonicProjF x) = 0⊢ ι ↑(fermionicProjF x) = 0 𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrahb:ι ↑(bosonicProjF x) = 0hx:ι ↑(bosonicProjF x) + ι ↑(fermionicProjF x) = 0⊢ ι ↑(fermionicProjF x) = 0 All goals completed! 🐙𝓕:FieldSpecificationx:𝓕.FieldOpFreeAlgebrah:ι ↑(bosonicProjF x) = 0 ∧ ι ↑(fermionicProjF x) = 0⊢ ι (↑(bosonicProjF x) + ↑(fermionicProjF x)) = 0 All goals completed! 🐙

Constructors

For a field specification 𝓕 and an element φ of 𝓕.FieldOp, ofFieldOp φ is defined as the element of 𝓕.WickAlgebra given by ι (ofFieldOpF φ).

def ofFieldOp (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra := ι (ofFieldOpF φ)
lemma ofFieldOp_eq_ι_ofFieldOpF (φ : 𝓕.FieldOp) : ofFieldOp φ = ι (ofFieldOpF φ) := rfl

For a field specification 𝓕 and a list φs of 𝓕.FieldOp, ofFieldOpList φs is defined as the element of 𝓕.WickAlgebra given by ι (ofFieldOpListF φ).

def ofFieldOpList (φs : List 𝓕.FieldOp) : 𝓕.WickAlgebra := ι (ofFieldOpListF φs)
lemma ofFieldOpList_eq_ι_ofFieldOpListF (φs : List 𝓕.FieldOp) : ofFieldOpList φs = ι (ofFieldOpListF φs) := rfl𝓕:FieldSpecificationφs:List 𝓕.FieldOpψs:List 𝓕.FieldOp⊢ ι (ofFieldOpListF φs * ofFieldOpListF ψs) = ι (ofFieldOpListF φs) * ι (ofFieldOpListF ψs) All goals completed! 🐙lemma ofFieldOpList_cons (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ofFieldOpList (φ :: φs) = ofFieldOp φ * ofFieldOpList φs := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ofFieldOpList (φ :: φs) = ofFieldOp φ * ofFieldOpList φs All goals completed! 🐙lemma ofFieldOpList_singleton (φ : 𝓕.FieldOp) : ofFieldOpList [φ] = ofFieldOp φ := 𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ ofFieldOpList [φ] = ofFieldOp φ All goals completed! 🐙

For a field specification 𝓕 and an element φ of 𝓕.CrAnFieldOp, ofCrAnOp φ is defined as the element of 𝓕.WickAlgebra given by ι (ofCrAnOpF φ).

def ofCrAnOp (φ : 𝓕.CrAnFieldOp) : 𝓕.WickAlgebra := ι (ofCrAnOpF φ)
lemma ofCrAnOp_eq_ι_ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : ofCrAnOp φ = ι (ofCrAnOpF φ) := rfl𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ ι (∑ i, ofCrAnOpF ⟨φ, i⟩) = ∑ i, ofCrAnOp ⟨φ, i⟩ All goals completed! 🐙

For a field specification 𝓕 and a list φs of 𝓕.CrAnFieldOp, ofCrAnList φs is defined as the element of 𝓕.WickAlgebra given by ι (ofCrAnListF φ).

def ofCrAnList (φs : List 𝓕.CrAnFieldOp) : 𝓕.WickAlgebra := ι (ofCrAnListF φs)
lemma ofCrAnList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) : ofCrAnList φs = ι (ofCrAnListF φs) := rfllemma ofCrAnList_nil : ofCrAnList (𝓕 := 𝓕) [] = 1 := 𝓕:FieldSpecification⊢ ofCrAnList [] = 1 𝓕:FieldSpecification⊢ ι 1 = 1 All goals completed! 🐙lemma ofCrAnList_append (φs ψs : List 𝓕.CrAnFieldOp) : ofCrAnList (φs ++ ψs) = ofCrAnList φs * ofCrAnList ψs := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (φs ++ ψs) = ofCrAnList φs * ofCrAnList ψs 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOp⊢ ι (ofCrAnListF φs * ofCrAnListF ψs) = ι (ofCrAnListF φs) * ι (ofCrAnListF ψs) All goals completed! 🐙lemma ofCrAnList_singleton (φ : 𝓕.CrAnFieldOp) : ofCrAnList [φ] = ofCrAnOp φ := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOp⊢ ofCrAnList [φ] = ofCrAnOp φ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ι (∑ s, ofCrAnListF ↑s) = ∑ s, ofCrAnList ↑s All goals completed! 🐙

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the annihilation part of 𝓕.FieldOp as an element of 𝓕.WickAlgebra. Thus for φ

    an incoming asymptotic state this is 0.

    a position based state this is ofCrAnOp ⟨φ, .create⟩.

    an outgoing asymptotic state this is ofCrAnOp ⟨φ, ()⟩.

def anPart (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra := ι (anPartF φ)
lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl@[simp] lemma anPart_inAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) : anPart (FieldOp.inAsymp φ) = 0 := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ anPart (FieldOp.inAsymp φ) = 0 All goals completed! 🐙@[simp] lemma anPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) : anPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ anPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ All goals completed! 🐙@[simp] lemma anPart_outAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) : anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩ All goals completed! 🐙

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the creation part of 𝓕.FieldOp as an element of 𝓕.WickAlgebra. Thus for φ

    an incoming asymptotic state this is ofCrAnOp ⟨φ, ()⟩.

    a position based state this is ofCrAnOp ⟨φ, .create⟩.

    an outgoing asymptotic state this is 0.

def crPart (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra := ι (crPartF φ)
lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl@[simp] lemma crPart_inAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) : crPart (FieldOp.inAsymp φ) = ofCrAnOp ⟨FieldOp.inAsymp φ, ()⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ crPart (FieldOp.inAsymp φ) = ofCrAnOp ⟨FieldOp.inAsymp φ, ()⟩ All goals completed! 🐙@[simp] lemma crPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) : crPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ crPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ All goals completed! 🐙@[simp] lemma crPart_outAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) : crPart (FieldOp.outAsymp φ) = 0 := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ crPart (FieldOp.outAsymp φ) = 0 All goals completed! 🐙

For field specification 𝓕, and an element φ of 𝓕.FieldOp the following relation holds:

ofFieldOp φ = crPart φ + anPart φ

That is, every field operator splits into its creation part plus its annihilation part.

𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ ι (crPartF φ + anPartF φ) = ι (crPartF φ) + ι (anPartF φ) All goals completed! 🐙
𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ anPart (FieldOp.outAsymp φ) = crPart (FieldOp.outAsymp φ) + anPart (FieldOp.outAsymp φ) All goals completed! 🐙𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ crPart (FieldOp.inAsymp φ) = crPart (FieldOp.inAsymp φ) + anPart (FieldOp.inAsymp φ) All goals completed! 🐙