Field statistics

Basic properties related to whether a field, or list of fields, is bosonic or fermionic.

inductive FieldStatistic : Type

The type FieldStatistic is the type containing two elements bosonic and fermionic. This type is used to specify if a field or operator obeys bosonic or fermionic statistics.

• bosonic : FieldStatistic
• fermionic : FieldStatistic

instance instDecidableEqFieldStatistic : DecidableEq FieldStatistic

Equations

• instDecidableEqFieldStatistic x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance FieldStatistic.instCommGroup : CommGroup FieldStatistic

The type FieldStatistic carries an instance of a commutative group in which

• bosonic * bosonic = bosonic
• bosonic * fermionic = fermionic
• fermionic * bosonic = fermionic
• fermionic * fermionic = bosonic

This group is isomorphic to ℤ₂.

Equations

• FieldStatistic.instCommGroup = CommGroup.mk FieldStatistic.instCommGroup.proof_11

@[simp]

theorem FieldStatistic.bosonic_mul_bosonic : bosonic * bosonic = bosonic

@[simp]

theorem FieldStatistic.bosonic_mul_fermionic : bosonic * fermionic = fermionic

@[simp]

theorem FieldStatistic.fermionic_mul_bosonic : fermionic * bosonic = fermionic

@[simp]

theorem FieldStatistic.fermionic_mul_fermionic : fermionic * fermionic = bosonic

@[simp]

theorem FieldStatistic.mul_bosonic (a : FieldStatistic) : a * bosonic = a

@[simp]

theorem FieldStatistic.mul_self (a : FieldStatistic) : a * a = 1

instance FieldStatistic.instFintype : Fintype FieldStatistic

Field statics form a finite type.

Equations

• FieldStatistic.instFintype = { elems := {FieldStatistic.bosonic, FieldStatistic.fermionic}, complete := FieldStatistic.instFintype.proof_1 }

@[simp]

theorem FieldStatistic.fermionic_not_eq_bonsic : ¬fermionic = bosonic

theorem FieldStatistic.bonsic_eq_fermionic_false : bosonic = fermionic ↔ false = true

@[simp]

theorem FieldStatistic.neq_fermionic_iff_eq_bosonic (a : FieldStatistic) : ¬a = fermionic ↔ a = bosonic

@[simp]

theorem FieldStatistic.neq_bosonic_iff_eq_fermionic (a : FieldStatistic) : ¬a = bosonic ↔ a = fermionic

@[simp]

theorem FieldStatistic.bosonic_neq_iff_fermionic_eq (a : FieldStatistic) : ¬bosonic = a ↔ fermionic = a

@[simp]

theorem FieldStatistic.fermionic_neq_iff_bosonic_eq (a : FieldStatistic) : ¬fermionic = a ↔ bosonic = a

theorem FieldStatistic.eq_self_if_eq_bosonic {a : FieldStatistic} : (if a = bosonic then bosonic else fermionic) = a

theorem FieldStatistic.eq_self_if_bosonic_eq {a : FieldStatistic} : (if bosonic = a then bosonic else fermionic) = a

theorem FieldStatistic.mul_eq_one_iff (a b : FieldStatistic) : a * b = 1 ↔ a = b

theorem FieldStatistic.one_eq_mul_iff (a b : FieldStatistic) : 1 = a * b ↔ a = b

theorem FieldStatistic.mul_eq_iff_eq_mul (a b c : FieldStatistic) : a * b = c ↔ a = b * c

theorem FieldStatistic.mul_eq_iff_eq_mul' (a b c : FieldStatistic) : a * b = c ↔ b = a * c

def FieldStatistic.ofList {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φs : List 𝓕) : FieldStatistic

The field statistics of a list of fields is fermionic if there is an odd number of fermions, otherwise it is bosonic.

Equations

• FieldStatistic.ofList s [] = FieldStatistic.bosonic
• FieldStatistic.ofList s (φ :: φs) = if s φ = FieldStatistic.ofList s φs then FieldStatistic.bosonic else FieldStatistic.fermionic

theorem FieldStatistic.ofList_cons_eq_mul {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φ : 𝓕) (φs : List 𝓕) : ofList s (φ :: φs) = s φ * ofList s φs

theorem FieldStatistic.ofList_eq_prod {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φs : List 𝓕) : ofList s φs = (List.map s φs).prod

@[simp]

theorem FieldStatistic.ofList_singleton {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s [φ] = s φ

@[simp]

theorem FieldStatistic.ofList_freeMonoid {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φ : 𝓕) : ofList s (FreeMonoid.of φ) = s φ

@[simp]

theorem FieldStatistic.ofList_empty {𝓕 : Type} (s : 𝓕 → FieldStatistic) : ofList s [] = bosonic

@[simp]

theorem FieldStatistic.ofList_append {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φs φs' : List 𝓕) : ofList s (φs ++ φs') = if ofList s φs = ofList s φs' then bosonic else fermionic

theorem FieldStatistic.ofList_append_eq_mul {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φs φs' : List 𝓕) : ofList s (φs ++ φs') = ofList s φs * ofList s φs'

theorem FieldStatistic.ofList_perm {𝓕 : Type} (s : 𝓕 → FieldStatistic) {l l' : List 𝓕} (h : l.Perm l') : ofList s l = ofList s l'

theorem FieldStatistic.ofList_orderedInsert {𝓕 : Type} (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1] (φs : List 𝓕) (φ : 𝓕) : ofList s (List.orderedInsert le1 φ φs) = ofList s (φ :: φs)

@[simp]

theorem FieldStatistic.ofList_insertionSort {𝓕 : Type} (s : 𝓕 → FieldStatistic) (le1 : 𝓕 → 𝓕 → Prop) [DecidableRel le1] (φs : List 𝓕) : ofList s (List.insertionSort le1 φs) = ofList s φs

@[irreducible]

theorem FieldStatistic.ofList_map_eq_finset_prod {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φs : List 𝓕) (l : List (Fin φs.length)) (hl : l.Nodup) : ofList s (List.map φs.get l) = ∏ i : Fin φs.length, if i ∈ l then s φs[i] else 1

theorem FieldStatistic.ofList_pair {𝓕 : Type} (s : 𝓕 → FieldStatistic) (φ1 φ2 : 𝓕) : ofList s [φ1, φ2] = s φ1 * s φ2

ofList and take

theorem FieldStatistic.ofList_take_insert {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n : ℕ) (φ : 𝓕) (φs : List 𝓕) : ofList q (List.take n φs) = ofList q (List.take n (List.insertIdx n φ φs))

theorem FieldStatistic.ofList_take_eraseIdx {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n : ℕ) (φs : List 𝓕) : ofList q (List.take n (φs.eraseIdx n)) = ofList q (List.take n φs)

theorem FieldStatistic.ofList_take_zero {𝓕 : Type} (q : 𝓕 → FieldStatistic) (φs : List 𝓕) : ofList q (List.take 0 φs) = 1

theorem FieldStatistic.ofList_take_succ_cons {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n : ℕ) (φ1 : 𝓕) (φs : List 𝓕) : ofList q (List.take (n + 1) (φ1 :: φs)) = q φ1 * ofList q (List.take n φs)

theorem FieldStatistic.ofList_take_insertIdx_gt {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : n < m) : ofList q (List.take n (List.insertIdx m φ1 φs)) = ofList q (List.take n φs)

theorem FieldStatistic.ofList_insert_lt_eq {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : m ≤ n) (hm : m ≤ φs.length) : ofList q (List.take (n + 1) (List.insertIdx m φ1 φs)) = ofList q (List.take (n + 1) (φ1 :: φs))

theorem FieldStatistic.ofList_take_insertIdx_le {𝓕 : Type} (q : 𝓕 → FieldStatistic) (n m : ℕ) (φ1 : 𝓕) (φs : List 𝓕) (hn : m ≤ n) (hm : m ≤ φs.length) : ofList q (List.take (n + 1) (List.insertIdx m φ1 φs)) = q φ1 * ofList q (List.take n φs)

instance FieldStatistic.instAddMonoid : AddMonoid FieldStatistic

The instance of an additive monoid on FieldStatistic.

Equations

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

@[simp]

theorem FieldStatistic.add_eq_mul (a b : FieldStatistic) : a + b = a * b