def
pbw_triangular_iso
(R : Type u_1)
[CommRing R]
(𝔤 : Type u_2)
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔥) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) ≃ₗ[R] UniversalEnvelopingAlgebra R 𝔤
Instances For
theorem
pbw_triangular_iso_maps_one
(R : Type u_1)
[CommRing R]
(𝔤 : Type u_2)
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
theorem
pbw_triangular_iso_one
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
def
pbw_triangular_inv
(R : Type u_1)
[CommRing R]
(𝔤 : Type u_2)
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
UniversalEnvelopingAlgebra R 𝔤 ≃ₗ[R] TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔥) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos))
Instances For
def
pbw_assoc_iso
(R : Type u_1)
[CommRing R]
(𝔤 : Type u_2)
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
:
TensorProduct R (TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔥))
(UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) ≃ₗ[R] UniversalEnvelopingAlgebra R 𝔤
Instances For
theorem
pbw_weightSpace_surjection_from_fin
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(S : Finset M)
(hS : LieSubmodule.lieSpan R 𝔤 ↑S = ⊤)
(hS_wt : ∀ v ∈ S, ∃ (wt : ↥Δ.𝔥 →ₗ[R] R), v ∈ WeightSpace Δ M wt)
(hbnd : ∃ (bds : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ ν ∈ weights Δ M, ∃ w ∈ bds, rd.IsInQPlus (w - ν))
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : WeightSpace Δ M μ ≠ ⊥)
:
∃ (n : ℕ) (φ : (Fin n → R) →ₗ[R] ↥(WeightSpace Δ M μ)), Function.Surjective ⇑φ
theorem
pbw_weightSpace_moduleFinite
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(S : Finset M)
(hS : LieSubmodule.lieSpan R 𝔤 ↑S = ⊤)
(hS_wt : ∀ v ∈ S, ∃ (wt : ↥Δ.𝔥 →ₗ[R] R), v ∈ WeightSpace Δ M wt)
(hbnd : ∃ (bds : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ ν ∈ weights Δ M, ∃ w ∈ bds, rd.IsInQPlus (w - ν))
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : WeightSpace Δ M μ ≠ ⊥)
:
Module.Finite R ↥(WeightSpace Δ M μ)
theorem
pbw_weightSpace_spanFinite_axiom
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(S : Finset M)
(hS : LieSubmodule.lieSpan R 𝔤 ↑S = ⊤)
(hS_wt : ∀ v ∈ S, ∃ (wt : ↥Δ.𝔥 →ₗ[R] R), v ∈ WeightSpace Δ M wt)
(hbnd : ∃ (bds : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ ν ∈ weights Δ M, ∃ w ∈ bds, rd.IsInQPlus (w - ν))
(μ : ↥Δ.𝔥 →ₗ[R] R)
(hμ : WeightSpace Δ M μ ≠ ⊥)
:
∃ (T : Finset ↥(WeightSpace Δ M μ)), Submodule.span R ↑T = ⊤
theorem
pbw_weightSpace_spanFinite
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(S : Finset M)
(hS : LieSubmodule.lieSpan R 𝔤 ↑S = ⊤)
(hS_wt : ∀ v ∈ S, ∃ (wt : ↥Δ.𝔥 →ₗ[R] R), v ∈ WeightSpace Δ M wt)
(hbnd : ∃ (bds : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ ν ∈ weights Δ M, ∃ w ∈ bds, rd.IsInQPlus (w - ν))
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
∃ (T : Finset ↥(WeightSpace Δ M μ)), Submodule.span R ↑T = ⊤
theorem
IsVermaModule.weight_subspace_finiteDimensional
{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)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Module.Finite R ↥(WeightSpace Δ M μ)
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)
(rd : PositiveRootData Δ)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Module.Finite R ↥(Δ.weightSubspace M μ)