Verma modules over algebras

This file defines a generalization of the notion of Verma modules used in Lie algebra representation theory.

Main definitions

• vermaIdeal: The left ideal in a 𝕜-algebra A generated by elemements of the form aᵢ - ηᵢ, for some aᵢ ∈ A and ηᵢ ∈ 𝕜.
• VermaModule: The generalized Verma module for a 𝕜-algebra A, defined as the quotient A / vermaIdeal η.
• VermaModule.hwVec: The "highest weight vector" of the Verma module.
• VermaModule.universalMap: The universal property of the Verma module: Given another module M over A and a "target" vector hwv ∈ M satisfying aᵢ • hwv = ηᵢ • hwv for all i, one obtains an A-module map from the Verma module to M uniquely specified by the requirement hwVec η ↦ hwv.

Main statements

• VermaModule.hwVec_cyclic: The Verma module is generated by its highest weight vector.
• VermaModule.range_universalMap_eq_span: The map guaranteed by the universal property of the Verma module is surjective onto the submodule generated by the "target" vector.

Implementation notes

The generalized Verma module for a 𝕜-algebra A is defined as a quotient of A by a left ideal generated by elemements of the form aᵢ - ηᵢ, for some aᵢ ∈ A and ηᵢ ∈ 𝕜. In the file LieVerma.lean this is specialized to the most common case of Verma modules of Lie algebras with a triangular decomposition. The generalized version applies beyond that case, e.g., with Clifford algebras, it allows to construct fermionic Fock spaces.

Tags

Verma module

def VirasoroProject.Ring.smulVectorₗ (R : Type u_1) [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (m : M) : R →ₗ[R] M

A surjective module map from a ring to the submodule generated by a given vector.

Equations

• VirasoroProject.Ring.smulVectorₗ R m = { toFun := fun (a : R) => a • m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem VirasoroProject.Ring.smulVectorₗ_one (R : Type u_1) [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (m : M) : (smulVectorₗ R m) 1 = m

theorem VirasoroProject.Ring.range_smulVectorₗ_eq_span (R : Type u_1) [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (m : M) : (smulVectorₗ R m).range = R ∙ m

theorem VirasoroProject.one_cyclic {R : Type u_1} [Semiring R] : R ∙ 1 = ⊤

The submodule spanned by the unit 1 of a ring is the whole ring.

theorem VirasoroProject.LinearMap.apply_cyclic_of_cyclic_of_surjective {R : Type u_1} [Semiring R] {M₁ : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {f : M₁ →ₗ[R] M₂} (f_surj : f.range = ⊤) (m : M₁) (cyclic : R ∙ m = ⊤) : R ∙ f m = ⊤

A surjective linear map maps any cyclic vector (a vector which generates the whole module) to a cyclic vector.

def VirasoroProject.vermaIdeal {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : Submodule A A

The left ideal used in the construction of a (generalized) Verma module for an algebra A: η : ι → A × 𝕜 is an indexed collection of algebra elements and scalars by which they should act on the "highest weight vector".

Equations

• VirasoroProject.vermaIdeal η = Submodule.span A (Set.range fun (i : ι) => (η i).1 - (algebraMap 𝕜 A) (η i).2)

def VirasoroProject.VermaModule {𝕜 : 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".

Equations

• VirasoroProject.VermaModule η = (A ⧸ VirasoroProject.vermaIdeal η)

def VirasoroProject.VermaModule.hwVec {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : VermaModule η

The highest weight vector in a (generalized) Verma module.

Equations

• VirasoroProject.VermaModule.hwVec η = Submodule.Quotient.mk 1

@[implicit_reducible]

instance VirasoroProject.instAddCommGroupVermaModule {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : AddCommGroup (VermaModule η)

Equations

• VirasoroProject.instAddCommGroupVermaModule η = Submodule.Quotient.addCommGroup (VirasoroProject.vermaIdeal η)

@[implicit_reducible]

instance VirasoroProject.instModuleVermaModule {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : Module A (VermaModule η)

Equations

• VirasoroProject.instModuleVermaModule η = Submodule.Quotient.module (VirasoroProject.vermaIdeal η)

theorem VirasoroProject.VermaModule.hwVec_cyclic {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : A ∙ hwVec η = ⊤

The highest weight vector in a Verma module is cyclic.

theorem VirasoroProject.VermaModule.apply_hwVec_eq {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) (i : ι) : (η i).1 • hwVec η = (algebraMap 𝕜 A) (η i).2 • hwVec η

The defining property of the highest weight vector in a Verma module.

theorem VirasoroProject.vermaIdeal_le_ker_smulVectorₗ {𝕜 : 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) : vermaIdeal η ≤ (Ring.smulVectorₗ A hwv).ker

def VirasoroProject.VermaModule.universalMap {𝕜 : 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) : VermaModule η →ₗ[A] M

The map guaranteed by the universal property of a Verma module.

Equations

• VirasoroProject.VermaModule.universalMap η hwv_prop = (VirasoroProject.vermaIdeal η).liftQ (VirasoroProject.Ring.smulVectorₗ A hwv) ⋯

@[simp]

theorem VirasoroProject.VermaModule.universalMap_hwVec {𝕜 : 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) : (universalMap η hwv_prop) (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.

theorem VirasoroProject.VermaModule.range_universalMap_eq_span {𝕜 : 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) : (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.

structure VirasoroProject.IsVermaModule {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) (M : Type u) (hwv : M) [AddCommGroup M] [Module A M] : Prop

The characteristic predicate of a Verma module.

• hwv_prop (i : ι) : (η i).1 • hwv = (algebraMap 𝕜 A) (η i).2 • hwv
• universal (V : Type u) [AddCommGroup V] [Module A V] (v : V) : (∀ (i : ι), (η i).1 • v = (algebraMap 𝕜 A) (η i).2 • v) → ∃! φ : M →ₗ[A] V, φ hwv = v

noncomputable def VirasoroProject.IsVermaModule.universalMap {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} {η : ι → A × 𝕜} {M : Type u} {hwv : M} [AddCommGroup M] [Module A M] (h : IsVermaModule η M hwv) {V : Type u} [AddCommGroup V] [Module A V] {v : V} (hv : ∀ (i : ι), (η i).1 • v = (algebraMap 𝕜 A) (η i).2 • v) : M →ₗ[A] V

The universal map from a module satisfying the characteristic predicate of a Verma module.

Equations

• h.universalMap hv = Exists.choose ⋯

@[simp]

theorem VirasoroProject.IsVermaModule.universalMap_hwv {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} {η : ι → A × 𝕜} {M : Type u} {hwv : M} [AddCommGroup M] [Module A M] (h : IsVermaModule η M hwv) {V : Type u} [AddCommGroup V] [Module A V] {v : V} (hv : ∀ (i : ι), (η i).1 • v = (algebraMap 𝕜 A) (η i).2 • v) : (h.universalMap hv) hwv = v

The defining property of a universal map from a module satisfying the characteristic predicate of a Verma module.

theorem VirasoroProject.IsVermaModule.universalMap_unique {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} {η : ι → A × 𝕜} {M : Type u} {hwv : M} [AddCommGroup M] [Module A M] (h : IsVermaModule η M hwv) {V : Type u} [AddCommGroup V] [Module A V] {v : V} (hv : ∀ (i : ι), (η i).1 • v = (algebraMap 𝕜 A) (η i).2 • v) {ψ : M →ₗ[A] V} (hψ : ψ hwv = v) : ψ = h.universalMap hv

The uniqueness of the universal map from a module satisfying the characteristic predicate of a Verma module.

theorem VirasoroProject.VermaModule.isVermaModule {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) : IsVermaModule η (VermaModule η) (hwVec η)

noncomputable def VirasoroProject.IsVermaModule.equivOfIsVermaModule {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [Ring A] [Algebra 𝕜 A] {ι : Type u_3} (η : ι → A × 𝕜) (M₁ M₂ : Type u) (hwv₁ : M₁) (hwv₂ : M₂) [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (h₁ : IsVermaModule η M₁ hwv₁) (h₂ : IsVermaModule η M₂ hwv₂) : M₁ ≃ₗ[A] M₂

Uniqueness up to isomorphism of a Verma module, phrased as the construction of an isomorphism between two modules that satisfy the characteristic predicate IsVermaModule.

Equations

• One or more equations did not get rendered due to their size.