/- 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 -/ import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp import HepLean.PerturbationTheory.FieldSpecification.CrAnSection /-! # Creation and annihlation free-algebra This module defines the creation and annihilation algebra for a field structure. The creation and annihilation algebra extends from the state algebra by adding information about whether a state is a creation or annihilation operator. The algebra is spanned by lists of creation/annihilation states. The main structures defined in this module are: * `FieldOpFreeAlgebra` - The creation and annihilation algebra * `ofCrAnOpF` - Maps a creation/annihilation state to the algebra * `ofCrAnListF` - Maps a list of creation/annihilation states to the algebra * `ofFieldOpF` - Maps a state to a sum of creation and annihilation operators * `crPartF` - The creation part of a state in the algebra * `anPartF` - The annihilation part of a state in the algebra * `superCommuteF` - The super commutator on the algebra The key lemmas show how these operators interact, particularly focusing on the super commutation relations between creation and annihilation operators. -/ namespace FieldSpecification variable {𝓕 : FieldSpecification} /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is the free algebra generated by creation and annihilation parts of field operators defined in `𝓕.CrAnFieldOp`. It represents the algebra containing all possible products and linear combinations of creation and annihilation parts of field operators, without imposing any conditions. -/ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra β„‚ 𝓕.CrAnFieldOp namespace FieldOpFreeAlgebra remark naming_convention := " For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix their names with an `F` to indicate that they are related to the free algebra. This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined as a quotient of `FieldOpFreeAlgebra`." /-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a single `𝓕.CrAnFieldOp`. -/ def ofCrAnOpF (Ο† : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := FreeAlgebra.ΞΉ β„‚ Ο† /-- For a field specification `𝓕`, `ofCrAnListF Ο†s` of `𝓕.FieldOpFreeAlgebra` formed by a list `Ο†s` of `𝓕.CrAnFieldOp`. For example for the list `[Ο†β‚αΆœ, φ₂ᡃ, Ο†β‚ƒαΆœ]` we schematically get `Ο†β‚αΆœΟ†β‚‚α΅ƒΟ†β‚ƒαΆœ`. The set of all `ofCrAnListF Ο†s` forms a basis of `FieldOpFreeAlgebra 𝓕`. -/ def ofCrAnListF (Ο†s : List 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofCrAnOpF Ο†s).prod @[simp] lemma ofCrAnListF_nil : ofCrAnListF ([] : List 𝓕.CrAnFieldOp) = 1 := rfl lemma ofCrAnListF_cons (Ο† : 𝓕.CrAnFieldOp) (Ο†s : List 𝓕.CrAnFieldOp) : ofCrAnListF (Ο† :: Ο†s) = ofCrAnOpF Ο† * ofCrAnListF Ο†s := rfl lemma ofCrAnListF_append (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : ofCrAnListF (Ο†s ++ Ο†s') = ofCrAnListF Ο†s * ofCrAnListF Ο†s' := by simp [ofCrAnListF, List.map_append] lemma ofCrAnListF_singleton (Ο† : 𝓕.CrAnFieldOp) : ofCrAnListF [Ο†] = ofCrAnOpF Ο† := by simp [ofCrAnListF] /-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a `𝓕.FieldOp` by summing over the creation and annihilation components of `𝓕.FieldOp`. For example for `φ₁` an incoming asymptotic field operator we get `Ο†β‚αΆœ`, and for `φ₁` a position field operator we get `Ο†β‚αΆœ + φ₁ᡃ`. -/ def ofFieldOpF (Ο† : 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 := βˆ‘ (i : 𝓕.fieldOpToCrAnType Ο†), ofCrAnOpF βŸ¨Ο†, i⟩ /-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a list of `𝓕.FieldOp` by summing over the creation and annihilation components. For example, `φ₁` and `Ο†β‚‚` position states `[Ο†1, Ο†2]` gets sent to `(Ο†1ᢜ+ Ο†1ᡃ) * (Ο†2ᢜ+ Ο†2ᡃ)`. -/ def ofFieldOpListF (Ο†s : List 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofFieldOpF Ο†s).prod /-- Coercion from `List 𝓕.FieldOp` to `FieldOpFreeAlgebra 𝓕` through `ofFieldOpListF`. -/ instance : Coe (List 𝓕.FieldOp) (FieldOpFreeAlgebra 𝓕) := ⟨ofFieldOpListF⟩ @[simp] lemma ofFieldOpListF_nil : ofFieldOpListF ([] : List 𝓕.FieldOp) = 1 := rfl lemma ofFieldOpListF_cons (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕.FieldOp) : ofFieldOpListF (Ο† :: Ο†s) = ofFieldOpF Ο† * ofFieldOpListF Ο†s := rfl lemma ofFieldOpListF_singleton (Ο† : 𝓕.FieldOp) : ofFieldOpListF [Ο†] = ofFieldOpF Ο† := by simp [ofFieldOpListF] lemma ofFieldOpListF_append (Ο†s Ο†s' : List 𝓕.FieldOp) : ofFieldOpListF (Ο†s ++ Ο†s') = ofFieldOpListF Ο†s * ofFieldOpListF Ο†s' := by dsimp only [ofFieldOpListF] rw [List.map_append, List.prod_append] lemma ofFieldOpListF_sum (Ο†s : List 𝓕.FieldOp) : ofFieldOpListF Ο†s = βˆ‘ (s : CrAnSection Ο†s), ofCrAnListF s.1 := by induction Ο†s with | nil => simp | cons Ο† Ο†s ih => rw [CrAnSection.sum_cons] dsimp only [CrAnSection.cons, ofCrAnListF_cons] conv_rhs => enter [2, x] rw [← Finset.mul_sum] rw [← Finset.sum_mul, ofFieldOpListF_cons, ← ih] rfl /-! ## Creation and annihilation parts of a state -/ /-- The algebra map taking an element of the free-state algbra to the part of it in the creation and annihlation free algebra spanned by creation operators. -/ def crPartF : 𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra := fun Ο† => match Ο† with | FieldOp.inAsymp Ο† => ofCrAnOpF ⟨FieldOp.inAsymp Ο†, ()⟩ | FieldOp.position Ο† => ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ | FieldOp.outAsymp _ => 0 @[simp] lemma crPartF_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : crPartF (FieldOp.inAsymp Ο†) = ofCrAnOpF ⟨FieldOp.inAsymp Ο†, ()⟩ := by simp [crPartF] @[simp] lemma crPartF_position (Ο† : 𝓕.Fields Γ— SpaceTime) : crPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ := by simp [crPartF] @[simp] lemma crPartF_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : crPartF (FieldOp.outAsymp Ο†) = 0 := by simp [crPartF] /-- The algebra map taking an element of the free-state algbra to the part of it in the creation and annihilation free algebra spanned by annihilation operators. -/ def anPartF : 𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra := fun Ο† => match Ο† with | FieldOp.inAsymp _ => 0 | FieldOp.position Ο† => ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ | FieldOp.outAsymp Ο† => ofCrAnOpF ⟨FieldOp.outAsymp Ο†, ()⟩ @[simp] lemma anPartF_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : anPartF (FieldOp.inAsymp Ο†) = 0 := by simp [anPartF] @[simp] lemma anPartF_position (Ο† : 𝓕.Fields Γ— SpaceTime) : anPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ := by simp [anPartF] @[simp] lemma anPartF_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : anPartF (FieldOp.outAsymp Ο†) = ofCrAnOpF ⟨FieldOp.outAsymp Ο†, ()⟩ := by simp [anPartF] lemma ofFieldOpF_eq_crPartF_add_anPartF (Ο† : 𝓕.FieldOp) : ofFieldOpF Ο† = crPartF Ο† + anPartF Ο† := by rw [ofFieldOpF] cases Ο† with | inAsymp Ο† => simp [fieldOpToCrAnType] | position Ο† => simp [fieldOpToCrAnType, CreateAnnihilate.sum_eq] | outAsymp Ο† => simp [fieldOpToCrAnType] /-! ## The basis of the creation and annihlation free-algebra. -/ /-- The basis of the free creation and annihilation algebra formed by lists of CrAnFieldOp. -/ noncomputable def ofCrAnListFBasis : Basis (List 𝓕.CrAnFieldOp) β„‚ (FieldOpFreeAlgebra 𝓕) where repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv @[simp] lemma ofListBasis_eq_ofList (Ο†s : List 𝓕.CrAnFieldOp) : ofCrAnListFBasis Ο†s = ofCrAnListF Ο†s := by simp only [ofCrAnListFBasis, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, Basis.coe_ofRepr, AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_apply, AlgEquiv.ofAlgHom_symm_apply, ofCrAnListF] erw [MonoidAlgebra.lift_apply] simp only [zero_smul, Finsupp.sum_single_index, one_smul] rw [@FreeMonoid.lift_apply] match Ο†s with | [] => rfl | Ο† :: Ο†s => erw [List.map_cons] /-! ## Some useful multi-linear maps. -/ /-- The bi-linear map associated with multiplication in `FieldOpFreeAlgebra`. -/ noncomputable def mulLinearMap : FieldOpFreeAlgebra 𝓕 β†’β‚—[β„‚] FieldOpFreeAlgebra 𝓕 β†’β‚—[β„‚] FieldOpFreeAlgebra 𝓕 where toFun a := { toFun := fun b => a * b, map_add' := fun c d => by simp [mul_add] map_smul' := by simp} map_add' := fun a b => by ext c simp [add_mul] map_smul' := by intros ext c simp [smul_mul'] lemma mulLinearMap_apply (a b : FieldOpFreeAlgebra 𝓕) : mulLinearMap a b = a * b := rfl /-- The linear map associated with scalar-multiplication in `FieldOpFreeAlgebra`. -/ noncomputable def smulLinearMap (c : β„‚) : FieldOpFreeAlgebra 𝓕 β†’β‚—[β„‚] FieldOpFreeAlgebra 𝓕 where toFun a := c β€’ a map_add' := by simp map_smul' m x := by simp [smul_smul, RingHom.id_apply, NonUnitalNormedCommRing.mul_comm] end FieldOpFreeAlgebra end FieldSpecification