Exchange sign for field statistics

Suppose we have two fields φ and ψ, and the term φψ, if we swap them ψφ, we may pick up a sign. This sign is called the exchange sign. This sign is -1 if both fields ψ and φ are fermionic and 1 otherwise.

In this module we define the exchange sign for general field statistics, and prove some properties of it. Importantly:

• It is symmetric exchangeSign_symm.
• When multiplied with itself it is 1 exchangeSign_mul_self.
• It is a cocycle exchangeSign_cocycle.

def FieldStatistic.exchangeSign : FieldStatistic →* FieldStatistic →* ℂ

The exchange sign, exchangeSign, is defined as the group homomorphism

FieldStatistic →* FieldStatistic →* ℂ,

for which exchangeSign a b is -1 if both a and b are fermionic and 1 otherwise. The exchange sign is the sign one picks up on exchanging an operator or field φ₁ of statistic a with an operator or field φ₂ of statistic b, i.e. φ₁φ₂ → φ₂φ₁.

The notation 𝓢(a, b) is used for the exchange sign of a and b.

Equations

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

def FieldStatistic.«term𝓢(_,_)» : Lean.ParserDescr

The exchange sign, exchangeSign, is defined as the group homomorphism

FieldStatistic →* FieldStatistic →* ℂ,

for which exchangeSign a b is -1 if both a and b are fermionic and 1 otherwise. The exchange sign is the sign one picks up on exchanging an operator or field φ₁ of statistic a with an operator or field φ₂ of statistic b, i.e. φ₁φ₂ → φ₂φ₁.

The notation 𝓢(a, b) is used for the exchange sign of a and b.

Equations

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

theorem FieldStatistic.exchangeSign_symm (a b : FieldStatistic) : (exchangeSign a) b = (exchangeSign b) a

The exchange sign is symmetric.

@[simp]

theorem FieldStatistic.exchangeSign_bosonic (a : FieldStatistic) : (exchangeSign a) bosonic = 1

@[simp]

theorem FieldStatistic.bosonic_exchangeSign (a : FieldStatistic) : (exchangeSign bosonic) a = 1

@[simp]

theorem FieldStatistic.fermionic_exchangeSign_fermionic : (exchangeSign fermionic) fermionic = -1

theorem FieldStatistic.exchangeSign_eq_if (a b : FieldStatistic) : (exchangeSign a) b = if a = fermionic ∧ b = fermionic then -1 else 1

@[simp]

theorem FieldStatistic.exchangeSign_mul_self (a b : FieldStatistic) : (exchangeSign a) b * (exchangeSign a) b = 1

@[simp]

theorem FieldStatistic.exchangeSign_mul_self_swap (a b : FieldStatistic) : (exchangeSign a) b * (exchangeSign b) a = 1

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

theorem FieldStatistic.exchangeSign_cocycle (a b c : FieldStatistic) : (exchangeSign a) (b * c) * (exchangeSign b) c = (exchangeSign a) b * (exchangeSign (a * b)) c

The exchange sign is a cocycle.