PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic

Creation and annihilation 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:

The key lemmas show how these operators interact, particularly focusing on the super commutation relations between creation and annihilation operators.

source
@[reducible, inline]
abbrev FieldSpecification.FieldOpFreeAlgebra (𝓕 : FieldSpecification) :
Type

For a field specification 𝓕, the algebra 𝓕.FieldOpFreeAlgebra is the free algebra generated by 𝓕.CrAnFieldOp.

Equations
Instances For
    source
    def FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) :
    𝓕.FieldOpFreeAlgebra

    For a field specification 𝓕, and a element Ο† of 𝓕.CrAnFieldOp, ofCrAnOpF Ο† is defined as the element of 𝓕.FieldOpFreeAlgebra formed by Ο†.

    Equations
    Instances For
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.universality {𝓕 : FieldSpecification} {A : Type} [Semiring A] [Algebra β„‚ A] (f : 𝓕.CrAnFieldOp β†’ A) :
      βˆƒ! g : 𝓕.FieldOpFreeAlgebra →ₐ[β„‚] A, ⇑g ∘ ofCrAnOpF = f

      The algebra 𝓕.FieldOpFreeAlgebra satisfies the universal property that for any other algebra A (e.g. the operator algebra of the theory) with a map f : 𝓕.CrAnFieldOp β†’ A (e.g. the inclusion of the creation and annihilation parts of field operators into the operator algebra) there is a unique algebra map g : 𝓕.FieldOpFreeAlgebra β†’ A such that g ∘ ofCrAnOpF = f.

      The unique g is given by FreeAlgebra.lift β„‚ f.

      source
      def FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      𝓕.FieldOpFreeAlgebra

      For a field specification 𝓕, and a list Ο†s of 𝓕.CrAnFieldOp, ofCrAnListF Ο†s is defined as the element of 𝓕.FieldOpFreeAlgebra obtained by the product of ofCrAnListF Ο† for each Ο† in Ο†s. For example ofCrAnListF [φ₁, Ο†β‚‚, φ₃] = ofCrAnOpF φ₁ * ofCrAnOpF Ο†β‚‚ * ofCrAnOpF φ₃. The set of all ofCrAnListF Ο†s forms a basis of FieldOpFreeAlgebra 𝓕.

      Equations
      Instances For
        source
        @[simp]
        theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_nil {𝓕 : FieldSpecification} :
        ofCrAnListF [] = 1
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_cons {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (Ο†s : List 𝓕.CrAnFieldOp) :
        ofCrAnListF (Ο† :: Ο†s) = ofCrAnOpF Ο† * ofCrAnListF Ο†s
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_append {𝓕 : FieldSpecification} (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
        ofCrAnListF (Ο†s ++ Ο†s') = ofCrAnListF Ο†s * ofCrAnListF Ο†s'
        source
        theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_singleton {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) :
        ofCrAnListF [Ο†] = ofCrAnOpF Ο†
        source
        def FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) :
        𝓕.FieldOpFreeAlgebra

        For a field specification 𝓕, and an element Ο† of 𝓕.FieldOp, ofFieldOpF Ο† is the element of 𝓕.FieldOpFreeAlgebra formed by summing over ofCrAnOpF of the creation and annihilation parts of Ο†.

        For example, for Ο† an incoming asymptotic field operator we get ofCrAnOpF βŸ¨Ο†, ()⟩, and for Ο† a position field operator we get ofCrAnOpF βŸ¨Ο†, .create⟩ + ofCrAnOpF βŸ¨Ο†, .annihilate⟩.

        Equations
        Instances For
          source
          def FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.FieldOp) :
          𝓕.FieldOpFreeAlgebra

          For a field specification 𝓕, and a list Ο†s of 𝓕.FieldOp, 𝓕.ofFieldOpListF Ο†s is defined as the element of 𝓕.FieldOpFreeAlgebra obtained by the product of ofFieldOpF Ο† for each Ο† in Ο†s. For example ofFieldOpListF [φ₁, Ο†β‚‚, φ₃] = ofFieldOpF φ₁ * ofFieldOpF Ο†β‚‚ * ofFieldOpF φ₃.

          Equations
          Instances For
            source
            instance FieldSpecification.FieldOpFreeAlgebra.instCoeListFieldOp {𝓕 : FieldSpecification} :
            Coe (List 𝓕.FieldOp) 𝓕.FieldOpFreeAlgebra

            Coercion from List 𝓕.FieldOp to FieldOpFreeAlgebra 𝓕 through ofFieldOpListF.

            Equations
            source
            @[simp]
            theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_nil {𝓕 : FieldSpecification} :
            ofFieldOpListF [] = 1
            source
            theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_cons {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕.FieldOp) :
            ofFieldOpListF (Ο† :: Ο†s) = ofFieldOpF Ο† * ofFieldOpListF Ο†s
            source
            theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_singleton {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) :
            ofFieldOpListF [Ο†] = ofFieldOpF Ο†
            source
            theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_append {𝓕 : FieldSpecification} (Ο†s Ο†s' : List 𝓕.FieldOp) :
            ofFieldOpListF (Ο†s ++ Ο†s') = ofFieldOpListF Ο†s * ofFieldOpListF Ο†s'
            source
            theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_sum {𝓕 : FieldSpecification} (Ο†s : List 𝓕.FieldOp) :
            ofFieldOpListF Ο†s = βˆ‘ s : CrAnSection Ο†s, ofCrAnListF ↑s

            Creation and annihilation parts of a state #

            source
            def FieldSpecification.FieldOpFreeAlgebra.crPartF {𝓕 : FieldSpecification} :
            𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra

            The algebra map taking an element of the free-state algebra to the part of it in the creation and annihilation free algebra spanned by creation operators.

            Equations
            Instances For
              source
              @[simp]
              theorem FieldSpecification.FieldOpFreeAlgebra.crPartF_negAsymp {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) :
              crPartF (FieldOp.inAsymp Ο†) = ofCrAnOpF ⟨FieldOp.inAsymp Ο†, ()⟩
              source
              @[simp]
              theorem FieldSpecification.FieldOpFreeAlgebra.crPartF_position {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.PositionLabel f) Γ— SpaceTime) :
              crPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩
              source
              @[simp]
              theorem FieldSpecification.FieldOpFreeAlgebra.crPartF_posAsymp {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) :
              crPartF (FieldOp.outAsymp Ο†) = 0
              source
              def FieldSpecification.FieldOpFreeAlgebra.anPartF {𝓕 : FieldSpecification} :
              𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra

              The algebra map taking an element of the free-state algebra to the part of it in the creation and annihilation free algebra spanned by annihilation operators.

              Equations
              Instances For
                source
                @[simp]
                theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_negAsymp {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) :
                anPartF (FieldOp.inAsymp Ο†) = 0
                source
                @[simp]
                theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_position {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.PositionLabel f) Γ— SpaceTime) :
                anPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩
                source
                @[simp]
                theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_posAsymp {𝓕 : FieldSpecification} (Ο† : ((f : 𝓕.Field) Γ— 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) :
                anPartF (FieldOp.outAsymp Ο†) = ofCrAnOpF ⟨FieldOp.outAsymp Ο†, ()⟩
                source
                theorem FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_eq_crPartF_add_anPartF {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) :
                ofFieldOpF Ο† = crPartF Ο† + anPartF Ο†

                The basis of the creation and annihilation free-algebra. #

                source
                noncomputable def FieldSpecification.FieldOpFreeAlgebra.ofCrAnListFBasis {𝓕 : FieldSpecification} :
                Basis (List 𝓕.CrAnFieldOp) β„‚ 𝓕.FieldOpFreeAlgebra

                The basis of the free creation and annihilation algebra formed by lists of CrAnFieldOp.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
                  ofCrAnListFBasis Ο†s = ofCrAnListF Ο†s

                  Some useful multi-linear maps. #

                  source
                  noncomputable def FieldSpecification.FieldOpFreeAlgebra.mulLinearMap {𝓕 : FieldSpecification} :
                  𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra

                  The bi-linear map associated with multiplication in FieldOpFreeAlgebra.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem FieldSpecification.FieldOpFreeAlgebra.mulLinearMap_apply {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
                    (mulLinearMap a) b = a * b
                    source
                    noncomputable def FieldSpecification.FieldOpFreeAlgebra.smulLinearMap {𝓕 : FieldSpecification} (c : β„‚) :
                    𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra

                    The linear map associated with scalar-multiplication in FieldOpFreeAlgebra.

                    Equations
                    Instances For