Super Commute

The super commutator on the FieldOpFreeAlgebra.

noncomputable def FieldSpecification.FieldOpFreeAlgebra.superCommuteF {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra

For a field specification 𝓕, the super commutator superCommuteF is defined as the linear map 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra which on the lists φs and φs' of 𝓕.CrAnFieldOp gives

superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs.

The notation [a, b]ₛF can be used for superCommuteF a b.

Equations

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

def FieldSpecification.FieldOpFreeAlgebra.«term[_,_]ₛF» : Lean.ParserDescr

For a field specification 𝓕, the super commutator superCommuteF is defined as the linear map 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra which on the lists φs and φs' of 𝓕.CrAnFieldOp gives

superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs.

The notation [a, b]ₛF can be used for superCommuteF a b.

Equations

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

The super commutator of different types of elements

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = ofCrAnListF (φs ++ φs') - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnListF (φs' ++ φs)

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') = ofCrAnOpF φ * ofCrAnOpF φ' - (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') • ofCrAnOpF φ' * ofCrAnOpF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList {𝓕 : FieldSpecification} (φcas : List 𝓕.CrAnFieldOp) (φs : List 𝓕.FieldOp) : (superCommuteF (ofCrAnListF φcas)) (ofFieldOpListF φs) = ofCrAnListF φcas * ofFieldOpListF φs - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φcas)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpListF φs * ofCrAnListF φcas

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList {𝓕 : FieldSpecification} (φ φs : List 𝓕.FieldOp) : (superCommuteF (ofFieldOpListF φ)) (ofFieldOpListF φs) = ofFieldOpListF φ * ofFieldOpListF φs - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpListF φs * ofFieldOpListF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommuteF (ofFieldOpF φ)) (ofFieldOpListF φs) = ofFieldOpF φ * ofFieldOpListF φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpListF φs * ofFieldOpF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) : (superCommuteF (ofFieldOpListF φs)) (ofFieldOpF φ) = ofFieldOpListF φs * ofFieldOpF φ - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (𝓕.fieldOpStatistic φ) • ofFieldOpF φ * ofFieldOpListF φs

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (anPartF φ)) (crPartF φ') = anPartF φ * crPartF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPartF φ' * anPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (crPartF φ)) (anPartF φ') = crPartF φ * anPartF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPartF φ' * crPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (crPartF φ)) (crPartF φ') = crPartF φ * crPartF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPartF φ' * crPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (anPartF φ)) (anPartF φ') = anPartF φ * anPartF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPartF φ' * anPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommuteF (crPartF φ)) (ofFieldOpListF φs) = crPartF φ * ofFieldOpListF φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpListF φs * crPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommuteF (anPartF φ)) (ofFieldOpListF φs) = anPartF φ * ofFieldOpListF φs - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • ofFieldOpListF φs * anPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (crPartF φ)) (ofFieldOpF φ') = crPartF φ * ofFieldOpF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • ofFieldOpF φ' * crPartF φ

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : (superCommuteF (anPartF φ)) (ofFieldOpF φ') = anPartF φ * ofFieldOpF φ' - (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • ofFieldOpF φ' * anPartF φ

Mul equal superCommuteF

Lemmas which rewrite a multiplication of two elements of the algebra as their commuted multiplication with a sign plus the super commutator.

theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : ofCrAnListF φs * ofCrAnListF φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnListF φs' * ofCrAnListF φs + (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.CrAnFieldOp) : ofCrAnOpF φ * ofCrAnListF φs' = (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • ofCrAnListF φs' * ofCrAnOpF φ + (superCommuteF (ofCrAnOpF φ)) (ofCrAnListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (φs φs' : List 𝓕.FieldOp) : ofFieldOpListF φs * ofFieldOpListF φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpListF φs' * ofFieldOpListF φs + (superCommuteF (ofFieldOpListF φs)) (ofFieldOpListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs' : List 𝓕.FieldOp) : ofFieldOpF φ * ofFieldOpListF φs' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpListF φs' * ofFieldOpF φ + (superCommuteF (ofFieldOpF φ)) (ofFieldOpListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) : ofFieldOpListF φs * ofFieldOpF φ = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.fieldOpStatistic φs)) (𝓕.fieldOpStatistic φ) • ofFieldOpF φ * ofFieldOpListF φs + (superCommuteF (ofFieldOpListF φs)) (ofFieldOpF φ)

theorem FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_anPartF_eq_superCommuteF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : crPartF φ * anPartF φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPartF φ' * crPartF φ + (superCommuteF (crPartF φ)) (anPartF φ')

theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : anPartF φ * crPartF φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPartF φ' * anPartF φ + (superCommuteF (anPartF φ)) (crPartF φ')

theorem FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_crPartF_eq_superCommuteF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : crPartF φ * crPartF φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPartF φ' * crPartF φ + (superCommuteF (crPartF φ)) (crPartF φ')

theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_anPartF_eq_superCommuteF {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : anPartF φ * anPartF φ' = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • anPartF φ' * anPartF φ + (superCommuteF (anPartF φ)) (anPartF φ')

theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : ofCrAnListF φs * ofFieldOpListF φs' = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • ofFieldOpListF φs' * ofCrAnListF φs + (superCommuteF (ofCrAnListF φs)) (ofFieldOpListF φs')

Symmetry of the super commutator.

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = -(FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics φs') • (superCommuteF (ofCrAnListF φs')) (ofCrAnListF φs)

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') = -(FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') • (superCommuteF (ofCrAnOpF φ')) (ofCrAnOpF φ)

Splitting the super commutator on lists into sums.

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF (φ :: φs')) = (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF φ) * ofCrAnListF φs' + (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ) • ofCrAnOpF φ * (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : (superCommuteF (ofCrAnListF φs)) (ofFieldOpListF (φ :: φs')) = (superCommuteF (ofCrAnListF φs)) (ofFieldOpF φ) * ofFieldOpListF φs' + (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (𝓕.fieldOpStatistic φ) • ofFieldOpF φ * (superCommuteF (ofCrAnListF φs)) (ofFieldOpListF φs')

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑n) φs')) • ofCrAnListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF (φs'.get n)) * ofCrAnListF (List.drop (↑n + 1) φs')

For a field specification 𝓕, and two lists φs = φ₀…φₙ and φs' of 𝓕.CrAnFieldOp the following super commutation relation holds:

[φs', φ₀…φₙ]ₛF = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛF * φᵢ₊₁ … φₙ

The proof of this relation is via induction on the length of φs.

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : (superCommuteF (ofCrAnListF φs)) (ofFieldOpListF φs') = ∑ n : Fin φs'.length, (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) • ofFieldOpListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF (φs'.get n)) * ofFieldOpListF (List.drop (↑n + 1) φs')

theorem FieldSpecification.FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF {𝓕 : FieldSpecification} (φs1 φs2 φs3 : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs1)) ((superCommuteF (ofCrAnListF φs2)) (ofCrAnListF φs3)) = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs1)) (FieldStatistic.ofList 𝓕.crAnStatistics φs3) • (-(FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs2)) (FieldStatistic.ofList 𝓕.crAnStatistics φs3) • (superCommuteF (ofCrAnListF φs3)) ((superCommuteF (ofCrAnListF φs1)) (ofCrAnListF φs2)) - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics φs1)) (FieldStatistic.ofList 𝓕.crAnStatistics φs2) • (superCommuteF (ofCrAnListF φs2)) ((superCommuteF (ofCrAnListF φs3)) (ofCrAnListF φs1)))

Interaction with grading.

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_grade {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} {f1 f2 : FieldStatistic} (ha : a ∈ statisticSubmodule f1) (hb : b ∈ statisticSubmodule f2) : (superCommuteF a) b ∈ statisticSubmodule (f1 + f2)

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_bosonic_bosonic {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.bosonic) (hb : b ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = a * b - b * a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_bosonic_fermionic {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.bosonic) (hb : b ∈ statisticSubmodule FieldStatistic.fermionic) : (superCommuteF a) b = a * b - b * a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_bonsonic {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.fermionic) (hb : b ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = a * b - b * a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_bonsonic {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (hb : b ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = a * b - b * a

theorem FieldSpecification.FieldOpFreeAlgebra.bosonic_superCommuteF {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = a * b - b * a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_bonsonic_symm {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (hb : b ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = -(superCommuteF b) a

theorem FieldSpecification.FieldOpFreeAlgebra.bonsonic_superCommuteF_symm {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) b = -(superCommuteF b) a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_fermionic {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.fermionic) (hb : b ∈ statisticSubmodule FieldStatistic.fermionic) : (superCommuteF a) b = a * b + b * a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_fermionic_symm {𝓕 : FieldSpecification} {a b : 𝓕.FieldOpFreeAlgebra} (ha : a ∈ statisticSubmodule FieldStatistic.fermionic) (hb : b ∈ statisticSubmodule FieldStatistic.fermionic) : (superCommuteF a) b = (superCommuteF b) a

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_expand_bosonicProjF_fermionicProjF {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) : (superCommuteF a) b = ↑(bosonicProjF a) * ↑(bosonicProjF b) - ↑(bosonicProjF b) * ↑(bosonicProjF a) + ↑(bosonicProjF a) * ↑(fermionicProjF b) - ↑(fermionicProjF b) * ↑(bosonicProjF a) + ↑(fermionicProjF a) * ↑(bosonicProjF b) - ↑(bosonicProjF b) * ↑(fermionicProjF a) + ↑(fermionicProjF a) * ↑(fermionicProjF b) + ↑(fermionicProjF b) * ↑(fermionicProjF a)

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') ∈ statisticSubmodule FieldStatistic.bosonic ∨ (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') ∈ statisticSubmodule FieldStatistic.fermionic

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic {𝓕 : FieldSpecification} (φ φ' : 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') ∈ statisticSubmodule FieldStatistic.bosonic ∨ (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF φ') ∈ statisticSubmodule FieldStatistic.fermionic

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic {𝓕 : FieldSpecification} (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) : (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) ∈ statisticSubmodule FieldStatistic.bosonic ∨ (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) ∈ statisticSubmodule FieldStatistic.fermionic

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_bosonic_ofCrAnListF_eq_sum {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (φs : List 𝓕.CrAnFieldOp) (ha : a ∈ statisticSubmodule FieldStatistic.bosonic) : (superCommuteF a) (ofCrAnListF φs) = ∑ n : Fin φs.length, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (↑n + 1) φs)

theorem FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_ofCrAnListF_eq_sum {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (φs : List 𝓕.CrAnFieldOp) (ha : a ∈ statisticSubmodule FieldStatistic.fermionic) : (superCommuteF a) (ofCrAnListF φs) = ∑ n : Fin φs.length, (FieldStatistic.exchangeSign FieldStatistic.fermionic) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑n) φs)) • ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (↑n + 1) φs)

theorem FieldSpecification.FieldOpFreeAlgebra.statistic_neq_of_superCommuteF_fermionic {𝓕 : FieldSpecification} {φs φs' : List 𝓕.CrAnFieldOp} (h : (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') ∈ statisticSubmodule FieldStatistic.fermionic) : FieldStatistic.ofList 𝓕.crAnStatistics φs ≠ FieldStatistic.ofList 𝓕.crAnStatistics φs' ∨ (superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = 0