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 Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Data.Fintype.CardCreation and annihilation parts of fields
@[expose] public section
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.
inductive CreateAnnihilate where
| create : CreateAnnihilate
| annihilate : CreateAnnihilate
deriving Inhabited, BEq, DecidableEq
The type CreateAnnihilate is finite.
instance : Fintype CreateAnnihilate where
elems := {create, annihilate}
complete := ⊢ ∀ (x : CreateAnnihilate), x ∈ {create, annihilate}
c:CreateAnnihilate⊢ c ∈ {create, annihilate}
⊢ create ∈ {create, annihilate}⊢ annihilate ∈ {create, annihilate}
⊢ create ∈ {create, annihilate} All goals completed! 🐙
⊢ annihilate ∈ {create, annihilate} All goals completed! 🐙lemma eq_create_or_annihilate (φ : CreateAnnihilate) : φ = create ∨ φ = annihilate := φ:CreateAnnihilate⊢ φ = create ∨ φ = annihilate
⊢ create = create ∨ create = annihilate⊢ annihilate = create ∨ annihilate = annihilate ⊢ create = create ∨ create = annihilate⊢ annihilate = create ∨ annihilate = annihilate All goals completed! 🐙
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.
def normalOrder : CreateAnnihilate → CreateAnnihilate → Prop
| create, _ => True
| annihilate, annihilate => True
| annihilate, create => False
The normal ordering on CreateAnnihilate is decidable.
instance : (φ φ' : CreateAnnihilate) → Decidable (normalOrder φ φ')
| create, create => isTrue True.intro
| annihilate, annihilate => isTrue True.intro
| create, annihilate => isTrue True.intro
| annihilate, create => isFalse False.elimNormal ordering is total.
instance : Std.Total normalOrder where
total := ⊢ ∀ (a b : CreateAnnihilate), a.normalOrder b ∨ b.normalOrder a All goals completed! 🐙Normal ordering is transitive.
instance : IsTrans CreateAnnihilate normalOrder where
trans := ⊢ ∀ (a b c : CreateAnnihilate), a.normalOrder b → b.normalOrder c → a.normalOrder c All goals completed! 🐙@[simp]
lemma not_normalOrder_annihilate_iff_false (a : CreateAnnihilate) :
(¬ normalOrder a annihilate) ↔ False := a:CreateAnnihilate⊢ ¬a.normalOrder annihilate ↔ False
⊢ ¬create.normalOrder annihilate ↔ False⊢ ¬annihilate.normalOrder annihilate ↔ False ⊢ ¬create.normalOrder annihilate ↔ False⊢ ¬annihilate.normalOrder annihilate ↔ False All goals completed! 🐙lemma sum_eq {M : Type} [AddCommMonoid M] (f : CreateAnnihilate → M) :
∑ i, f i = f create + f annihilate := M:Typeinst✝:AddCommMonoid Mf:CreateAnnihilate → M⊢ ∑ i, f i = f create + f annihilate
M:Typeinst✝:AddCommMonoid Mf:CreateAnnihilate → M⊢ ∑ i ∈ {create, annihilate}, f i = f create + f annihilate
All goals completed! 🐙@[simp]
lemma CreateAnnihilate_card_eq_two : Fintype.card CreateAnnihilate = 2 := rfl