1. Physlib
  2. QFT
  3. PerturbationTheory
  4. FieldOpFreeAlgebra
  5. Grading
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic public import Mathlib.RingTheory.GradedAlgebra.Basic

Grading on the FieldOpFreeAlgebra

@[expose] public section

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

def statisticSubmodule (f : FieldStatistic) : Submodule β„‚ 𝓕.FieldOpFreeAlgebra := Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ (𝓕 |>β‚› Ο†s) = f}
lemma ofCrAnListF_mem_statisticSubmodule_of (Ο†s : List 𝓕.CrAnFieldOp) (f : FieldStatistic) (h : (𝓕 |>β‚› Ο†s) = f) : ofCrAnListF Ο†s ∈ statisticSubmodule f := 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOpf:FieldStatistich:ofList 𝓕.crAnStatistics Ο†s = f⊒ ofCrAnListF Ο†s ∈ statisticSubmodule f All goals completed! πŸ™lemma ofCrAnListF_bosonic_or_fermionic (Ο†s : List 𝓕.CrAnFieldOp) : ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic := 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic All goals completed! πŸ™ 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule bosonic ∨ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofCrAnListF Ο†s ∈ statisticSubmodule fermionic exact ofCrAnListF_mem_statisticSubmodule_of Ο†s fermionic (𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ofList 𝓕.crAnStatistics Ο†s = fermionic All goals completed! πŸ™)𝓕:FieldSpecificationΟ†:𝓕.CrAnFieldOp⊒ ofCrAnListF [Ο†] ∈ statisticSubmodule bosonic ∨ ofCrAnListF [Ο†] ∈ statisticSubmodule fermionic All goals completed! πŸ™

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

def bosonicProjF : 𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] statisticSubmodule (𝓕 := 𝓕) bosonic := Basis.constr ofCrAnListFBasis β„‚ fun Ο†s => if h : (𝓕 |>β‚› Ο†s) = bosonic then ⟨ofCrAnListF Ο†s, Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, h⟩⟩⟩ else 0
lemma bosonicProjF_ofCrAnListF (Ο†s : List 𝓕.CrAnFieldOp) : bosonicProjF (ofCrAnListF Ο†s) = if h : (𝓕 |>β‚› Ο†s) = bosonic then ⟨ofCrAnListF Ο†s, Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, h⟩⟩⟩ else 0 := 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp⊒ bosonicProjF (ofCrAnListF Ο†s) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0 conv_lhs => 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp| if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0set_option backward.isDefEq.respectTransparency false in lemma bosonicProjF_of_mem_bosonic (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule bosonic) : bosonicProjF a = ⟨a, h⟩ := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonic⊒ bosonicProjF a = ⟨a, h⟩ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ bosonicProjF a = ⟨a, h⟩ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ p a h 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ p 0 ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p y hy β†’ p (x + y) ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebrahx:βˆƒ Ο†s, x = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hxβŸ©Ο†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ p (ofCrAnListF Ο†s) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ p 0 β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ 0 = ⟨0, β‹―βŸ© All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p y hy β†’ p (x + y) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hy:y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hpx:p x hxhpy:p y hy⊒ p (x + y) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => bosonicProjF a = ⟨a, hx⟩a:β„‚x:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hy:p x hx⊒ p (a β€’ x) β‹― All goals completed! πŸ™lemma bosonicProjF_of_mem_fermionic (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule fermionic) : bosonicProjF a = 0 := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionic⊒ bosonicProjF a = 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ bosonicProjF a = 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ p a h 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ p 0 ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p y hy β†’ p (x + y) ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0x:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0x:𝓕.FieldOpFreeAlgebrahx:βˆƒ Ο†s, x = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0Ο†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ p (ofCrAnListF Ο†s) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ p 0 β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p y hy β†’ p (x + y) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hy:y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hpx:p x hxhpy:p y hy⊒ p (x + y) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => bosonicProjF a = 0a:β„‚x:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hy:p x hx⊒ p (a β€’ x) β‹― All goals completed! πŸ™@[simp] lemma bosonicProjF_of_bonosic_part (a : DirectSum FieldStatistic (fun i => (statisticSubmodule (𝓕 := 𝓕) i))) : bosonicProjF (a bosonic) = a bosonic := 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ bosonicProjF ↑(a bosonic) = a bosonic All goals completed! πŸ™@[simp] lemma bosonicProjF_of_fermionic_part (a : DirectSum FieldStatistic (fun i => (statisticSubmodule (𝓕 := 𝓕) i))) : bosonicProjF (a fermionic).1 = 0 := 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ bosonicProjF ↑(a fermionic) = 0 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ ↑(a fermionic) ∈ statisticSubmodule fermionic All goals completed! πŸ™

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

def fermionicProjF : 𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] statisticSubmodule (𝓕 := 𝓕) fermionic := Basis.constr ofCrAnListFBasis β„‚ fun Ο†s => if h : (𝓕 |>β‚› Ο†s) = fermionic then ⟨ofCrAnListF Ο†s, Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, h⟩⟩⟩ else 0
lemma fermionicProjF_ofCrAnListF (Ο†s : List 𝓕.CrAnFieldOp) : fermionicProjF (ofCrAnListF Ο†s) = if h : (𝓕 |>β‚› Ο†s) = fermionic then ⟨ofCrAnListF Ο†s, Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, h⟩⟩⟩ else 0 := 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp⊒ fermionicProjF (ofCrAnListF Ο†s) = if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0 conv_lhs => 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp| if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOp⊒ (if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ (if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©π“•:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:Β¬ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ (if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ (if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© All goals completed! πŸ™ 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:Β¬ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ (if h : ofList 𝓕.crAnStatistics Ο†s = fermionic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:Β¬ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ 0 = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© 𝓕:FieldSpecificationΟ†s:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ 0 = if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ© All goals completed! πŸ™set_option backward.isDefEq.respectTransparency false in lemma fermionicProjF_of_mem_fermionic (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule fermionic) : fermionicProjF a = ⟨a, h⟩ := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionic⊒ fermionicProjF a = ⟨a, h⟩ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ fermionicProjF a = ⟨a, h⟩ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ p a h 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ p 0 ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p y hy β†’ p (x + y) ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebrahx:βˆƒ Ο†s, x = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hxβŸ©Ο†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = fermionic⊒ p (ofCrAnListF Ο†s) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ p 0 β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ 0 = ⟨0, β‹―βŸ© All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p y hy β†’ p (x + y) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hy:y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hpx:p x hxhpy:p y hy⊒ p (x + y) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule fermionic β†’ Prop := fun a hx => fermionicProjF a = ⟨a, hx⟩a:β„‚x:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = fermionic}hy:p x hx⊒ p (a β€’ x) β‹― All goals completed! πŸ™lemma fermionicProjF_of_mem_bosonic (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ statisticSubmodule bosonic) : fermionicProjF a = 0 := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonic⊒ fermionicProjF a = 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ fermionicProjF a = 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ p a h 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ p 0 ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p y hy β†’ p (x + y) ⋯𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0x:𝓕.FieldOpFreeAlgebrahx:x ∈ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0x:𝓕.FieldOpFreeAlgebrahx:βˆƒ Ο†s, x = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ p x β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah✝:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0Ο†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ p (ofCrAnListF Ο†s) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ p 0 β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}) (hy : y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p y hy β†’ p (x + y) β‹― 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hy:y ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hpx:p x hxhpy:p y hy⊒ p (x + y) β‹― All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0⊒ βˆ€ (a : β„‚) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}), p x hx β†’ p (a β€’ x) β‹― 𝓕:FieldSpecificationa✝:𝓕.FieldOpFreeAlgebrah:a ∈ statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) β†’ a ∈ statisticSubmodule bosonic β†’ Prop := fun a hx => fermionicProjF a = 0a:β„‚x:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnListF Ο†s ∧ ofList 𝓕.crAnStatistics Ο†s = bosonic}hy:p x hx⊒ p (a β€’ x) β‹― All goals completed! πŸ™@[simp] lemma fermionicProjF_of_bosonic_part (a : DirectSum FieldStatistic (fun i => (statisticSubmodule (𝓕 := 𝓕) i))) : fermionicProjF (a bosonic).1 = 0 := 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ fermionicProjF ↑(a bosonic) = 0 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ ↑(a bosonic) ∈ statisticSubmodule bosonic All goals completed! πŸ™@[simp] lemma fermionicProjF_of_fermionic_part (a : DirectSum FieldStatistic (fun i => (statisticSubmodule (𝓕 := 𝓕) i))) : fermionicProjF (a fermionic) = a fermionic := 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ fermionicProjF ↑(a fermionic) = a fermionic All goals completed! πŸ™π“•:FieldSpecificationa:𝓕.FieldOpFreeAlgebraf1:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule bosonic).subtype βˆ˜β‚— bosonicProjFf2:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule fermionic).subtype βˆ˜β‚— fermionicProjFΟ†s:List 𝓕.CrAnFieldOp⊒ ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) + ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©) = ofCrAnListF Ο†s 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraf1:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule bosonic).subtype βˆ˜β‚— bosonicProjFf2:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule fermionic).subtype βˆ˜β‚— fermionicProjFΟ†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) + ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©) = ofCrAnListF Ο†s𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraf1:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule bosonic).subtype βˆ˜β‚— bosonicProjFf2:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule fermionic).subtype βˆ˜β‚— fermionicProjFΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) + ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©) = ofCrAnListF Ο†s 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraf1:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule bosonic).subtype βˆ˜β‚— bosonicProjFf2:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule fermionic).subtype βˆ˜β‚— fermionicProjFΟ†s:List 𝓕.CrAnFieldOph:ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) + ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©) = ofCrAnListF Ο†s All goals completed! πŸ™ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraf1:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule bosonic).subtype βˆ˜β‚— bosonicProjFf2:𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra := (statisticSubmodule fermionic).subtype βˆ˜β‚— fermionicProjFΟ†s:List 𝓕.CrAnFieldOph:Β¬ofList 𝓕.crAnStatistics Ο†s = bosonic⊒ ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then ⟨ofCrAnListF Ο†s, β‹―βŸ© else 0) + ↑(if h : ofList 𝓕.crAnStatistics Ο†s = bosonic then 0 else ⟨ofCrAnListF Ο†s, β‹―βŸ©) = ofCrAnListF Ο†s All goals completed! πŸ™π“•:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:β†₯(statisticSubmodule i)⊒ ↑x = ↑(if h : i = bosonic then Eq.recOn h x else 0) + ↑(if h : i = fermionic then Eq.recOn h x else 0) match i with 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:β†₯(statisticSubmodule bosonic)⊒ ↑x = ↑(if h : bosonic = bosonic then Eq.recOn h x else 0) + ↑(if h : bosonic = fermionic then Eq.recOn h x else 0) All goals completed! πŸ™ 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)i:FieldStatisticx:β†₯(statisticSubmodule fermionic)⊒ ↑x = ↑(if h : fermionic = bosonic then Eq.recOn h x else 0) + ↑(if h : fermionic = fermionic then Eq.recOn h x else 0) All goals completed! πŸ™ 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)⊒ βˆ€ (x y : DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)), C x β†’ C y β†’ C (x + y) 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)x:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)y:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)hx:C xhy:C y⊒ C (x + y) 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => (DirectSum.coeAddMonoidHom statisticSubmodule) a = ↑(a.toFun bosonic) + ↑(a.toFun fermionic)x:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)y:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)hx:(DirectSum.coeAddMonoidHom statisticSubmodule) x = ↑(x bosonic) + ↑(x fermionic)hy:(DirectSum.coeAddMonoidHom statisticSubmodule) y = ↑(y bosonic) + ↑(y fermionic)⊒ ↑(x bosonic) + ↑(x fermionic) + (↑(y bosonic) + ↑(y fermionic)) = ↑(x bosonic) + ↑(y bosonic) + (↑(x fermionic) + ↑(y fermionic)) All goals completed! πŸ™π“•:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:β†₯(statisticSubmodule fermionic)⊒ (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) x = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) 0 + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) x𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:β†₯(statisticSubmodule fermionic)⊒ bosonic β‰  fermionic 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)i:FieldStatisticx:β†₯(statisticSubmodule fermionic)⊒ bosonic β‰  fermionic All goals completed! πŸ™ 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)⊒ βˆ€ (x y : DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)), C x β†’ C y β†’ C (x + y) 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)y:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)hx:C xhy:C y⊒ C (x + y) 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)y:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)hx:x = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (x bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (x fermionic)hy:y = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (y bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (y fermionic)⊒ x + y = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (x bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (y bosonic) + ((DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (x fermionic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (y fermionic)) conv_lhs => 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)C:(DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)) β†’ Prop := fun a => a = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)x:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)y:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)hx:x = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (x bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (x fermionic)hy:y = (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (y bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (y fermionic)| (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (x bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (x fermionic) + ((DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (y bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (y fermionic)) All goals completed! πŸ™

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.

𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ (fun a => (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (bosonicProjF a) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (fermionicProjF a)) (↑(a.toFun bosonic) + ↑(a.toFun fermionic)) = a 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)⊒ (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic) = a conv_rhs => 𝓕:FieldSpecificationa:DirectSum FieldStatistic fun i => β†₯(statisticSubmodule i)| (DirectSum.of (fun i => β†₯(statisticSubmodule i)) bosonic) (a bosonic) + (DirectSum.of (fun i => β†₯(statisticSubmodule i)) fermionic) (a fermionic)
𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrahb✝:a ∈ statisticSubmodule bosonichf:a ∈ statisticSubmodule fermionicha:bosonicProjF a = ⟨a, hb⟩hb:fermionicProjF a = ⟨a, hf⟩hc:β†‘βŸ¨a, hb✝⟩ + β†‘βŸ¨a, hf⟩ = a⊒ a = 0 All goals completed! πŸ™π“•:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = bosonic + bosonic⊒ ↑(bosonicProjF a) * ↑(bosonicProjF b) ∈ statisticSubmodule bosonic conv_lhs => 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = bosonic + bosonic| statisticSubmodule (bosonic + bosonic) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = bosonic + bosonic⊒ ↑(bosonicProjF a) ∈ statisticSubmodule bosonic𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = bosonic + bosonic⊒ ↑(bosonicProjF b) ∈ statisticSubmodule bosonic 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = bosonic + bosonic⊒ ↑(bosonicProjF b) ∈ statisticSubmodule bosonic All goals completed! πŸ™π“•:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = fermionic + fermionic⊒ ↑(fermionicProjF a) * ↑(fermionicProjF b) ∈ statisticSubmodule bosonic conv_lhs => 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = fermionic + fermionic| statisticSubmodule (fermionic + fermionic) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = fermionic + fermionic⊒ ↑(fermionicProjF a) ∈ statisticSubmodule fermionic𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = fermionic + fermionic⊒ ↑(fermionicProjF b) ∈ statisticSubmodule fermionic 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah1:bosonic = fermionic + fermionic⊒ ↑(fermionicProjF b) ∈ statisticSubmodule fermionic All goals completed! πŸ™)] 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊒ ↑(fermionicProjF a) * ↑(bosonicProjF b) + ↑(bosonicProjF a) * ↑(fermionicProjF b) = ↑(bosonicProjF a) * ↑(fermionicProjF b) + ↑(fermionicProjF a) * ↑(bosonicProjF b) All goals completed! πŸ™