Physlib.QFT.PerturbationTheory.FieldStatistics.ExchangeSign

Imports

/-
Copyright (c) 2024 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 Physlib.QFT.PerturbationTheory.FieldStatistics.Basic
public import Mathlib.Analysis.Complex.Basic

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.

@[expose] public section

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.

def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
  toFun a :=
    {
      toFun := fun b =>
        match a, b with
        | bosonic, _ => 1
        | _, bosonic => 1
        | fermionic, fermionic => -1
      map_one' := by𝓕:Typea:FieldStatistic⊢ (match a, 1 with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  1
        fin_cases a«0»𝓕:Type⊢ (match bosonic, 1 with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  1«1»𝓕:Type⊢ (match fermionic, 1 with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  1
        <;>«0»𝓕:Type⊢ (match bosonic, 1 with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  1«1»𝓕:Type⊢ (match fermionic, 1 with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  1 simpAll goals completed! 🐙
      map_mul' := fun c b => by𝓕:Typea:FieldStatisticc:FieldStatisticb:FieldStatistic⊢ (match a, c * b with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match a, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match a, b with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1
        fin_cases a«0»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ (match bosonic, c * b with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, b with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ (match fermionic, c * b with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, b with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1 <;>«0»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ (match bosonic, c * b with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, b with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ (match fermionic, c * b with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, b with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1
          fin_cases b«1».«0»𝓕:Typec:FieldStatistic⊢ (match fermionic, c * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«1»𝓕:Typec:FieldStatistic⊢ (match fermionic, c * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1 <;>«0».«0»𝓕:Typec:FieldStatistic⊢ (match bosonic, c * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«0».«1»𝓕:Typec:FieldStatistic⊢ (match bosonic, c * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«0»𝓕:Typec:FieldStatistic⊢ (match fermionic, c * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«1»𝓕:Typec:FieldStatistic⊢ (match fermionic, c * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, c with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1
          fin_cases c«1».«1».«0»𝓕:Type⊢ (match fermionic, bosonic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«1».«1»𝓕:Type⊢ (match fermionic, fermionic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1 <;>«0».«0».«0»𝓕:Type⊢ (match bosonic, bosonic * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«0».«0».«1»𝓕:Type⊢ (match bosonic, fermionic * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«0».«1».«0»𝓕:Type⊢ (match bosonic, bosonic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«0».«1».«1»𝓕:Type⊢ (match bosonic, fermionic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match bosonic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match bosonic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«0».«0»𝓕:Type⊢ (match fermionic, bosonic * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«0».«1»𝓕:Type⊢ (match fermionic, fermionic * bosonic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«1».«0»𝓕:Type⊢ (match fermionic, bosonic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, bosonic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1«1».«1».«1»𝓕:Type⊢ (match fermionic, fermionic * fermionic with
  | bosonic, x => 1
  | x, bosonic => 1
  | fermionic, fermionic => -1) =
  (match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1) *
    match fermionic, fermionic with
    | bosonic, x => 1
    | x, bosonic => 1
    | fermionic, fermionic => -1
          simpAll goals completed! 🐙
    }
  map_one' := by𝓕:Type⊢ {
    toFun := fun b =>
      match 1, b with
      | bosonic, x => 1
      | x, bosonic => 1
      | fermionic, fermionic => -1,
    map_one' := ⋯, map_mul' := ⋯ } =
  1
    ext b𝓕:Typeb:FieldStatistic⊢ {
      toFun := fun b =>
        match 1, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    b =
  1 b
    fin_cases b«0»𝓕:Type⊢ {
      toFun := fun b =>
        match 1, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  1 bosonic«1»𝓕:Type⊢ {
      toFun := fun b =>
        match 1, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  1 fermionic
    <;>«0»𝓕:Type⊢ {
      toFun := fun b =>
        match 1, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  1 bosonic«1»𝓕:Type⊢ {
      toFun := fun b =>
        match 1, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  1 fermionic simpAll goals completed! 🐙
  map_mul' c b := by𝓕:Typec:FieldStatisticb:FieldStatistic⊢ {
    toFun := fun b_1 =>
      match c * b, b_1 with
      | bosonic, x => 1
      | x, bosonic => 1
      | fermionic, fermionic => -1,
    map_one' := ⋯, map_mul' := ⋯ } =
  {
      toFun := fun b =>
        match c, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ } *
    {
      toFun := fun b_1 =>
        match b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    ext a𝓕:Typec:FieldStatisticb:FieldStatistica:FieldStatistic⊢ {
      toFun := fun b_1 =>
        match c * b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    a =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b_1 =>
          match b, b_1 with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    a
    fin_cases a«0»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ {
      toFun := fun b_1 =>
        match c * b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b_1 =>
          match b, b_1 with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«1»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ {
      toFun := fun b_1 =>
        match c * b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b_1 =>
          match b, b_1 with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic
    <;>«0»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ {
      toFun := fun b_1 =>
        match c * b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b_1 =>
          match b, b_1 with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«1»𝓕:Typec:FieldStatisticb:FieldStatistic⊢ {
      toFun := fun b_1 =>
        match c * b, b_1 with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b_1 =>
          match b, b_1 with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic fin_cases b«1».«0»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«1»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic <;>«0».«0»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«0».«1»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«1».«0»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«1»𝓕:Typec:FieldStatistic⊢ {
      toFun := fun b =>
        match c * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match c, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic fin_cases c«1».«1».«0»𝓕:Type⊢ {
      toFun := fun b =>
        match bosonic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«1».«1»𝓕:Type⊢ {
      toFun := fun b =>
        match fermionic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic
    <;>«0».«0».«0»𝓕:Type⊢ {
      toFun := fun b =>
        match bosonic * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«0».«0».«1»𝓕:Type⊢ {
      toFun := fun b =>
        match fermionic * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«0».«1».«0»𝓕:Type⊢ {
      toFun := fun b =>
        match bosonic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«0».«1».«1»𝓕:Type⊢ {
      toFun := fun b =>
        match fermionic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    bosonic =
  ({
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    bosonic«1».«0».«0»𝓕:Type⊢ {
      toFun := fun b =>
        match bosonic * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«0».«1»𝓕:Type⊢ {
      toFun := fun b =>
        match fermionic * bosonic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«1».«0»𝓕:Type⊢ {
      toFun := fun b =>
        match bosonic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match bosonic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic«1».«1».«1»𝓕:Type⊢ {
      toFun := fun b =>
        match fermionic * fermionic, b with
        | bosonic, x => 1
        | x, bosonic => 1
        | fermionic, fermionic => -1,
      map_one' := ⋯, map_mul' := ⋯ }
    fermionic =
  ({
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ } *
      {
        toFun := fun b =>
          match fermionic, b with
          | bosonic, x => 1
          | x, bosonic => 1
          | fermionic, fermionic => -1,
        map_one' := ⋯, map_mul' := ⋯ })
    fermionic simpAll goals completed! 🐙

@[inherit_doc exchangeSign]
scoped[FieldStatistic] notation "𝓢(" a "," b ")" => exchangeSign a b

The exchange sign is symmetric.

lemma exchangeSign_symm (a b : FieldStatistic) : 𝓢(a, b) = 𝓢(b, a) := bya:FieldStatisticb:FieldStatistic⊢ (exchangeSign a) b = (exchangeSign b) a
  fin_cases a«0»b:FieldStatistic⊢ (exchangeSign bosonic) b = (exchangeSign b) bosonic«1»b:FieldStatistic⊢ (exchangeSign fermionic) b = (exchangeSign b) fermionic <;>«0»b:FieldStatistic⊢ (exchangeSign bosonic) b = (exchangeSign b) bosonic«1»b:FieldStatistic⊢ (exchangeSign fermionic) b = (exchangeSign b) fermionic fin_cases b«1».«0»⊢ (exchangeSign fermionic) bosonic = (exchangeSign bosonic) fermionic«1».«1»⊢ (exchangeSign fermionic) fermionic = (exchangeSign fermionic) fermionic <;>«0».«0»⊢ (exchangeSign bosonic) bosonic = (exchangeSign bosonic) bosonic«0».«1»⊢ (exchangeSign bosonic) fermionic = (exchangeSign fermionic) bosonic«1».«0»⊢ (exchangeSign fermionic) bosonic = (exchangeSign bosonic) fermionic«1».«1»⊢ (exchangeSign fermionic) fermionic = (exchangeSign fermionic) fermionic rflAll goals completed! 🐙

              @[simp]
lemma exchangeSign_bosonic (a : FieldStatistic) : 𝓢(a, bosonic) = 1 := bya:FieldStatistic⊢ (exchangeSign a) bosonic = 1
  fin_cases a«0»⊢ (exchangeSign bosonic) bosonic = 1«1»⊢ (exchangeSign fermionic) bosonic = 1 <;>«0»⊢ (exchangeSign bosonic) bosonic = 1«1»⊢ (exchangeSign fermionic) bosonic = 1 rflAll goals completed! 🐙

@[simp]
lemma bosonic_exchangeSign (a : FieldStatistic) : 𝓢(bosonic, a) = 1 := bya:FieldStatistic⊢ (exchangeSign bosonic) a = 1
  rw [exchangeSign_symm,a:FieldStatistic⊢ (exchangeSign a) bosonic = 1All goals completed! 🐙 exchangeSign_bosonica:FieldStatistic⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙@[simp]
lemma fermionic_exchangeSign_fermionic : 𝓢(fermionic, fermionic) = - 1 := by⊢ (exchangeSign fermionic) fermionic = -1
  rflAll goals completed! 🐙lemma exchangeSign_eq_if (a b : FieldStatistic) :
    𝓢(a, b) = if a = fermionic ∧ b = fermionic then - 1 else 1 := bya:FieldStatisticb:FieldStatistic⊢ (exchangeSign a) b = if a = fermionic ∧ b = fermionic then -1 else 1
  fin_cases a«0»b:FieldStatistic⊢ (exchangeSign bosonic) b = if bosonic = fermionic ∧ b = fermionic then -1 else 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b = if fermionic = fermionic ∧ b = fermionic then -1 else 1 <;>«0»b:FieldStatistic⊢ (exchangeSign bosonic) b = if bosonic = fermionic ∧ b = fermionic then -1 else 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b = if fermionic = fermionic ∧ b = fermionic then -1 else 1 fin_cases b«1».«0»⊢ (exchangeSign fermionic) bosonic = if fermionic = fermionic ∧ bosonic = fermionic then -1 else 1«1».«1»⊢ (exchangeSign fermionic) fermionic = if fermionic = fermionic ∧ fermionic = fermionic then -1 else 1 <;>«0».«0»⊢ (exchangeSign bosonic) bosonic = if bosonic = fermionic ∧ bosonic = fermionic then -1 else 1«0».«1»⊢ (exchangeSign bosonic) fermionic = if bosonic = fermionic ∧ fermionic = fermionic then -1 else 1«1».«0»⊢ (exchangeSign fermionic) bosonic = if fermionic = fermionic ∧ bosonic = fermionic then -1 else 1«1».«1»⊢ (exchangeSign fermionic) fermionic = if fermionic = fermionic ∧ fermionic = fermionic then -1 else 1 rflAll goals completed! 🐙@[simp]
lemma exchangeSign_mul_self (a b : FieldStatistic) : 𝓢(a, b) * 𝓢(a, b) = 1 := bya:FieldStatisticb:FieldStatistic⊢ (exchangeSign a) b * (exchangeSign a) b = 1
  fin_cases a«0»b:FieldStatistic⊢ (exchangeSign bosonic) b * (exchangeSign bosonic) b = 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b * (exchangeSign fermionic) b = 1 <;>«0»b:FieldStatistic⊢ (exchangeSign bosonic) b * (exchangeSign bosonic) b = 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b * (exchangeSign fermionic) b = 1 fin_cases b«1».«0»⊢ (exchangeSign fermionic) bosonic * (exchangeSign fermionic) bosonic = 1«1».«1»⊢ (exchangeSign fermionic) fermionic * (exchangeSign fermionic) fermionic = 1 <;>«0».«0»⊢ (exchangeSign bosonic) bosonic * (exchangeSign bosonic) bosonic = 1«0».«1»⊢ (exchangeSign bosonic) fermionic * (exchangeSign bosonic) fermionic = 1«1».«0»⊢ (exchangeSign fermionic) bosonic * (exchangeSign fermionic) bosonic = 1«1».«1»⊢ (exchangeSign fermionic) fermionic * (exchangeSign fermionic) fermionic = 1 simp [exchangeSign]All goals completed! 🐙@[simp]
lemma exchangeSign_mul_self_swap (a b : FieldStatistic) : 𝓢(a, b) * 𝓢(b, a) = 1 := bya:FieldStatisticb:FieldStatistic⊢ (exchangeSign a) b * (exchangeSign b) a = 1
  fin_cases a«0»b:FieldStatistic⊢ (exchangeSign bosonic) b * (exchangeSign b) bosonic = 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b * (exchangeSign b) fermionic = 1 <;>«0»b:FieldStatistic⊢ (exchangeSign bosonic) b * (exchangeSign b) bosonic = 1«1»b:FieldStatistic⊢ (exchangeSign fermionic) b * (exchangeSign b) fermionic = 1 fin_cases b«1».«0»⊢ (exchangeSign fermionic) bosonic * (exchangeSign bosonic) fermionic = 1«1».«1»⊢ (exchangeSign fermionic) fermionic * (exchangeSign fermionic) fermionic = 1 <;>«0».«0»⊢ (exchangeSign bosonic) bosonic * (exchangeSign bosonic) bosonic = 1«0».«1»⊢ (exchangeSign bosonic) fermionic * (exchangeSign fermionic) bosonic = 1«1».«0»⊢ (exchangeSign fermionic) bosonic * (exchangeSign bosonic) fermionic = 1«1».«1»⊢ (exchangeSign fermionic) fermionic * (exchangeSign fermionic) fermionic = 1 simp [exchangeSign]All goals completed! 🐙

lemma exchangeSign_ofList_cons (a : FieldStatistic)
    (s : 𝓕 → FieldStatistic) (φ : 𝓕) (φs : List 𝓕) :
    𝓢(a, ofList s (φ :: φs)) = 𝓢(a, s φ) * 𝓢(a, ofList s φs) := by𝓕:Typea:FieldStatistics:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (exchangeSign a) (ofList s (φ :: φs)) = (exchangeSign a) (s φ) * (exchangeSign a) (ofList s φs)
  rw [ofList_cons_eq_mul,𝓕:Typea:FieldStatistics:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (exchangeSign a) (s φ * ofList s φs) = (exchangeSign a) (s φ) * (exchangeSign a) (ofList s φs)All goals completed! 🐙 map_mul𝓕:Typea:FieldStatistics:𝓕 → FieldStatisticφ:𝓕φs:List 𝓕⊢ (exchangeSign a) (s φ) * (exchangeSign a) (ofList s φs) = (exchangeSign a) (s φ) * (exchangeSign a) (ofList s φs)All goals completed! 🐙]All goals completed! 🐙

The exchange sign is a cocycle.

lemma exchangeSign_cocycle (a b c : FieldStatistic) :
    𝓢(a, b * c) * 𝓢(b, c) = 𝓢(a, b) * 𝓢(a * b, c) := bya:FieldStatisticb:FieldStatisticc:FieldStatistic⊢ (exchangeSign a) (b * c) * (exchangeSign b) c = (exchangeSign a) b * (exchangeSign (a * b)) c
  fin_cases a«0»b:FieldStatisticc:FieldStatistic⊢ (exchangeSign bosonic) (b * c) * (exchangeSign b) c = (exchangeSign bosonic) b * (exchangeSign (bosonic * b)) c«1»b:FieldStatisticc:FieldStatistic⊢ (exchangeSign fermionic) (b * c) * (exchangeSign b) c = (exchangeSign fermionic) b * (exchangeSign (fermionic * b)) c <;>«0»b:FieldStatisticc:FieldStatistic⊢ (exchangeSign bosonic) (b * c) * (exchangeSign b) c = (exchangeSign bosonic) b * (exchangeSign (bosonic * b)) c«1»b:FieldStatisticc:FieldStatistic⊢ (exchangeSign fermionic) (b * c) * (exchangeSign b) c = (exchangeSign fermionic) b * (exchangeSign (fermionic * b)) c fin_cases b«1».«0»c:FieldStatistic⊢ (exchangeSign fermionic) (bosonic * c) * (exchangeSign bosonic) c =
  (exchangeSign fermionic) bosonic * (exchangeSign (fermionic * bosonic)) c«1».«1»c:FieldStatistic⊢ (exchangeSign fermionic) (fermionic * c) * (exchangeSign fermionic) c =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) c <;>«0».«0»c:FieldStatistic⊢ (exchangeSign bosonic) (bosonic * c) * (exchangeSign bosonic) c =
  (exchangeSign bosonic) bosonic * (exchangeSign (bosonic * bosonic)) c«0».«1»c:FieldStatistic⊢ (exchangeSign bosonic) (fermionic * c) * (exchangeSign fermionic) c =
  (exchangeSign bosonic) fermionic * (exchangeSign (bosonic * fermionic)) c«1».«0»c:FieldStatistic⊢ (exchangeSign fermionic) (bosonic * c) * (exchangeSign bosonic) c =
  (exchangeSign fermionic) bosonic * (exchangeSign (fermionic * bosonic)) c«1».«1»c:FieldStatistic⊢ (exchangeSign fermionic) (fermionic * c) * (exchangeSign fermionic) c =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) c fin_cases c«1».«1».«0»⊢ (exchangeSign fermionic) (fermionic * bosonic) * (exchangeSign fermionic) bosonic =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) bosonic«1».«1».«1»⊢ (exchangeSign fermionic) (fermionic * fermionic) * (exchangeSign fermionic) fermionic =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) fermionic <;>«0».«0».«0»⊢ (exchangeSign bosonic) (bosonic * bosonic) * (exchangeSign bosonic) bosonic =
  (exchangeSign bosonic) bosonic * (exchangeSign (bosonic * bosonic)) bosonic«0».«0».«1»⊢ (exchangeSign bosonic) (bosonic * fermionic) * (exchangeSign bosonic) fermionic =
  (exchangeSign bosonic) bosonic * (exchangeSign (bosonic * bosonic)) fermionic«0».«1».«0»⊢ (exchangeSign bosonic) (fermionic * bosonic) * (exchangeSign fermionic) bosonic =
  (exchangeSign bosonic) fermionic * (exchangeSign (bosonic * fermionic)) bosonic«0».«1».«1»⊢ (exchangeSign bosonic) (fermionic * fermionic) * (exchangeSign fermionic) fermionic =
  (exchangeSign bosonic) fermionic * (exchangeSign (bosonic * fermionic)) fermionic«1».«0».«0»⊢ (exchangeSign fermionic) (bosonic * bosonic) * (exchangeSign bosonic) bosonic =
  (exchangeSign fermionic) bosonic * (exchangeSign (fermionic * bosonic)) bosonic«1».«0».«1»⊢ (exchangeSign fermionic) (bosonic * fermionic) * (exchangeSign bosonic) fermionic =
  (exchangeSign fermionic) bosonic * (exchangeSign (fermionic * bosonic)) fermionic«1».«1».«0»⊢ (exchangeSign fermionic) (fermionic * bosonic) * (exchangeSign fermionic) bosonic =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) bosonic«1».«1».«1»⊢ (exchangeSign fermionic) (fermionic * fermionic) * (exchangeSign fermionic) fermionic =
  (exchangeSign fermionic) fermionic * (exchangeSign (fermionic * fermionic)) fermionic simpAll goals completed! 🐙