Time Ordering on Field operator algebra

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF {𝓕 : FieldSpecification} {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (φs1 φs2 : List 𝓕.CrAnFieldOp) (h : crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2) : ι (FieldOpFreeAlgebra.timeOrderF (FieldOpFreeAlgebra.ofCrAnListF φs1 * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ2)) (FieldOpFreeAlgebra.ofCrAnOpF φ3)) * FieldOpFreeAlgebra.ofCrAnListF φs2)) = 0

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF {𝓕 : FieldSpecification} {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (φs1 φs2 : List 𝓕.CrAnFieldOp) : ι (FieldOpFreeAlgebra.timeOrderF (FieldOpFreeAlgebra.ofCrAnListF φs1 * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ2)) (FieldOpFreeAlgebra.ofCrAnOpF φ3)) * FieldOpFreeAlgebra.ofCrAnListF φs2)) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_superCommuteF_superCommuteF {𝓕 : FieldSpecification} {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (a b : 𝓕.FieldOpFreeAlgebra) : ι (FieldOpFreeAlgebra.timeOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ2)) (FieldOpFreeAlgebra.ofCrAnOpF φ3)) * b)) = 0

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_superCommuteF_eq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.FieldOpFreeAlgebra) : ι (FieldOpFreeAlgebra.timeOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ) * b)) = ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ) * FieldOpFreeAlgebra.timeOrderF (a * b))

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_superCommuteF_neq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (hφψ : ¬(crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) (a b : 𝓕.FieldOpFreeAlgebra) : ι (FieldOpFreeAlgebra.timeOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ) * b)) = 0

Defining time order for FiedOpAlgebra.

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_zero_of_mem_ideal {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι (FieldOpFreeAlgebra.timeOrderF a) = 0

theorem FieldSpecification.FieldOpAlgebra.ι_timeOrderF_eq_of_equiv {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) : ι (FieldOpFreeAlgebra.timeOrderF a) = ι (FieldOpFreeAlgebra.timeOrderF b)

noncomputable def FieldSpecification.FieldOpAlgebra.timeOrder {𝓕 : FieldSpecification} : 𝓕.FieldOpAlgebra →ₗ[ℂ] 𝓕.FieldOpAlgebra

For a field specification 𝓕, timeOrder is the linear map

FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕

defined as the descent of ι ∘ₗ timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 from FieldOpFreeAlgebra 𝓕 to FieldOpAlgebra 𝓕. This descent exists because ι ∘ₗ timeOrderF is well-defined on equivalence classes.

The notation 𝓣(a) is used for timeOrder a.

Equations

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

def FieldSpecification.FieldOpAlgebra.«term𝓣(_)» : Lean.ParserDescr

For a field specification 𝓕, timeOrder is the linear map

FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕

defined as the descent of ι ∘ₗ timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 from FieldOpFreeAlgebra 𝓕 to FieldOpAlgebra 𝓕. This descent exists because ι ∘ₗ timeOrderF is well-defined on equivalence classes.

The notation 𝓣(a) is used for timeOrder a.

Equations

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

Properties of time ordering

theorem FieldSpecification.FieldOpAlgebra.timeOrder_eq_ι_timeOrderF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : timeOrder (ι a) = ι (FieldOpFreeAlgebra.timeOrderF a)

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOp_ofFieldOp_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) : timeOrder (ofFieldOp φ * ofFieldOp ψ) = ofFieldOp φ * ofFieldOp ψ

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : ¬timeOrderRel φ ψ) : timeOrder (ofFieldOp φ * ofFieldOp ψ) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • ofFieldOp ψ * ofFieldOp φ

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h : ¬timeOrderRel φ ψ) : timeOrder (ofFieldOp φ * ofFieldOp ψ) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ)

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOpList_nil {𝓕 : FieldSpecification} : timeOrder (ofFieldOpList []) = 1

@[simp]

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOpList_singleton {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : timeOrder (ofFieldOpList [φ]) = ofFieldOpList [φ]

theorem FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : timeOrder (ofFieldOpList (φ :: φs)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (maxTimeField φ φs))) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get (Finset.filter (fun (x : Fin (eraseMaxTimeField φ φs).length) => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)) • ofFieldOp (maxTimeField φ φs) * timeOrder (ofFieldOpList (eraseMaxTimeField φ φs))

For a field specification 𝓕, the time order operator acting on a list of 𝓕.FieldOp, 𝓣(φ₀…φₙ), is equal to 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) where φᵢ is the maximal time field operator in φ₀…φₙ.

The proof of this result ultimately relies on basic properties of ordering and signs.

theorem FieldSpecification.FieldOpAlgebra.timeOrder_superCommute_eq_time_mid {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) : timeOrder (a * (superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * b) = (superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * timeOrder (a * b)

theorem FieldSpecification.FieldOpAlgebra.timeOrder_superCommute_eq_time_left {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) : timeOrder ((superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * b) = (superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * timeOrder b

theorem FieldSpecification.FieldOpAlgebra.timeOrder_superCommute_neq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (hφψ : ¬(crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) : timeOrder ((superCommute (ofCrAnOp φ)) (ofCrAnOp ψ)) = 0

theorem FieldSpecification.FieldOpAlgebra.timeOrder_superCommute_anPart_ofFieldOp_neq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (hφψ : ¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) : timeOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0

theorem FieldSpecification.FieldOpAlgebra.timeOrder_timeOrder_mid {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpAlgebra) : timeOrder (a * b * c) = timeOrder (a * timeOrder b * c)

For a field specification 𝓕, and a, b, c in 𝓕.FieldOpAlgebra, then 𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c).

theorem FieldSpecification.FieldOpAlgebra.timeOrder_timeOrder_left {𝓕 : FieldSpecification} (b c : 𝓕.FieldOpAlgebra) : timeOrder (b * c) = timeOrder (timeOrder b * c)

theorem FieldSpecification.FieldOpAlgebra.timeOrder_timeOrder_right {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpAlgebra) : timeOrder (a * b) = timeOrder (a * timeOrder b)

theorem FieldSpecification.FieldOpAlgebra.timeOrder_timeOrder {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : timeOrder (timeOrder a) = timeOrder a

Time ordering is a projection.