PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading

Grading on the FieldOpFreeAlgebra #

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mem_statisticSubmodule_of {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic) (h : FieldStatistic.ofList 𝓕.crAnStatistics φs = f) :
    ofCrAnListF φs ∈ statisticSubmodule f
    source
    theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_bosonic_or_fermionic {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) :
    ofCrAnListF φs ∈ statisticSubmodule FieldStatistic.bosonic ∨ ofCrAnListF φs ∈ statisticSubmodule FieldStatistic.fermionic
    source
    theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_bosonic_or_fermionic {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) :
    ofCrAnOpF φ ∈ statisticSubmodule FieldStatistic.bosonic ∨ ofCrAnOpF φ ∈ statisticSubmodule FieldStatistic.fermionic
    source
    def FieldSpecification.FieldOpFreeAlgebra.bosonicProjF {𝓕 : FieldSpecification} :
    𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statisticSubmodule FieldStatistic.bosonic)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.bosonic) :
      bosonicProjF a = ⟨a, h⟩
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.fermionic) :
      bosonicProjF a = 0
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_bonosic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) :
      bosonicProjF ↑(a FieldStatistic.bosonic) = a FieldStatistic.bosonic
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) :
      bosonicProjF ↑(a FieldStatistic.fermionic) = 0
      source
      def FieldSpecification.FieldOpFreeAlgebra.fermionicProjF {𝓕 : FieldSpecification} :
      𝓕.FieldOpFreeAlgebra →ₗ[ℂ] ↥(statisticSubmodule FieldStatistic.fermionic)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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
        source
        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, ⋯⟩
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_mem_fermionic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.fermionic) :
        fermionicProjF a = ⟨a, h⟩
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_mem_bosonic {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule FieldStatistic.bosonic) :
        fermionicProjF a = 0
        source
        @[simp]
        theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_bosonic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) :
        fermionicProjF ↑(a FieldStatistic.bosonic) = 0
        source
        @[simp]
        theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_fermionic_part {𝓕 : FieldSpecification} (a : DirectSum FieldStatistic fun (i : FieldStatistic) => ↥(statisticSubmodule i)) :
        fermionicProjF ↑(a FieldStatistic.fermionic) = a FieldStatistic.fermionic
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_add_fermionicProjF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) :
        ↑(bosonicProjF a) + ↑(fermionicProjF a) = a
        source
        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)
        source
        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)
        source
        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.

        Equations
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.eq_zero_of_bosonic_and_fermionic {𝓕 : FieldSpecification} {a : 𝓕.FieldOpFreeAlgebra} (hb : a ∈ statisticSubmodule FieldStatistic.bosonic) (hf : a ∈ statisticSubmodule FieldStatistic.fermionic) :
        a = 0
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_mul {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
        ↑(bosonicProjF (a * b)) = ↑(bosonicProjF a) * ↑(bosonicProjF b) + ↑(fermionicProjF a) * ↑(fermionicProjF b)
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_mul {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
        ↑(fermionicProjF (a * b)) = ↑(bosonicProjF a) * ↑(fermionicProjF b) + ↑(fermionicProjF a) * ↑(bosonicProjF b)