Creation and annihilation parts of fields

inductive CreateAnnihilate : Type

The type CreateAnnihilate is the type containing two elements create and annihilate. This type is used to specify if an operator is a creation, or annihilation, operator or the sum thereof or integral thereof etc.

• create : CreateAnnihilate
• annihilate : CreateAnnihilate

instance instInhabitedCreateAnnihilate : Inhabited CreateAnnihilate

Equations

• instInhabitedCreateAnnihilate = { default := instInhabitedCreateAnnihilate.default }

def instInhabitedCreateAnnihilate.default : CreateAnnihilate

Equations

• instInhabitedCreateAnnihilate.default = CreateAnnihilate.create

def instBEqCreateAnnihilate.beq : CreateAnnihilate → CreateAnnihilate → Bool

Equations

• instBEqCreateAnnihilate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqCreateAnnihilate : BEq CreateAnnihilate

Equations

• instBEqCreateAnnihilate = { beq := instBEqCreateAnnihilate.beq }

instance instDecidableEqCreateAnnihilate : DecidableEq CreateAnnihilate

Equations

• instDecidableEqCreateAnnihilate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CreateAnnihilate.instFintype : Fintype CreateAnnihilate

The type CreateAnnihilate is finite.

Equations

• CreateAnnihilate.instFintype = { elems := {CreateAnnihilate.create, CreateAnnihilate.annihilate}, complete := CreateAnnihilate.instFintype._proof_1 }

theorem CreateAnnihilate.eq_create_or_annihilate (φ : CreateAnnihilate) : φ = create ∨ φ = annihilate

def CreateAnnihilate.normalOrder : CreateAnnihilate → CreateAnnihilate → Prop

The normal ordering on creation and annihilation operators. Under this relation, normalOrder a b is false only if a is annihilate and b is create.

Equations

• CreateAnnihilate.create.normalOrder x✝ = True
• CreateAnnihilate.annihilate.normalOrder CreateAnnihilate.annihilate = True
• CreateAnnihilate.annihilate.normalOrder CreateAnnihilate.create = False

instance CreateAnnihilate.instDecidableNormalOrder (φ φ' : CreateAnnihilate) : Decidable (φ.normalOrder φ')

The normal ordering on CreateAnnihilate is decidable.

Equations

• CreateAnnihilate.create.instDecidableNormalOrder CreateAnnihilate.create = isTrue True.intro
• CreateAnnihilate.annihilate.instDecidableNormalOrder CreateAnnihilate.annihilate = isTrue True.intro
• CreateAnnihilate.create.instDecidableNormalOrder CreateAnnihilate.annihilate = isTrue True.intro
• CreateAnnihilate.annihilate.instDecidableNormalOrder CreateAnnihilate.create = isFalse ⋯

instance CreateAnnihilate.instIsTotalNormalOrder : IsTotal CreateAnnihilate normalOrder

Normal ordering is total.

instance CreateAnnihilate.instIsTransNormalOrder : IsTrans CreateAnnihilate normalOrder

Normal ordering is transitive.

@[simp]

theorem CreateAnnihilate.not_normalOrder_annihilate_iff_false (a : CreateAnnihilate) : ¬a.normalOrder annihilate ↔ False

theorem CreateAnnihilate.sum_eq {M : Type} [AddCommMonoid M] (f : CreateAnnihilate → M) : ∑ i : CreateAnnihilate, f i = f create + f annihilate

@[simp]

theorem CreateAnnihilate.CreateAnnihilate_card_eq_two : Fintype.card CreateAnnihilate = 2