def
IsSimpleInHCThetaOne
{R : Type u_R}
[CommRing R]
{𝔤 : Type u_𝔤}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(L : LieBimodule R 𝔤)
(θ : CenterCharacter R 𝔤)
(_hL : IsInHCThetaOne L θ)
:
Instances For
def
IsIndecomposableInHCThetaOne
{R : Type u_R}
[CommRing R]
{𝔤 : Type u_𝔤}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(P : LieBimodule R 𝔤)
(θ : CenterCharacter R 𝔤)
(_hP : IsInHCThetaOne P θ)
:
Instances For
def
IsProjectiveCoverInHCThetaOne
{R : Type u_R}
[CommRing R]
{𝔤 : Type u_𝔤}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(P L : LieBimodule R 𝔤)
(θ : CenterCharacter R 𝔤)
(hP : IsInHCThetaOne P θ)
(hL : IsInHCThetaOne L θ)
:
Instances For
def
IsIndecomposableInO
{R : Type u_R}
[CommRing R]
{𝔤 : Type u_𝔤}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(_rd : PositiveRootData Δ)
(P : Type u_mod)
[AddCommGroup P]
[Module R P]
[LieRingModule 𝔤 P]
[LieModule R 𝔤 P]
(_hP : IsCategoryO Δ _rd P)
:
Instances For
def
quotientLieBimodule
{R : Type u}
[CommRing R]
{𝔤 : Type u}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(M : LieBimodule R 𝔤)
(J : Submodule R M.carrier)
(hJ : M.IsSubBimodule J)
:
LieBimodule R 𝔤
Instances For
theorem
theorem_25_6
{R : Type u}
[CommRing R]
{𝔤 : Type u}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
[LieAlgebra.IsSemisimple R 𝔤]
[Module.Finite R 𝔤]
{D : TriangularDecomposition R 𝔤}
{rd : PositiveRootData D}
(wg : WeylGroupData D)
(theta : CenterCharacter R 𝔤)
(Tl : TlambdaData theta)
:
(∀ (mu lam : ↥D.𝔥 →ₗ[R] R),
IsProperRep rd wg mu lam →
∃ (L_xi : LieBimodule R 𝔤) (P_xi : LieBimodule R 𝔤) (hL : IsInHCThetaOne L_xi theta) (hP :
IsInHCThetaOne P_xi theta),
IsSimpleInHCThetaOne L_xi theta hL ∧ IsProjectiveCoverInHCThetaOne P_xi L_xi theta hP hL ∧ ∃ (Q : LieModuleObj R 𝔤),
Nonempty (IsHighestWeightModule D Q.carrier (mu - wg.ρ)) ∧ Nonempty (IsCategoryO D rd Q.carrier) ∧ (∀ (hQO : IsCategoryO D rd Q.carrier), IsProjectiveInO rd Q.carrier hQO) ∧ (∀ (hQO : IsCategoryO D rd Q.carrier), IsIndecomposableInO rd Q.carrier hQO) ∧ Nonempty (LieModuleIso R 𝔤 (Tl.applyObj P_xi hP) Q)) ∧ (∀ (L : LieBimodule R 𝔤) (hL : IsInHCThetaOne L theta),
IsSimpleInHCThetaOne L theta hL →
∃ (mu' : ↥D.𝔥 →ₗ[R] R) (lam' : ↥D.𝔥 →ₗ[R] R),
IsProperRep rd wg mu' lam' ∧ ∃ (L' : LieBimodule R 𝔤) (_ : IsInHCThetaOne L' theta), L.AreIsomorphic L') ∧ ∀ (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P theta),
IsIndecomposableInHCThetaOne P theta hP →
IsProjectiveInHCThetaOne P theta hP →
∃ (mu' : ↥D.𝔥 →ₗ[R] R) (lam' : ↥D.𝔥 →ₗ[R] R),
IsProperRep rd wg mu' lam' ∧ ∃ (P' : LieBimodule R 𝔤) (_ : IsInHCThetaOne P' theta), P.AreIsomorphic P'