Creation and annihilation sections

In the module PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic we defined states for a field specification, and in the module PhysLean.QFT.PerturbationTheory.FieldStatistics.CrAnFieldOp we defined a refinement of states called CrAnFieldOp which distinguishes between the creation and annihilation components of states. There exists, in particular, a map from CrAnFieldOp to FieldOp called crAnFieldOpToFieldOp.

Given a list of FieldOp, φs, in this module we define a section of φs to be a list of CrAnFieldOp, ψs, such that under the map crAnFieldOpToFieldOp, ψs is mapped to φs. That is to say, the states underlying ψs are the states in φs. We denote these sections as CrAnSection φs.

Looking forward the main consequence of this definition is the lemma FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_sum.

In this module we define various properties of CrAnSection.

def FieldSpecification.CrAnSection {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : Type

The sections in 𝓕.CrAnFieldOp over a list φs : List 𝓕.FieldOp. In terms of physics, given some fields φ₁...φₙ, the different ways one can associate each field as a creation or an annilation operator. E.g. the number of terms φ₁⁰φ₂¹...φₙ⁰ φ₁¹φ₂¹...φₙ⁰ etc. If some fields are exclusively creation or annihilation operators at this point (e.g. asymptotic states) this is accounted for.

Equations

• FieldSpecification.CrAnSection φs = { ψs : List 𝓕.CrAnFieldOp // List.map 𝓕.crAnFieldOpToFieldOp ψs = φs }

@[simp]

theorem FieldSpecification.CrAnSection.length_eq {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : (↑ψs).length = φs.length

def FieldSpecification.CrAnSection.tail {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : CrAnSection φs.tail

The tail of a section for φs.

Equations

• FieldSpecification.CrAnSection.tail ⟨[], h⟩ = ⟨[], h⟩
• FieldSpecification.CrAnSection.tail ⟨[], h⟩ = ⋯.elim
• FieldSpecification.CrAnSection.tail ⟨ψ :: ψs, h⟩ = ⟨ψs, ⋯⟩

theorem FieldSpecification.CrAnSection.head_state_eq {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} (ψs : CrAnSection (φ :: φs)) : ((↑ψs).head ⋯).fst = φ

theorem FieldSpecification.CrAnSection.statistics_eq_state_statistics {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) : FieldStatistic.ofList 𝓕.crAnStatistics ↑ψs = FieldStatistic.ofList 𝓕.fieldOpStatistic φs

theorem FieldSpecification.CrAnSection.take_statistics_eq_take_state_statistics {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (ψs : CrAnSection φs) (n : ℕ) : FieldStatistic.ofList 𝓕.crAnStatistics (List.take n ↑ψs) = FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take n φs)

def FieldSpecification.CrAnSection.head {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} (ψs : CrAnSection (φ :: φs)) : 𝓕.fieldOpToCrAnType φ

The head of a section for φ :: φs as an element in 𝓕.fieldOpToCreateAnnihilateType φ.

Equations

• FieldSpecification.CrAnSection.head ⟨[], h⟩ = ⋯.elim
• FieldSpecification.CrAnSection.head ⟨ψ :: ψs, h⟩ = (𝓕.fieldOpToCreateAnnihilateTypeCongr ⋯) ψ.snd

theorem FieldSpecification.CrAnSection.eq_head_cons_tail {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} {ψs : CrAnSection (φ :: φs)} : ↑ψs = ⟨φ, ψs.head⟩ :: ↑ψs.tail

def FieldSpecification.CrAnSection.cons {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} (ψ : 𝓕.fieldOpToCrAnType φ) (ψs : CrAnSection φs) : CrAnSection (φ :: φs)

The creation of a section from for φ : φs from a section for φs and a element of 𝓕.fieldOpToCreateAnnihilateType φ.

Equations

• FieldSpecification.CrAnSection.cons ψ ψs = ⟨⟨φ, ψ⟩ :: ↑ψs, ⋯⟩

def FieldSpecification.CrAnSection.nilEquiv {𝓕 : FieldSpecification} : CrAnSection [] ≃ Unit

For the empty list of states there is only one CrAnSection. Corresponding to the empty list of CrAnFieldOp.

Equations

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

def FieldSpecification.CrAnSection.singletonEquiv {𝓕 : FieldSpecification} {φ : 𝓕.FieldOp} : CrAnSection [φ] ≃ 𝓕.fieldOpToCrAnType φ

The creation and annihilation sections for a singleton list is given by a choice of 𝓕.fieldOpToCreateAnnihilateType φ. If φ is a asymptotic state there is no choice here, else there are two choices.

Equations

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

def FieldSpecification.CrAnSection.consEquiv {𝓕 : FieldSpecification} {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} : CrAnSection (φ :: φs) ≃ 𝓕.fieldOpToCrAnType φ × CrAnSection φs

An equivalence separating the head of a creation and annihilation section from the tail.

Equations

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

instance FieldSpecification.CrAnSection.fintype {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : Fintype (CrAnSection φs)

The instance of a finite type on CrAnSections defined recursively through consEquiv.

Equations

• FieldSpecification.CrAnSection.fintype [] = Fintype.ofEquiv Unit FieldSpecification.CrAnSection.nilEquiv.symm
• FieldSpecification.CrAnSection.fintype (head :: φs) = Fintype.ofEquiv (𝓕.fieldOpToCrAnType head × FieldSpecification.CrAnSection φs) FieldSpecification.CrAnSection.consEquiv.symm

@[simp]

theorem FieldSpecification.CrAnSection.card_nil_eq {𝓕 : FieldSpecification} : Fintype.card (CrAnSection []) = 1

theorem FieldSpecification.CrAnSection.card_cons_eq {𝓕 : FieldSpecification} {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} : Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.fieldOpToCrAnType φ) * Fintype.card (CrAnSection φs)

theorem FieldSpecification.CrAnSection.card_eq_mul {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : Fintype.card (CrAnSection φs) = 2 ^ List.countP 𝓕.statesIsPosition φs

theorem FieldSpecification.CrAnSection.card_perm_eq {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs.Perm φs') : Fintype.card (CrAnSection φs) = Fintype.card (CrAnSection φs')

@[simp]

theorem FieldSpecification.CrAnSection.sum_nil {𝓕 : FieldSpecification} {M : Type u_1} (f : CrAnSection [] → M) [AddCommMonoid M] : ∑ s : CrAnSection [], f s = f ⟨[], ⋯⟩

theorem FieldSpecification.CrAnSection.sum_cons {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} {M : Type u_1} (f : CrAnSection (φ :: φs) → M) [AddCommMonoid M] : ∑ s : CrAnSection (φ :: φs), f s = ∑ a : 𝓕.fieldOpToCrAnType φ, ∑ s : CrAnSection φs, f (cons a s)

theorem FieldSpecification.CrAnSection.sum_over_length {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {M : Type u_1} {s : CrAnSection φs} (f : Fin (↑s).length → M) [AddCommMonoid M] : ∑ n : Fin (↑s).length, f n = ∑ n : Fin φs.length, f (Fin.cast ⋯ n)

def FieldSpecification.CrAnSection.congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') : CrAnSection φs ≃ CrAnSection φs'

The equivalence between CrAnSection φs and CrAnSection φs' induced by an equality φs = φs'.

Equations

• FieldSpecification.CrAnSection.congr ⋯ = Equiv.refl (FieldSpecification.CrAnSection x✝)

@[simp]

theorem FieldSpecification.CrAnSection.congr_fst {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (ψs : CrAnSection φs) : ↑((congr h) ψs) = ↑ψs

@[simp]

theorem FieldSpecification.CrAnSection.congr_symm {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') : (congr h).symm = congr ⋯

@[simp]

theorem FieldSpecification.CrAnSection.congr_trans_apply {𝓕 : FieldSpecification} {φs φs' φs'' : List 𝓕.FieldOp} (h1 : φs = φs') (h2 : φs' = φs'') (ψs : CrAnSection φs) : (congr h2) ((congr h1) ψs) = (congr ⋯) ψs

def FieldSpecification.CrAnSection.take {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (List.take n φs)

Returns the first n elements of a section and its underlying list.

Equations

• FieldSpecification.CrAnSection.take n ψs = ⟨List.take n ↑ψs, ⋯⟩

@[simp]

theorem FieldSpecification.CrAnSection.take_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ) (ψs : CrAnSection φs) : take n ((congr h) ψs) = (congr ⋯) (take n ψs)

def FieldSpecification.CrAnSection.drop {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (List.drop n φs)

Removes the first n elements of a section and its underlying list.

Equations

• FieldSpecification.CrAnSection.drop n ψs = ⟨List.drop n ↑ψs, ⋯⟩

@[simp]

theorem FieldSpecification.CrAnSection.drop_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (n : ℕ) (ψs : CrAnSection φs) : drop n ((congr h) ψs) = (congr ⋯) (drop n ψs)

def FieldSpecification.CrAnSection.append {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs) (ψs' : CrAnSection φs') : CrAnSection (φs ++ φs')

Appends two sections and their underlying lists.

Equations

• ψs.append ψs' = ⟨↑ψs ++ ↑ψs', ⋯⟩

theorem FieldSpecification.CrAnSection.append_assoc {𝓕 : FieldSpecification} {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs) (ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') : ψs.append (ψs'.append ψs'') = (congr ⋯) ((ψs.append ψs').append ψs'')

theorem FieldSpecification.CrAnSection.append_assoc' {𝓕 : FieldSpecification} {φs φs' φs'' : List 𝓕.FieldOp} (ψs : CrAnSection φs) (ψs' : CrAnSection φs') (ψs'' : CrAnSection φs'') : (ψs.append ψs').append ψs'' = (congr ⋯) (ψs.append (ψs'.append ψs''))

theorem FieldSpecification.CrAnSection.singletonEquiv_append_eq_cons {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φ : 𝓕.FieldOp} (ψs : CrAnSection φs) (ψ : 𝓕.fieldOpToCrAnType φ) : (singletonEquiv.symm ψ).append ψs = cons ψ ψs

@[simp]

theorem FieldSpecification.CrAnSection.take_append_drop {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {n : ℕ} (ψs : CrAnSection φs) : (take n ψs).append (drop n ψs) = (congr ⋯) ψs

theorem FieldSpecification.CrAnSection.congr_append {𝓕 : FieldSpecification} {φs1 φs1' φs2 φs2' : List 𝓕.FieldOp} (h1 : φs1 = φs1') (h2 : φs2 = φs2') (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) : ((congr h1) ψs1).append ((congr h2) ψs2) = (congr ⋯) (ψs1.append ψs2)

@[simp]

theorem FieldSpecification.CrAnSection.congr_fst_append {𝓕 : FieldSpecification} {φs1 φs1' φs2 : List 𝓕.FieldOp} (h1 : φs1 = φs1') (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) : ((congr h1) ψs1).append ψs2 = (congr ⋯) (ψs1.append ψs2)

@[simp]

theorem FieldSpecification.CrAnSection.congr_snd_append {𝓕 : FieldSpecification} {φs1 φs2 φs2' : List 𝓕.FieldOp} (h2 : φs2 = φs2') (ψs1 : CrAnSection φs1) (ψs2 : CrAnSection φs2) : ψs1.append ((congr h2) ψs2) = (congr ⋯) (ψs1.append ψs2)

@[simp]

theorem FieldSpecification.CrAnSection.take_left {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs) (ψs' : CrAnSection φs') : take φs.length (ψs.append ψs') = (congr ⋯) ψs

@[simp]

theorem FieldSpecification.CrAnSection.drop_left {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (ψs : CrAnSection φs) (ψs' : CrAnSection φs') : drop φs.length (ψs.append ψs') = (congr ⋯) ψs'

def FieldSpecification.CrAnSection.appendEquiv {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} : CrAnSection (φs ++ φs') ≃ CrAnSection φs × CrAnSection φs'

The equivalence between CrAnSection (φs ++ φs') and CrAnSection φs × CrAnSection φs formed by append, take and drop and their interrelationship.

Equations

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

@[simp]

theorem List.map_eraseIdx {α β : Type} (f : α → β) (l : List α) (n : ℕ) : map f (l.eraseIdx n) = (map f l).eraseIdx n

def FieldSpecification.CrAnSection.eraseIdx {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (n : ℕ) (ψs : CrAnSection φs) : CrAnSection (φs.eraseIdx n)

Erasing an element from a section and it's underlying list.

Equations

• FieldSpecification.CrAnSection.eraseIdx n ψs = ⟨(↑ψs).eraseIdx n, ⋯⟩

def FieldSpecification.CrAnSection.eraseIdxEquiv {𝓕 : FieldSpecification} (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length) : CrAnSection φs ≃ 𝓕.fieldOpToCrAnType φs[n] × CrAnSection (φs.eraseIdx n)

The equivalence formed by extracting an element from a section.

Equations

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

@[simp]

theorem FieldSpecification.CrAnSection.eraseIdxEquiv_apply_snd {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {n : ℕ} (ψs : CrAnSection φs) (hn : n < φs.length) : ((eraseIdxEquiv n φs hn) ψs).2 = eraseIdx n ψs

theorem FieldSpecification.CrAnSection.eraseIdxEquiv_symm_eq_take_cons_drop {𝓕 : FieldSpecification} {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length) (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) : (eraseIdxEquiv n φs hn).symm (a, s) = (congr ⋯) ((take n s).append (cons a (drop n s)))

@[simp]

theorem FieldSpecification.CrAnSection.eraseIdxEquiv_symm_getElem {𝓕 : FieldSpecification} {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length) (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) : (↑((eraseIdxEquiv n φs hn).symm (a, s)))[n] = ⟨φs[n], a⟩

@[simp]

theorem FieldSpecification.CrAnSection.eraseIdxEquiv_symm_eraseIdx {𝓕 : FieldSpecification} {n : ℕ} (φs : List 𝓕.FieldOp) (hn : n < φs.length) (a : 𝓕.fieldOpToCrAnType φs[n]) (s : CrAnSection (φs.eraseIdx n)) : (↑((eraseIdxEquiv n φs hn).symm (a, s))).eraseIdx n = ↑s

theorem FieldSpecification.CrAnSection.sum_eraseIdxEquiv {𝓕 : FieldSpecification} {M : Type u_1} (n : ℕ) (φs : List 𝓕.FieldOp) (hn : n < φs.length) (f : CrAnSection φs → M) [AddCommMonoid M] : ∑ s : CrAnSection φs, f s = ∑ a : 𝓕.fieldOpToCrAnType φs[n], ∑ s : CrAnSection (φs.eraseIdx n), f ((eraseIdxEquiv n φs hn).symm (a, s))