structure
TriangularDecomposition
(R : Type u_1)
[CommRing R]
(𝔤 : Type u_2)
[LieRing 𝔤]
[LieAlgebra R 𝔤]
:
Type u_2
- 𝔥 : LieSubalgebra R 𝔤
- 𝔫_pos : LieSubalgebra R 𝔤
- 𝔫_neg : LieSubalgebra R 𝔤
- is_cartan : self.𝔥.IsCartanSubalgebra
- h_abelian : IsLieAbelian ↥self.𝔥
Instances For
def
TriangularDecomposition.𝔟
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
LieSubalgebra R 𝔤
Instances For
def
TriangularDecomposition.weightSubspace
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_mod)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Submodule R M
Instances For
theorem
TriangularDecomposition.weightSubspace_eq_mathlib
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
structure
IsHighestWeightModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_mod)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
Type u_mod
- highestWeightVec : M
Instances For
structure
IsVermaModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_mod)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(wt : ↥Δ.𝔥 →ₗ[R] R)
extends IsHighestWeightModule Δ M wt :
Type u_mod
- highestWeightVec : M
- universal_unique (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (η₁ η₂ : M →ₗ⁅R,𝔤⁆ V) : η₁ self.highestWeightVec = η₂ self.highestWeightVec → η₁ = η₂
Instances For
def
ueaSubalgAction
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(𝔫 : LieSubalgebra R 𝔤)
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
:
Instances For
def
instModuleUEASubalg
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(𝔫 : LieSubalgebra R 𝔤)
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
:
Module (UniversalEnvelopingAlgebra R ↥𝔫) M
Instances For
theorem
ueaSubalg_mul_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(u₁ u₂ : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(m : M)
:
((ueaSubalgAction Δ.𝔫_neg M) (u₁ * u₂)) m = ((ueaSubalgAction Δ.𝔫_neg M) u₁) (((ueaSubalgAction Δ.𝔫_neg M) u₂) m)
theorem
ueaSubalg_add_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(u₁ u₂ : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(m : M)
:
((ueaSubalgAction Δ.𝔫_neg M) (u₁ + u₂)) m = ((ueaSubalgAction Δ.𝔫_neg M) u₁) m + ((ueaSubalgAction Δ.𝔫_neg M) u₂) m
theorem
ueaSubalg_smul_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(r : R)
(u₀ : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(m : M)
:
theorem
ueaSubalg_one_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(m : M)
:
theorem
ueaSubalg_ι_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(n : ↥Δ.𝔫_neg)
(m : M)
:
theorem
ueaSubalg_algebraMap_apply
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(r : R)
(m : M)
:
theorem
nminus_orbit_lie_stable
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(x : 𝔤)
(m : M)
(hm : ∃ (u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec = m)
:
∃ (u' : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), ((ueaSubalgAction Δ.𝔫_neg M) u') hM.highestWeightVec = ⁅x, m⁆
theorem
pbw_verma_surjective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
pbw_verma_retraction_from_pbw
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (ψ : M →ₗ[R] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg),
∀ (u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), ψ (((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec) = u
theorem
pbw_verma_phi_injective_of_action
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(hu : ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec = 0)
:
theorem
pbw_verma_retraction_R
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (ψ : M →ₗ[R] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg),
∀ (u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), ψ (((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec) = u
theorem
pbw_verma_action_injective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(hu : ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec = 0)
:
theorem
pbw_verma_left_inverse
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (ψ : M →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg),
ψ ∘ₗ LinearMap.toSpanSingleton (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) M hM.highestWeightVec = LinearMap.id
theorem
pbw_verma_phi_injective_helper
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
pbw_verma_retraction
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (ψ : M →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), ψ hM.highestWeightVec = 1
theorem
pbw_ideal_factorization
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (ψ : M →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg),
ψ ∘ₗ LinearMap.toSpanSingleton (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) M hM.highestWeightVec = LinearMap.id
theorem
pbw_verma_injective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
pbw_verma_bijective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
IsVermaModule.toSpanSingleton_injective
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
IsVermaModule.toSpanSingleton_surjective
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
IsVermaModule.free_over_nminus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (φ : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg ≃ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] M), φ 1 = hM.highestWeightVec
theorem
IsVermaModule.hwv_not_mem_proper
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(N : LieSubmodule R 𝔤 M)
(hN : N ≠ ⊤)
:
hM.highestWeightVec ∉ N
Instances For
theorem
pbw_separation_functional
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (f : M →ₗ[R] R),
f hM.highestWeightVec = 1 ∧ (∀ (u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg),
f (((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec) = (augmentationUEA R ↥Δ.𝔫_neg) u) ∧ ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → ∀ m ∈ N, f m = 0
theorem
pbw_augmentation_hwv_component_zero
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(N : LieSubmodule R 𝔤 M)
(hN : N ≠ ⊤)
(hu : ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec ∈ N)
:
theorem
pbw_augmentation_vanish_proper
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(N : LieSubmodule R 𝔤 M)
(hN : N ≠ ⊤)
(hu : ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec ∈ N)
:
theorem
augmentation_retraction_vanish_on_proper
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(ψ : M →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
:
ψ hM.highestWeightVec = 1 → ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → ∀ m ∈ N, (augmentationUEA R ↥Δ.𝔫_neg) (ψ m) = 0
theorem
pbw_hwv_separation
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (f : M →ₗ[R] R), f hM.highestWeightVec = 1 ∧ ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → ∀ m ∈ N, f m = 0
theorem
IsVermaModule.proper_sSup
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
IsVermaModule.exists_unique_maximal_submodule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (J : LieSubmodule R 𝔤 M), J ≠ ⊤ ∧ ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ J
theorem
IsVermaModule.quotient_by_maximal_irreducible
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(_hM : IsVermaModule Δ M wt)
(J : LieSubmodule R 𝔤 M)
(hJ_ne_top : J ≠ ⊤)
(hJ_max : ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ J)
:
LieModule.IsIrreducible R 𝔤 (M ⧸ J)
theorem
pbw_augmentation_ideal_weight_zero
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(w : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(hw_ker : (augmentationUEA R ↥Δ.𝔫_neg) w = 0)
(hw_wt :
∀ (h : ↥Δ.𝔥),
⁅↑h, ((ueaSubalgAction Δ.𝔫_neg M) w) hM.highestWeightVec⁆ = wt h • ((ueaSubalgAction Δ.𝔫_neg M) w) hM.highestWeightVec)
:
theorem
pbw_nminus_weight_zero_scalar
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(hu :
∀ (h : ↥Δ.𝔥),
⁅↑h, ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec⁆ = wt h • ((ueaSubalgAction Δ.𝔫_neg M) u) hM.highestWeightVec)
:
∃ (c : R), u = (algebraMap R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)) c
theorem
pbw_nminus_singular_proportional
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(u₁ u₂ : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(hu₁_ne : ((ueaSubalgAction Δ.𝔫_neg M) u₁) hM.highestWeightVec ≠ 0)
(hu₁_wt :
∀ (h : ↥Δ.𝔥),
⁅↑h, ((ueaSubalgAction Δ.𝔫_neg M) u₁) hM.highestWeightVec⁆ = μ h • ((ueaSubalgAction Δ.𝔫_neg M) u₁) hM.highestWeightVec)
(hu₁_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, ((ueaSubalgAction Δ.𝔫_neg M) u₁) hM.highestWeightVec⁆ = 0)
(hu₂_wt :
∀ (h : ↥Δ.𝔥),
⁅↑h, ((ueaSubalgAction Δ.𝔫_neg M) u₂) hM.highestWeightVec⁆ = μ h • ((ueaSubalgAction Δ.𝔫_neg M) u₂) hM.highestWeightVec)
(hu₂_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, ((ueaSubalgAction Δ.𝔫_neg M) u₂) hM.highestWeightVec⁆ = 0)
:
∃ (c : R),
((ueaSubalgAction Δ.𝔫_neg M) u₂) hM.highestWeightVec = c • ((ueaSubalgAction Δ.𝔫_neg M) u₁) hM.highestWeightVec
theorem
IsVermaModule.highestWeightSpace_one_dim
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(v : M)
(hv : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = wt h • v)
:
∃ (c : R), v = c • hM.highestWeightVec
def
WeightSpace
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Submodule R M
Instances For
theorem
weightSpace_eq_mathlib_weightSpace
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
theorem
weightSpace_eq_weightSubspace
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
def
weights
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
:
Instances For
structure
PositiveRootData
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
Type (max u_1 u_2)
- corootPairing_add_left (μ ν α : ↥Δ.𝔥 →ₗ[R] R) : self.corootPairing (μ + ν) α = self.corootPairing μ α + self.corootPairing ν α
- corootPairing_nsmul_left (n : ℕ) (μ α : ↥Δ.𝔥 →ₗ[R] R) : self.corootPairing (n • μ) α = n • self.corootPairing μ α
- ι_negRootVec_ne_zero (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ self.posRoots) : (UniversalEnvelopingAlgebra.ι R) (self.negRootVec α hα) ≠ 0
- uea_nminus_noZeroDivisors : NoZeroDivisors (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
- uea_nminus_nontrivial : Nontrivial (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
Instances For
theorem
PositiveRootData.posRoots_coeff_bound
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(a b : ↥Δ.𝔥 →ₗ[R] R)
:
theorem
PositiveRootData.cone_inter_finite
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(a b : ↥Δ.𝔥 →ₗ[R] R)
:
def
PositiveRootData.IsInQPlus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Instances For
theorem
nminus_UEA_weight_in_QPlus
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(rd : PositiveRootData Δ)
(v : M)
(hv : v ∈ WeightSpace Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hu : ((ueaSubalgAction Δ.𝔫_neg M) u) v ∈ WeightSpace Δ M μ)
(hne : ((ueaSubalgAction Δ.𝔫_neg M) u) v ≠ 0)
:
theorem
pbw_weight_subset_QPlus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : WeightSpace Δ M μ ≠ ⊥)
:
theorem
nminus_QPlus_weight_vector
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(rd : PositiveRootData Δ)
(v : M)
(hv : v ∈ WeightSpace Δ M wt)
(β : ↥Δ.𝔥 →ₗ[R] R)
(hβ : rd.IsInQPlus β)
:
∃ (u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg), u ≠ 0 ∧ ((ueaSubalgAction Δ.𝔫_neg M) u) v ∈ WeightSpace Δ M (wt - β)
theorem
pbw_QPlus_subset_weights
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : rd.IsInQPlus (wt - μ))
:
theorem
pbw_verma_weight_iff
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
theorem
IsVermaModule.weight_subset_QPlus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : WeightSpace Δ M μ ≠ ⊥)
:
theorem
IsVermaModule.QPlus_subset_weights
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : rd.IsInQPlus (wt - μ))
:
theorem
IsVermaModule.weight_set_eq
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
:
theorem
IsVermaModule.highest_weight_module_is_quotient
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(V : Type u_mod)
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
(hV : IsHighestWeightModule Δ V wt)
:
∃ (η : M →ₗ⁅R,𝔤⁆ V), Function.Surjective ⇑η
theorem
IsVermaModule.simpleQuotient_of_hwm
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(J : LieSubmodule R 𝔤 M)
(_hJ_ne_top : J ≠ ⊤)
(hJ_max : ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ J)
(V : Type u_mod)
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
(hV : IsHighestWeightModule Δ V wt)
:
∃ (π : V →ₗ⁅R,𝔤⁆ M ⧸ J), Function.Surjective ⇑π
theorem
IsVermaModule.exists_maximal_submodule_irreducible_quotient
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
∃ (J : LieSubmodule R 𝔤 M),
J ≠ ⊤ ∧ (∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ J) ∧ LieModule.IsIrreducible R 𝔤 (M ⧸ J) ∧ ∀ (V : Type u_mod) [inst : AddCommGroup V] [inst_1 : Module R V] [inst_2 : LieRingModule 𝔤 V]
[inst_3 : LieModule R 𝔤 V] (a : IsHighestWeightModule Δ V wt), ∃ (π : V →ₗ⁅R,𝔤⁆ M ⧸ J), Function.Surjective ⇑π
noncomputable def
IsVermaModule.maxProperSubmodule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
LieSubmodule R 𝔤 M
Instances For
theorem
IsVermaModule.maxProperSubmodule_ne_top
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
IsVermaModule.le_maxProperSubmodule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(N : LieSubmodule R 𝔤 M)
(hN : N ≠ ⊤)
:
noncomputable def
IsVermaModule.simpleQuotient
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
Type u_mod
Instances For
@[implicit_reducible]
noncomputable instance
IsVermaModule.simpleQuotient_addCommGroup
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
@[implicit_reducible]
noncomputable instance
IsVermaModule.simpleQuotient_module
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
Module R hM.simpleQuotient
@[implicit_reducible]
noncomputable instance
IsVermaModule.simpleQuotient_lieRingModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
instance
IsVermaModule.simpleQuotient_lieModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
LieModule R 𝔤 hM.simpleQuotient
theorem
pbw_uea_nminus_action_in_weight_spaces
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
:
theorem
verma_weight_decomposition
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
:
theorem
verma_quotient_weight_surj
{R : Type u_3}
[CommRing R]
[IsDomain R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{V : Type u_6}
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
[Module.IsTorsionFree R V]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(η : M →ₗ⁅R,𝔤⁆ V)
(hη : Function.Surjective ⇑η)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(v : V)
(hv : v ∈ Δ.weightSubspace V μ)
:
∃ w ∈ Δ.weightSubspace M μ, η w = v
theorem
verma_module_exists
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
∃ (M : Type u_mod) (x : AddCommGroup M) (x_1 : Module R M) (x_2 : LieRingModule 𝔤 M) (x_3 : LieModule R 𝔤 M),
Nonempty (IsVermaModule Δ M wt)
theorem
verma_weightSubspace_finite
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Module.Finite R ↥(Δ.weightSubspace M μ)
theorem
IsVermaModule.corollary_8_7
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsVermaModule Δ M wt)
(rd : PositiveRootData Δ)
:
theorem
IsHighestWeightModule.highestWeightSpace_one_dim
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsHighestWeightModule Δ M wt)
(v : M)
(hv : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = wt h • v)
:
∃ (c : R), v = c • hM.highestWeightVec
theorem
IsHighestWeightModule.weight_decomposition
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsHighestWeightModule Δ M wt)
:
theorem
IsHighestWeightModule.weightSubspace_finite
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_mod}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(hM : IsHighestWeightModule Δ M wt)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Module.Finite R ↥(Δ.weightSubspace M μ)
def
vermaIdeal
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
Instances For
def
VermaModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
Type (max u_1 u_2)
Instances For
@[implicit_reducible]
instance
VermaModule.instRing
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
Ring (VermaModule Δ wt)
@[implicit_reducible]
instance
VermaModule.instAddCommGroup
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
AddCommGroup (VermaModule Δ wt)
@[implicit_reducible]
instance
VermaModule.instModule
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
Module R (VermaModule Δ wt)
def
VermaModule.highestWeightVec
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
:
VermaModule Δ wt
Instances For
theorem
liftQ_comp_quotKerEquiv_symm_apply
{R : Type u_1}
[CommRing R]
{M₀ : Type u_3}
[AddCommGroup M₀]
[Module R M₀]
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
(f₁ : M₀ →ₗ[R] N₁)
(hf₁ : Function.Surjective ⇑f₁)
(f₂ : M₀ →ₗ[R] N₂)
(h : f₁.ker ≤ f₂.ker)
(m : M₀)
:
noncomputable def
lieModuleEquivOfSurjEqKer
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{M₀ : Type u_3}
{V₁ : Type u_4}
{V₂ : Type u_5}
[AddCommGroup M₀]
[Module R M₀]
[LieRingModule 𝔤 M₀]
[LieModule R 𝔤 M₀]
[AddCommGroup V₁]
[Module R V₁]
[LieRingModule 𝔤 V₁]
[LieModule R 𝔤 V₁]
[AddCommGroup V₂]
[Module R V₂]
[LieRingModule 𝔤 V₂]
[LieModule R 𝔤 V₂]
(η₁ : M₀ →ₗ⁅R,𝔤⁆ V₁)
(hη₁ : Function.Surjective ⇑η₁)
(η₂ : M₀ →ₗ⁅R,𝔤⁆ V₂)
(hη₂ : Function.Surjective ⇑η₂)
(hker : η₁.ker = η₂.ker)
:
Instances For
theorem
ker_ne_top_of_surj_irreducible
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{M₀ : Type u_3}
{V : Type u_4}
[AddCommGroup M₀]
[Module R M₀]
[LieRingModule 𝔤 M₀]
[LieModule R 𝔤 M₀]
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
(η : M₀ →ₗ⁅R,𝔤⁆ V)
(hη : Function.Surjective ⇑η)
(hirr : LieModule.IsIrreducible R 𝔤 V)
:
theorem
ker_eq_unique_max_of_surj_irreducible
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M₀ : Type u_mod}
[AddCommGroup M₀]
[Module R M₀]
[LieRingModule 𝔤 M₀]
[LieModule R 𝔤 M₀]
{wt : ↥Δ.𝔥 →ₗ[R] R}
(_hM : IsVermaModule Δ M₀ wt)
{V : Type u_mod}
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
(η : M₀ →ₗ⁅R,𝔤⁆ V)
(hη : Function.Surjective ⇑η)
(hirr : LieModule.IsIrreducible R 𝔤 V)
(J : LieSubmodule R 𝔤 M₀)
(hJ_ne_top : J ≠ ⊤)
(hJ_max : ∀ (N : LieSubmodule R 𝔤 M₀), N ≠ ⊤ → N ≤ J)
:
theorem
irreducible_highest_weight_unique_up_to_iso
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
(wt : ↥Δ.𝔥 →ₗ[R] R)
(V₁ : Type u_mod)
[AddCommGroup V₁]
[Module R V₁]
[LieRingModule 𝔤 V₁]
[LieModule R 𝔤 V₁]
(V₂ : Type u_mod)
[AddCommGroup V₂]
[Module R V₂]
[LieRingModule 𝔤 V₂]
[LieModule R 𝔤 V₂]
(hV₁ : IsHighestWeightModule Δ V₁ wt)
(hirr₁ : LieModule.IsIrreducible R 𝔤 V₁)
(hV₂ : IsHighestWeightModule Δ V₂ wt)
(hirr₂ : LieModule.IsIrreducible R 𝔤 V₂)
: