Grading on the field operation algebra

def FieldSpecification.FieldOpAlgebra.statSubmodule {𝓕 : FieldSpecification} (f : FieldStatistic) : Submodule ℂ 𝓕.FieldOpAlgebra

The submodule of 𝓕.FieldOpAlgebra spanned by lists of field statistic f.

Equations

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

theorem FieldSpecification.FieldOpAlgebra.ofCrAnList_mem_statSubmodule_of_eq {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic) (h : FieldStatistic.ofList 𝓕.crAnStatistics φs = f) : ofCrAnList φs ∈ statSubmodule f

theorem FieldSpecification.FieldOpAlgebra.ofCrAnList_mem_statSubmodule {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : ofCrAnList φs ∈ statSubmodule (FieldStatistic.ofList 𝓕.crAnStatistics φs)

theorem FieldSpecification.FieldOpAlgebra.mem_bosonic_of_mem_free_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ FieldOpFreeAlgebra.statisticSubmodule FieldStatistic.bosonic) : ι a ∈ statSubmodule FieldStatistic.bosonic

theorem FieldSpecification.FieldOpAlgebra.mem_fermionic_of_mem_free_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ FieldOpFreeAlgebra.statisticSubmodule FieldStatistic.fermionic) : ι a ∈ statSubmodule FieldStatistic.fermionic

theorem FieldSpecification.FieldOpAlgebra.mem_statSubmodule_of_mem_statisticSubmodule {𝓕 : FieldSpecification} (f : FieldStatistic) (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ FieldOpFreeAlgebra.statisticSubmodule f) : ι a ∈ statSubmodule f

def FieldSpecification.FieldOpAlgebra.ιStateSubmodule {𝓕 : FieldSpecification} (f : FieldStatistic) : ↥(FieldOpFreeAlgebra.statisticSubmodule f) →ₗ[ℂ] ↥(statSubmodule f)

The projection of statisticSubmodule (𝓕 := 𝓕) f defined in the free algebra to statSubmodule (𝓕 := 𝓕) f.

Equations

• FieldSpecification.FieldOpAlgebra.ιStateSubmodule f = { toFun := fun (a : ↥(FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule f)) => ⟨↑↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Defining bosonicProj

def FieldSpecification.FieldOpAlgebra.bosonicProjFree {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statSubmodule FieldStatistic.bosonic)

The projection of 𝓕.FieldOpFreeAlgebra to statSubmodule (𝓕 := 𝓕) bosonic.

Equations

• FieldSpecification.FieldOpAlgebra.bosonicProjFree = FieldSpecification.FieldOpAlgebra.ιStateSubmodule FieldStatistic.bosonic ∘ₗ FieldSpecification.FieldOpFreeAlgebra.bosonicProjF

theorem FieldSpecification.FieldOpAlgebra.bosonicProjFree_eq_ι_bosonicProjF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : ↑(bosonicProjFree a) = ι ↑(FieldOpFreeAlgebra.bosonicProjF a)

theorem FieldSpecification.FieldOpAlgebra.bosonicProjFree_zero_of_ι_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) : bosonicProjFree a = 0

theorem FieldSpecification.FieldOpAlgebra.bosonicProjFree_eq_of_equiv {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) : bosonicProjFree a = bosonicProjFree b

def FieldSpecification.FieldOpAlgebra.bosonicProj {𝓕 : FieldSpecification} : 𝓕.FieldOpAlgebra →ₗ[ℂ] ↥(statSubmodule FieldStatistic.bosonic)

The projection of 𝓕.FieldOpAlgebra to statSubmodule (𝓕 := 𝓕) bosonic.

Equations

• FieldSpecification.FieldOpAlgebra.bosonicProj = { toFun := Quotient.lift ⇑FieldSpecification.FieldOpAlgebra.bosonicProjFree ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_eq_bosonicProjFree {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : bosonicProj (ι a) = bosonicProjFree a

Defining fermionicProj

def FieldSpecification.FieldOpAlgebra.fermionicProjFree {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statSubmodule FieldStatistic.fermionic)

The projection of 𝓕.FieldOpFreeAlgebra to statSubmodule (𝓕 := 𝓕) fermionic.

Equations

• FieldSpecification.FieldOpAlgebra.fermionicProjFree = FieldSpecification.FieldOpAlgebra.ιStateSubmodule FieldStatistic.fermionic ∘ₗ FieldSpecification.FieldOpFreeAlgebra.fermionicProjF

theorem FieldSpecification.FieldOpAlgebra.fermionicProjFree_eq_ι_fermionicProjF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : ↑(fermionicProjFree a) = ι ↑(FieldOpFreeAlgebra.fermionicProjF a)

theorem FieldSpecification.FieldOpAlgebra.fermionicProjFree_zero_of_ι_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : ι a = 0) : fermionicProjFree a = 0

theorem FieldSpecification.FieldOpAlgebra.fermionicProjFree_eq_of_equiv {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) : fermionicProjFree a = fermionicProjFree b

def FieldSpecification.FieldOpAlgebra.fermionicProj {𝓕 : FieldSpecification} : 𝓕.FieldOpAlgebra →ₗ[ℂ] ↥(statSubmodule FieldStatistic.fermionic)

The projection of 𝓕.FieldOpAlgebra to statSubmodule (𝓕 := 𝓕) fermionic.

Equations

• FieldSpecification.FieldOpAlgebra.fermionicProj = { toFun := Quotient.lift ⇑FieldSpecification.FieldOpAlgebra.fermionicProjFree ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_eq_fermionicProjFree {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : fermionicProj (ι a) = fermionicProjFree a

Interactino between bosonicProj and fermionicProj

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_add_fermionicProj {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : ↑(bosonicProj a) + ↑(fermionicProj a) = a

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodule FieldStatistic.bosonic) : bosonicProj a = ⟨a, ha⟩

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodule FieldStatistic.fermionic) : fermionicProj a = ⟨a, ha⟩

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodule FieldStatistic.fermionic) : bosonicProj a = 0

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodule FieldStatistic.bosonic) : fermionicProj a = 0

theorem FieldSpecification.FieldOpAlgebra.mem_bosonic_iff_fermionicProj_eq_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : a ∈ statSubmodule FieldStatistic.bosonic ↔ fermionicProj a = 0

theorem FieldSpecification.FieldOpAlgebra.mem_fermionic_iff_bosonicProj_eq_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : a ∈ statSubmodule FieldStatistic.fermionic ↔ bosonicProj a = 0

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_fermionicProj_eq_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : bosonicProj ↑(fermionicProj a) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_bosonicProj_eq_zero {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : fermionicProj ↑(bosonicProj a) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_bosonicProj_eq_bosonicProj {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : bosonicProj ↑(bosonicProj a) = bosonicProj a

@[simp]

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_fermionicProj_eq_fermionicProj {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : fermionicProj ↑(fermionicProj a) = fermionicProj a

@[simp]

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_of_bosonic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statSubmodule i)) : bosonicProj ↑(a FieldStatistic.bosonic) = a FieldStatistic.bosonic

@[simp]

theorem FieldSpecification.FieldOpAlgebra.bosonicProj_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statSubmodule i)) : bosonicProj ↑(a FieldStatistic.fermionic) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_of_bosonic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statSubmodule i)) : fermionicProj ↑(a FieldStatistic.bosonic) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.fermionicProj_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statSubmodule i)) : fermionicProj ↑(a FieldStatistic.fermionic) = a FieldStatistic.fermionic

The grading

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

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

instance FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade {𝓕 : FieldSpecification} : GradedAlgebra statSubmodule

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

Equations

• FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade = GradedRing.mk