VirasoroProject

7.1. A generalized notion of Verma modules🔗

Definition7.1.1
uses 0
Used by 3
Reverse dependency previews
Preview
Lemma 7.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Generalized Verma module. Let A be an algebra over a commutative ring \bbk. Let \eta = (a_i, r_i)_{i \in I} \in (A \times \bbk)^I be a family of pairs of algebra elements a_i \in A and scalars r_i \in \bbk. The generalized Verma module associated to the data \eta is the quotient

\begin{aligned} \Verma^{\eta} = A / J^{\eta} , \end{aligned}

where J^{\eta} \subset A is the left ideal (an A-submodule) of A generated by the elements a_i - r_i \, 1 \in A. Note that \Verma^{\eta} is a (left) A-module.

Lean code for Definition7.1.1●2 definitions
  • defdefined in VirasoroProject/VermaModule.lean
    complete
    def VirasoroProject.VermaModule.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3}
  (η : ι → A × 𝕜) : Type u_2
    def VirasoroProject.VermaModule.{u_1, u_2,
    u_3}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) :
  Type u_2
    The (generalied) Verma module of an algebra `A`:
`η : ι → A × 𝕜` is an indexed collection of algebra elements and scalars by which they should act
on the "highest weight vector".
  • defdefined in VirasoroProject/VermaModule.lean
    complete
    def VirasoroProject.instModuleVermaModule.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3}
  (η : ι → A × 𝕜) : Module A (VirasoroProject.VermaModule η)
    def VirasoroProject.instModuleVermaModule.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) :
  Module A (VirasoroProject.VermaModule η)
Lemma7.1.2
uses 1used by 1✓L∃∀N

The highest weight vector of a Verma module. The vector \VermaHWV^{\eta} := 1 + J^{\eta} \in \Verma^{\eta} (the equivalence class of the unit element of A) is called the highest weight vector of \Verma^{\eta}. It is cyclic, i.e., it generates the whole Verma module \VermaHWV^{\eta} as an A-module, and it satisfies

\begin{aligned} a_i \cdot \VermaHWV^{\eta} = r_i \, \VermaHWV^{\eta} \end{aligned}

for all i \in I, where a_i \in A and r_i \in \bbk are the algebra elements and scalars in the collection \eta = (a_i, r_i)_{i \in I}.

Lean code for Lemma7.1.2●3 declarations
  • defdefined in VirasoroProject/VermaModule.lean
    complete
    def VirasoroProject.VermaModule.hwVec.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3}
  (η : ι → A × 𝕜) : VirasoroProject.VermaModule η
    def VirasoroProject.VermaModule.hwVec.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) :
  VirasoroProject.VermaModule η
    The highest weight vector in a (generalized) Verma module.
  • theoremdefined in VirasoroProject/VermaModule.lean
    complete
    theorem VirasoroProject.VermaModule.hwVec_cyclic.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3}
  (η : ι → A × 𝕜) : A ∙ VirasoroProject.VermaModule.hwVec η = ⊤
    theorem VirasoroProject.VermaModule.hwVec_cyclic.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) :
  A ∙
      VirasoroProject.VermaModule.hwVec
        η =
    ⊤
    The highest weight vector in a Verma module is cyclic.
  • theoremdefined in VirasoroProject/VermaModule.lean
    complete
    theorem VirasoroProject.VermaModule.apply_hwVec_eq.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) (i : ι) :
  (η i).1 • VirasoroProject.VermaModule.hwVec η =
    (algebraMap 𝕜 A) (η i).2 • VirasoroProject.VermaModule.hwVec η
    theorem VirasoroProject.VermaModule.apply_hwVec_eq.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} (η : ι → A × 𝕜) (i : ι) :
  (η i).1 •
      VirasoroProject.VermaModule.hwVec
        η =
    (algebraMap 𝕜 A) (η i).2 •
      VirasoroProject.VermaModule.hwVec η
    The defining property of the highest weight vector in a Verma module.
Proof for Lemma 7.1.2
uses 0

Clear from the construction.

Lemma7.1.3
Statement uses 2
Statement dependency previews
Preview
Definition 7.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Universal property of the Verma module. Suppose that M is an A-module and v \in M is a vector such that

\begin{aligned} a_i \cdot v = r_i \, v \end{aligned}

for all i \in I, where a_i \in A and r_i \in \bbk are the algebra elements and scalars in the collection \eta = (a_i, r_i)_{i \in I}. Then there exists a (unique) A-module homomorphism \phi \colon \Verma^{\eta} \to M such that \phi(\VermaHWV^{\eta}) = v. The range of the map \phi is the submodule generated by v in M.

Lean code for Lemma7.1.3●3 declarations
  • defdefined in VirasoroProject/VermaModule.lean
    complete
    def VirasoroProject.VermaModule.universalMap.{u_1, u_2, u_3, u_4}
  {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4} [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι), (η i).1 • hwv = (algebraMap 𝕜 A) (η i).2 • hwv) :
  VirasoroProject.VermaModule η →ₗ[A] M
    def VirasoroProject.VermaModule.universalMap.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4}
  [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι),
      (η i).1 • hwv =
        (algebraMap 𝕜 A) (η i).2 • hwv) :
  VirasoroProject.VermaModule η →ₗ[A] M
    The map guaranteed by the universal property of a Verma module.
  • theoremdefined in VirasoroProject/VermaModule.lean
    complete
    theorem VirasoroProject.VermaModule.universalMap_hwVec.{u_1, u_2, u_3, u_4}
  {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4} [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι), (η i).1 • hwv = (algebraMap 𝕜 A) (η i).2 • hwv) :
  (VirasoroProject.VermaModule.universalMap η hwv_prop)
      (VirasoroProject.VermaModule.hwVec η) =
    hwv
    theorem VirasoroProject.VermaModule.universalMap_hwVec.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4}
  [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι),
      (η i).1 • hwv =
        (algebraMap 𝕜 A) (η i).2 • hwv) :
  (VirasoroProject.VermaModule.universalMap
        η hwv_prop)
      (VirasoroProject.VermaModule.hwVec
        η) =
    hwv
    The image of the highest weight vector of a Verma module under the map guaranteed by the
universal property is the assigned highest weight vector in the image module.
  • theoremdefined in VirasoroProject/VermaModule.lean
    complete
    theorem VirasoroProject.VermaModule.range_universalMap_eq_span.{u_1, u_2, u_3,
    u_4}
  {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4} [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι), (η i).1 • hwv = (algebraMap 𝕜 A) (η i).2 • hwv) :
  (VirasoroProject.VermaModule.universalMap η hwv_prop).range = A ∙ hwv
    theorem VirasoroProject.VermaModule.range_universalMap_eq_span.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {A : Type u_2}
  [CommRing 𝕜] [Ring A] [Algebra 𝕜 A]
  {ι : Type u_3} {M : Type u_4}
  [AddCommGroup M] [Module A M]
  (η : ι → A × 𝕜) {hwv : M}
  (hwv_prop :
    ∀ (i : ι),
      (η i).1 • hwv =
        (algebraMap 𝕜 A) (η i).2 • hwv) :
  (VirasoroProject.VermaModule.universalMap
        η hwv_prop).range =
    A ∙ hwv
    The range of the map guaranteed by the universal property of a Verma module is the submodule
generated by the assigned highest weight vector in the image module.
Proof for Lemma 7.1.3
uses 0

By cyclicity of the highest weight vector \VermaHWV^{\eta}, any element of \Verma^{\eta} can be written as a \cdot \VermaHWV^{\eta} for some a \in A. The map A \to M given by a \mapsto a \cdot v factors through the quotient by the ideal J^{\eta} by our assumption on v, and since \Verma^{\eta} = A / J^{\eta}, we thus get a well-defined map \phi \colon \Verma^{\eta} \to M with the asserted properties.