Grading on the FieldOpFreeAlgebra

def FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule {𝓕 : FieldSpecification} (f : FieldStatistic) : Submodule ℂ 𝓕.FieldOpFreeAlgebra

The submodule of FieldOpFreeAlgebra spanned by lists of field statistic f.

theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mem_statisticSubmodule_of {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic) (h : FieldStatistic.ofList 𝓕.crAnStatistics φs = f) : ofCrAnListF φs ∈ statisticSubmodule f

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

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

def FieldSpecification.FieldOpFreeAlgebra.bosonicProjF {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statisticSubmodule FieldStatistic.bosonic)

The projection of an element of FieldOpFreeAlgebra onto it's bosonic part.

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_ofCrAnListF {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : bosonicProjF (ofCrAnListF φs) = if h : FieldStatistic.ofList 𝓕.crAnStatistics φs = FieldStatistic.bosonic then ⟨ofCrAnListF φs, ⋯⟩ else 0

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.bosonic) : bosonicProjF a = ⟨a, h⟩

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.fermionic) : bosonicProjF a = 0

@[simp]

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_bonosic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : bosonicProjF ↑(a FieldStatistic.bosonic) = a FieldStatistic.bosonic

@[simp]

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : bosonicProjF ↑(a FieldStatistic.fermionic) = 0

def FieldSpecification.FieldOpFreeAlgebra.fermionicProjF {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statisticSubmodule FieldStatistic.fermionic)

The projection of an element of FieldOpFreeAlgebra onto it's fermionic part.

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : fermionicProjF (ofCrAnListF φs) = if h : FieldStatistic.ofList 𝓕.crAnStatistics φs = FieldStatistic.fermionic then ⟨ofCrAnListF φs, ⋯⟩ else 0

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : fermionicProjF (ofCrAnListF φs) = if h : FieldStatistic.ofList 𝓕.crAnStatistics φs = FieldStatistic.bosonic then 0 else ⟨ofCrAnListF φs, ⋯⟩

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.fermionic) : fermionicProjF a = ⟨a, h⟩

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.bosonic) : fermionicProjF a = 0

@[simp]

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_bosonic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : fermionicProjF ↑(a FieldStatistic.bosonic) = 0

@[simp]

theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : fermionicProjF ↑(a FieldStatistic.fermionic) = a FieldStatistic.fermionic

theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_add_fermionicProjF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : ↑(bosonicProjF a) + ↑(fermionicProjF a) = a

theorem FieldSpecification.FieldOpFreeAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun FieldStatistic.bosonic) + ↑(a.toFun FieldStatistic.fermionic)

theorem FieldSpecification.FieldOpFreeAlgebra.directSum_eq_bosonic_plus_fermionic {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) : a = (DirectSum.of (fun (i : FieldStatistic) => ↥(statisticSubmodule i)) FieldStatistic.bosonic) (a FieldStatistic.bosonic) + (DirectSum.of (fun (i : FieldStatistic) => ↥(statisticSubmodule i)) FieldStatistic.fermionic) (a FieldStatistic.fermionic)

instance FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade {𝓕 : FieldSpecification} : GradedAlgebra statisticSubmodule

For a field specification 𝓕, the algebra 𝓕.FieldOpFreeAlgebra is graded by FieldStatistic. Those ofCrAnListF φs for which φs has an overall bosonic statistic (i.e. 𝓕 |>ₛ φs = bosonic) span bosonic submodule, whilst those ofCrAnListF φs for which φs has an overall fermionic statistic (i.e. 𝓕 |>ₛ φs = fermionic) span the fermionic submodule.

theorem FieldSpecification.FieldOpFreeAlgebra.eq_zero_of_bosonic_and_fermionic {𝓕 : FieldSpecification} {a : 𝓕.FieldOpFreeAlgebra} (hb : a ∈ statisticSubmodule FieldStatistic.bosonic) (hf : a ∈ statisticSubmodule FieldStatistic.fermionic) : a = 0

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

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