Grading on the field operation algebra

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

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

Equations

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

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

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

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

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

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

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

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

Equations

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

Defining bosonicProj

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Defining fermionicProj

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Interaction between bosonicProj and fermionicProj

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

The grading

theorem FieldSpecification.WickAlgebra.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.WickAlgebra.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.WickAlgebra.WickAlgebraGrade {𝓕 : FieldSpecification} : GradedAlgebra statSubmodule

For a field statistic 𝓕, the algebra 𝓕.WickAlgebra 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

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