def
HasStandardFiltration
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(V : Type uCatO)
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
(_hV : IsCategoryO Δ rd V)
:
Instances For
def
Ext1VanishingForContragredientVerma
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(X : Type uCatO)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
:
Instances For
noncomputable def
CategoryO.compositionLengthO
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(X : Type uCatO)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
:
Instances For
theorem
CategoryO.subsingleton_of_compositionLengthO_zero
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(X : Type uCatO)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hlen : compositionLengthO X hXO = 0)
(x : X)
:
theorem
CategoryO.maximal_weight_hwv_exists
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hlen : compositionLengthO X hXO ≠ 0)
:
theorem
CategoryO.ext_vanishing_verma_iso
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hlen : compositionLengthO X hXO ≠ 0)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(v : X)
(hv_ne : v ≠ 0)
(hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v)
(hv_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0)
:
∃ (Z : LieSubmodule R 𝔤 X) (Q : Type uCatO) (x : AddCommGroup Q) (x_1 : Module R Q) (x_2 : LieRingModule 𝔤 Q) (x_3 :
LieModule R 𝔤 Q) (x_4 : IsVermaModule Δ Q lam) (π : ↥Z →ₗ⁅R,𝔤⁆ Q),
v ∈ Z ∧ Function.Surjective ⇑π ∧ (∀ (x_5 : ↥Z), π x_5 = 0 ↔ ↑x_5 ∈ ⊥) ∧ Z ≠ ⊤
theorem
CategoryO.maximal_weight_verma_submodule
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hlen : compositionLengthO X hXO ≠ 0)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
:
∃ (Z : LieSubmodule R 𝔤 X) (lam_step : ↥Δ.𝔥 →ₗ[R] R) (Q : Type uCatO) (x : AddCommGroup Q) (x_1 : Module R Q) (x_2 :
LieRingModule 𝔤 Q) (x_3 : LieModule R 𝔤 Q) (x_4 : IsVermaModule Δ Q lam_step) (π : ↥Z →ₗ⁅R,𝔤⁆ Q),
Function.Surjective ⇑π ∧ (∀ (x_5 : ↥Z), π x_5 = 0 ↔ ↑x_5 ∈ ⊥) ∧ Z ≠ ⊤
theorem
HasWeightDecomposition_lieSubmodule
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hwd : HasWeightDecomposition Δ X)
(Z : LieSubmodule R 𝔤 X)
:
theorem
IsCategoryO_lieSubmodule_commRing
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
:
IsCategoryO Δ rd ↥Z
theorem
jordanHolder_length_independent
{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]
(cs₁ cs₂ : LieModule.CompositionSeriesOf rd M)
:
theorem
compositionSeries_ses_concat
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(Z : LieSubmodule R 𝔤 X)
(csZ : LieModule.CompositionSeriesOf rd ↥Z)
(csQ : LieModule.CompositionSeriesOf rd (X ⧸ Z))
:
theorem
compositionLengthO_additive_ses
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
(hZO : IsCategoryO Δ rd ↥Z)
(hQO : IsCategoryO Δ rd (X ⧸ Z))
:
CategoryO.compositionLengthO X hXO = CategoryO.compositionLengthO (↥Z) hZO + CategoryO.compositionLengthO (X ⧸ Z) hQO
theorem
compositionLengthO_pos_of_ne_bot
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
(hZO : IsCategoryO Δ rd ↥Z)
(hZ_ne_bot : Z ≠ ⊥)
:
theorem
compositionLengthO_quotient_lt
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
(hZ_ne_top : Z ≠ ⊤)
(hZ_ne_bot : Z ≠ ⊥)
(hQO : IsCategoryO Δ rd (X ⧸ Z))
:
theorem
CategoryO.quotient_in_O_smaller_length
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
(hZ_ne_top : Z ≠ ⊤)
(hZ_ne_bot : Z ≠ ⊥)
:
∃ (Y : Type uCatO) (x : AddCommGroup Y) (x_1 : Module R Y) (x_2 : LieRingModule 𝔤 Y) (x_3 : LieModule R 𝔤 Y) (hYO :
IsCategoryO Δ rd Y) (q : X →ₗ⁅R,𝔤⁆ Y),
Function.Surjective ⇑q ∧ (∀ (x_4 : X), q x_4 = 0 ↔ x_4 ∈ Z) ∧ compositionLengthO Y hYO < compositionLengthO X hXO
theorem
bilinear_vanishing_on_hwv'
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{MmuDual : Type uCatO}
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
{Mmu_inner : Type uCatO}
[AddCommGroup Mmu_inner]
[Module R Mmu_inner]
[LieRingModule 𝔤 Mmu_inner]
[LieModule R 𝔤 Mmu_inner]
(mu : ↥Δ.𝔥 →ₗ[R] R)
(hVerma : IsVermaModule Δ Mmu_inner mu)
(β : MmuDual →ₗ[R] Mmu_inner →ₗ[R] R)
(hβ_contra : ∀ (x : 𝔤) (m : MmuDual) (m' : Mmu_inner), (β ⁅x, m⁆) m' + (β m) ⁅x, m'⁆ = 0)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hmu : lam ≠ mu)
(w : MmuDual)
(hw_cartan : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = lam h • w)
(hw_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, w⁆ = 0)
(w' : MmuDual)
(hw' : w' ∈ LieSubmodule.lieSpan R 𝔤 {w})
:
theorem
contragredient_verma_no_hwv_of_ne'
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(mu : ↥Δ.𝔥 →ₗ[R] R)
(MmuDual : Type uCatO)
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
(hMmuDualO : IsCategoryO Δ rd MmuDual)
(hContra : IsContragredientVerma rd MmuDual mu hMmuDualO)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hmu : lam ≠ mu)
(w : MmuDual)
(hw_cartan : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = lam h • w)
(hw_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, w⁆ = 0)
:
theorem
hom_vanishing_verma_contragredientVerma_neq
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(Z : LieSubmodule R 𝔤 X)
(lam_step : ↥Δ.𝔥 →ₗ[R] R)
(Q : Type uCatO)
[AddCommGroup Q]
[Module R Q]
[LieRingModule 𝔤 Q]
[LieModule R 𝔤 Q]
:
∀ (x : IsVermaModule Δ Q lam_step) (π : ↥Z →ₗ⁅R,𝔤⁆ Q) (_hπ_surj : Function.Surjective ⇑π)
(_hπ_ker : ∀ (x : ↥Z), π x = 0 ↔ ↑x ∈ ⊥) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu_ne : mu ≠ lam_step) (MmuDual : Type uCatO)
[inst : AddCommGroup MmuDual] [inst✝ : Module R MmuDual] [inst✝¹ : LieRingModule 𝔤 MmuDual]
[inst✝² : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual)
(_hContra : IsContragredientVerma rd MmuDual mu hMmuDualO) (f : ↥Z →ₗ⁅R,𝔤⁆ MmuDual), f = 0
theorem
ses_weight_space_surjective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
(Δ : TriangularDecomposition R 𝔤)
{A : Type u_5}
[AddCommGroup A]
[Module R A]
[LieRingModule 𝔤 A]
[LieModule R 𝔤 A]
(hA : HasWeightDecomposition Δ A)
{B : Type u_6}
[AddCommGroup B]
[Module R B]
[LieRingModule 𝔤 B]
[LieModule R 𝔤 B]
(j : A →ₗ⁅R,𝔤⁆ B)
(hj : Function.Injective ⇑j)
{C : Type u_7}
[AddCommGroup C]
[Module R C]
[LieRingModule 𝔤 C]
[LieModule R 𝔤 C]
(q : B →ₗ⁅R,𝔤⁆ C)
(hq : Function.Surjective ⇑q)
(hexact : ∀ (b : B), q b = 0 ↔ ∃ (a : A), j a = b)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(c : C)
(hc : c ∈ WeightSpace Δ C μ)
:
∃ b' ∈ WeightSpace Δ B μ, q b' = c
theorem
HasWeightDecomposition_of_ses
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{A : Type u_5}
[AddCommGroup A]
[Module R A]
[LieRingModule 𝔤 A]
[LieModule R 𝔤 A]
(hA : HasWeightDecomposition Δ A)
{C : Type u_6}
[AddCommGroup C]
[Module R C]
[LieRingModule 𝔤 C]
[LieModule R 𝔤 C]
(hC : HasWeightDecomposition Δ C)
{B : Type u_7}
[AddCommGroup B]
[Module R B]
[LieRingModule 𝔤 B]
[LieModule R 𝔤 B]
(j : A →ₗ⁅R,𝔤⁆ B)
(hj : Function.Injective ⇑j)
(q : B →ₗ⁅R,𝔤⁆ C)
(hq : Function.Surjective ⇑q)
(hexact : ∀ (b : B), q b = 0 ↔ ∃ (a : A), j a = b)
:
theorem
IsCategoryO_of_extension
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{A : Type u_5}
[AddCommGroup A]
[Module R A]
[LieRingModule 𝔤 A]
[LieModule R 𝔤 A]
(hA : IsCategoryO Δ rd A)
{C : Type u_6}
[AddCommGroup C]
[Module R C]
[LieRingModule 𝔤 C]
[LieModule R 𝔤 C]
(hC : IsCategoryO Δ rd C)
{B : Type u_7}
[AddCommGroup B]
[Module R B]
[LieRingModule 𝔤 B]
[LieModule R 𝔤 B]
(j : A →ₗ⁅R,𝔤⁆ B)
(hj : Function.Injective ⇑j)
(q : B →ₗ⁅R,𝔤⁆ C)
(hq : Function.Surjective ⇑q)
(hexact : ∀ (b : B), q b = 0 ↔ ∃ (a : A), j a = b)
:
IsCategoryO Δ rd B
theorem
ext1_vanishing_of_hom_vanishing_and_ext_vanishing_for_X
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
{Y : Type uCatO}
[AddCommGroup Y]
[Module R Y]
[LieRingModule 𝔤 Y]
[LieModule R 𝔤 Y]
(_hYO : IsCategoryO Δ rd Y)
(q : X →ₗ⁅R,𝔤⁆ Y)
(_hq_surj : Function.Surjective ⇑q)
(Z : LieSubmodule R 𝔤 X)
(_hq_ker : ∀ (x : X), q x = 0 ↔ x ∈ Z)
{N : Type uCatO}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(hNO : IsCategoryO Δ rd N)
(hhom_vanish : ∀ (f : ↥Z →ₗ⁅R,𝔤⁆ N), f = 0)
(hExt_X :
∀ (E' : Type uCatO) [inst : AddCommGroup E'] [inst_1 : Module R E'] [inst_2 : LieRingModule 𝔤 E']
[inst_3 : LieModule R 𝔤 E'],
IsCategoryO Δ rd E' →
∀ (i' : N →ₗ⁅R,𝔤⁆ E'),
Function.Injective ⇑i' →
∀ (p' : E' →ₗ⁅R,𝔤⁆ X),
Function.Surjective ⇑p' →
(∀ (e : E'), p' e = 0 ↔ ∃ (m : N), i' m = e) → ∃ (s : X →ₗ⁅R,𝔤⁆ E'), ∀ (x : X), p' (s x) = x)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(i : N →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ Y)
(_hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : N), i m = e)
:
theorem
ext_vanishing_transfer_neq
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
{Y : Type uCatO}
[AddCommGroup Y]
[Module R Y]
[LieRingModule 𝔤 Y]
[LieModule R 𝔤 Y]
(hYO : IsCategoryO Δ rd Y)
(q : X →ₗ⁅R,𝔤⁆ Y)
(hq_surj : Function.Surjective ⇑q)
(Z : LieSubmodule R 𝔤 X)
(hq_ker : ∀ (x : X), q x = 0 ↔ x ∈ Z)
(lam_step : ↥Δ.𝔥 →ₗ[R] R)
(Q : Type uCatO)
[AddCommGroup Q]
[Module R Q]
[LieRingModule 𝔤 Q]
[LieModule R 𝔤 Q]
:
∀ (x : IsVermaModule Δ Q lam_step) (π : ↥Z →ₗ⁅R,𝔤⁆ Q) (hπ_surj : Function.Surjective ⇑π)
(hπ_ker : ∀ (x : ↥Z), π x = 0 ↔ ↑x ∈ ⊥) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu_ne : mu ≠ lam_step) (MmuDual : Type uCatO)
[inst : AddCommGroup MmuDual] [inst✝ : Module R MmuDual] [inst✝¹ : LieRingModule 𝔤 MmuDual]
[inst✝² : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual)
(_hContra : IsContragredientVerma rd MmuDual mu hMmuDualO) (E : Type uCatO) [inst✝³ : AddCommGroup E]
[inst✝⁴ : Module R E] [inst✝⁵ : LieRingModule 𝔤 E] [inst✝⁶ : LieModule R 𝔤 E] (_hEO : IsCategoryO Δ rd E)
(i : MmuDual →ₗ⁅R,𝔤⁆ E) (_hi : Function.Injective ⇑i) (p : E →ₗ⁅R,𝔤⁆ Y) (_hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MmuDual), i m = e), ∃ (s : Y →ₗ⁅R,𝔤⁆ E), ∀ (x : Y), p (s x) = x
theorem
contragredientVerma_injective_in_O
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(_i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑_i)
:
theorem
contragredientVerma_ses_splits
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(_i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑_i)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), _i m = e)
:
theorem
frobenius_reciprocity_coinduction_splitting
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(_i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑_i)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), _i m = e)
:
theorem
frobenius_reciprocity_ext_vanishing_eq_case
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{Y : Type uCatO}
[AddCommGroup Y]
[Module R Y]
[LieRingModule 𝔤 Y]
[LieModule R 𝔤 Y]
(_hYO : IsCategoryO Δ rd Y)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(_i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑_i)
(p : E →ₗ⁅R,𝔤⁆ Y)
(_hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), _i m = e)
:
theorem
ext_vanishing_transfer_eq
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
{Y : Type uCatO}
[AddCommGroup Y]
[Module R Y]
[LieRingModule 𝔤 Y]
[LieModule R 𝔤 Y]
(hYO : IsCategoryO Δ rd Y)
(q : X →ₗ⁅R,𝔤⁆ Y)
(hq_surj : Function.Surjective ⇑q)
(Z : LieSubmodule R 𝔤 X)
(hq_ker : ∀ (x : X), q x = 0 ↔ x ∈ Z)
(lam_step : ↥Δ.𝔥 →ₗ[R] R)
(Q : Type uCatO)
[AddCommGroup Q]
[Module R Q]
[LieRingModule 𝔤 Q]
[LieModule R 𝔤 Q]
:
∀ (x : IsVermaModule Δ Q lam_step) (π : ↥Z →ₗ⁅R,𝔤⁆ Q) (hπ_surj : Function.Surjective ⇑π)
(hπ_ker : ∀ (x : ↥Z), π x = 0 ↔ ↑x ∈ ⊥) (MlamDual : Type uCatO) [inst : AddCommGroup MlamDual]
[inst✝ : Module R MlamDual] [inst✝¹ : LieRingModule 𝔤 MlamDual] [inst✝² : LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual) (_hContra : IsContragredientVerma rd MlamDual lam_step hMlamDualO)
(E : Type uCatO) [inst✝³ : AddCommGroup E] [inst✝⁴ : Module R E] [inst✝⁵ : LieRingModule 𝔤 E]
[inst✝⁶ : LieModule R 𝔤 E] (_hEO : IsCategoryO Δ rd E) (i : MlamDual →ₗ⁅R,𝔤⁆ E) (_hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ Y) (_hp : Function.Surjective ⇑p) (hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e),
∃ (s : Y →ₗ⁅R,𝔤⁆ E), ∀ (x : Y), p (s x) = x
theorem
CategoryO.ext_vanishing_transfer
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
{Y : Type uCatO}
[AddCommGroup Y]
[Module R Y]
[LieRingModule 𝔤 Y]
[LieModule R 𝔤 Y]
(hYO : IsCategoryO Δ rd Y)
(q : X →ₗ⁅R,𝔤⁆ Y)
(hq_surj : Function.Surjective ⇑q)
(Z : LieSubmodule R 𝔤 X)
(hq_ker : ∀ (x : X), q x = 0 ↔ x ∈ Z)
(lam_step : ↥Δ.𝔥 →ₗ[R] R)
(Q : Type uCatO)
[AddCommGroup Q]
[Module R Q]
[LieRingModule 𝔤 Q]
[LieModule R 𝔤 Q]
(hQ : IsVermaModule Δ Q lam_step)
(π : ↥Z →ₗ⁅R,𝔤⁆ Q)
(hπ_surj : Function.Surjective ⇑π)
(hπ_ker : ∀ (x : ↥Z), π x = 0 ↔ ↑x ∈ ⊥)
:
Ext1VanishingForContragredientVerma rd Y hYO
theorem
CategoryO.ext_vanishing_step
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hlen : compositionLengthO X hXO ≠ 0)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
:
∃ (Z : LieSubmodule R 𝔤 X) (lam_step : ↥Δ.𝔥 →ₗ[R] R) (Q : Type uCatO) (x : AddCommGroup Q) (x_1 : Module R Q) (x_2 :
LieRingModule 𝔤 Q) (x_3 : LieModule R 𝔤 Q) (x_4 : IsVermaModule Δ Q lam_step) (π : ↥Z →ₗ⁅R,𝔤⁆ Q),
Function.Surjective ⇑π ∧ (∀ (x_5 : ↥Z), π x_5 = 0 ↔ ↑x_5 ∈ ⊥) ∧ ∃ (Y : Type uCatO) (x : AddCommGroup Y) (x_5 : Module R Y) (x_6 : LieRingModule 𝔤 Y) (x_7 : LieModule R 𝔤 Y) (hYO
: IsCategoryO Δ rd Y) (q : X →ₗ⁅R,𝔤⁆ Y),
Function.Surjective ⇑q ∧ (∀ (x_8 : X), q x_8 = 0 ↔ x_8 ∈ Z) ∧ compositionLengthO Y hYO < compositionLengthO X hXO ∧ Ext1VanishingForContragredientVerma rd Y hYO
theorem
standard_filtration_gluing
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(Z : LieSubmodule R 𝔤 X)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(Q : Type uCatO)
[AddCommGroup Q]
[Module R Q]
[LieRingModule 𝔤 Q]
[LieModule R 𝔤 Q]
:
∀ (x : IsVermaModule Δ Q lam) (π : ↥Z →ₗ⁅R,𝔤⁆ Q) (hπ_surj : Function.Surjective ⇑π)
(hπ_ker : ∀ (x : ↥Z), π x = 0 ↔ ↑x ∈ ⊥) {Y : Type uCatO} [inst : AddCommGroup Y] [inst✝ : Module R Y]
[inst✝¹ : LieRingModule 𝔤 Y] [inst✝² : LieModule R 𝔤 Y] (hYO : IsCategoryO Δ rd Y) (q : X →ₗ⁅R,𝔤⁆ Y)
(hq_surj : Function.Surjective ⇑q) (hq_ker : ∀ (x : X), q x = 0 ↔ x ∈ Z) (hY_sf : HasStandardFiltration rd Y hYO),
HasStandardFiltration rd X hXO
theorem
standard_filtration_of_ext_vanishing
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hExt : Ext1VanishingForContragredientVerma rd X hXO)
:
HasStandardFiltration rd X hXO
theorem
UEA_induction_on_gen
{R : Type u_3}
[CommRing R]
{L : Type u_4}
[LieRing L]
[LieAlgebra R L]
{C : UniversalEnvelopingAlgebra R L → Prop}
(u : UniversalEnvelopingAlgebra R L)
(h_alg : ∀ (r : R), C ((algebraMap R (UniversalEnvelopingAlgebra R L)) r))
(h_ι : ∀ (x : L), C ((UniversalEnvelopingAlgebra.ι R) x))
(h_mul : ∀ (a b : UniversalEnvelopingAlgebra R L), C a → C b → C (a * b))
(h_add : ∀ (a b : UniversalEnvelopingAlgebra R L), C a → C b → C (a + b))
:
C u
theorem
lieModuleHom_ueaSubalg_compat_gen
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
{N : Type u_6}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : M →ₗ⁅R,𝔤⁆ N)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(m : M)
:
theorem
Module.Free.of_right_split_ses
{S : Type u_3}
[Ring S]
{A : Type u_4}
{M : Type u_5}
{B : Type u_6}
[AddCommGroup A]
[AddCommGroup M]
[AddCommGroup B]
[Module S A]
[Module S M]
[Module S B]
(j : A →ₗ[S] M)
(g : M →ₗ[S] B)
(s : B →ₗ[S] M)
(hj_inj : Function.Injective ⇑j)
(hexact : j.range = g.ker)
(hgs : g ∘ₗ s = LinearMap.id)
(hA : Free S A)
(hB : Free S B)
:
Free S M
noncomputable def
lieModuleHomToUEALinearMap_gen
{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 : Type u_6}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : M →ₗ⁅R,𝔤⁆ N)
:
Instances For
theorem
standard_filtration_free_nminus_helper
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hSF : HasStandardFiltration rd X hXO)
:
Module.Free (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) X
theorem
UEA_induction_on_local
{R : Type u_3}
[CommRing R]
{L : Type u_4}
[LieRing L]
[LieAlgebra R L]
{C : UniversalEnvelopingAlgebra R L → Prop}
(u : UniversalEnvelopingAlgebra R L)
(h_alg : ∀ (r : R), C ((algebraMap R (UniversalEnvelopingAlgebra R L)) r))
(h_ι : ∀ (x : L), C ((UniversalEnvelopingAlgebra.ι R) x))
(h_mul : ∀ (a b : UniversalEnvelopingAlgebra R L), C a → C b → C (a * b))
(h_add : ∀ (a b : UniversalEnvelopingAlgebra R L), C a → C b → C (a + b))
:
C u
theorem
lieModuleHom_ueaSubalg_compat_local
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
{N : Type u_6}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : M →ₗ⁅R,𝔤⁆ N)
(u : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg)
(m : M)
:
noncomputable def
lieModuleHomToUEALinearMap_local
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M N : Type uCatO}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : M →ₗ⁅R,𝔤⁆ N)
:
Instances For
theorem
free_nminus_is_projective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXfree : Module.Free (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) X)
:
theorem
projective_nminus_gives_section
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(p : E →ₗ⁅R,𝔤⁆ X)
(hp : Function.Surjective ⇑p)
(hXproj : Module.Projective (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) X)
:
∃ (s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E), ∀ (x : X), p (s₀ x) = x
theorem
frobenius_reciprocity_borel_neg_to_g_section
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(_hKerContra :
∃ (MlamDual : Type uCatO) (x : AddCommGroup MlamDual) (x_1 : Module R MlamDual) (x_2 : LieRingModule 𝔤 MlamDual) (x_3
: LieModule R 𝔤 MlamDual) (hMlamDualO : IsCategoryO Δ rd MlamDual) (_ :
IsContragredientVerma rd MlamDual lam hMlamDualO) (i : MlamDual →ₗ⁅R,𝔤⁆ E),
Function.Injective ⇑i ∧ ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
(_s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
(_hs₀ : ∀ (x : X), p (_s₀ x) = x)
(_hs₀_weight : ∀ (h : ↥Δ.𝔥) (x : X), _s₀ ⁅↑h, x⁆ = ⁅↑h, _s₀ x⁆)
:
noncomputable def
weightSpaceProjector
{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]
(hw : HasWeightDecomposition Δ M)
(μ : ↥Δ.𝔥 →ₗ[R] R)
:
Instances For
theorem
weightSpaceProjector_mem
{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]
(hw : HasWeightDecomposition Δ M)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(m : M)
:
theorem
weightSpaceProjector_sum
{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]
(hw : HasWeightDecomposition Δ M)
(m : M)
:
theorem
weightSpaceProjector_idempotent
{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]
(hw : HasWeightDecomposition Δ M)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(m : M)
:
theorem
weightSpaceProjector_naturality
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{E : Type u_5}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
{X : Type u_6}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hwE : HasWeightDecomposition Δ E)
(hwX : HasWeightDecomposition Δ X)
(f : E →ₗ⁅R,𝔤⁆ X)
(μ : ↥Δ.𝔥 →ₗ[R] R)
(e : E)
:
theorem
weightSpaceProjector_diag_uea_map
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{X : Type u_5}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
{E : Type u_6}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(hwX : HasWeightDecomposition Δ X)
(hwE : HasWeightDecomposition Δ E)
(s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
:
theorem
categoryO_weight_diag_section_ax
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(hEO : IsCategoryO Δ rd E)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
(hs₀ : ∀ (x : X), p (s₀ x) = x)
:
theorem
nminus_section_to_borel_neg_section
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(hEO : IsCategoryO Δ rd E)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
(hs₀ : ∀ (x : X), p (s₀ x) = x)
:
theorem
frobenius_reciprocity_section_lift
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(_hKerContra :
∃ (MlamDual : Type uCatO) (x : AddCommGroup MlamDual) (x_1 : Module R MlamDual) (x_2 : LieRingModule 𝔤 MlamDual) (x_3
: LieModule R 𝔤 MlamDual) (hMlamDualO : IsCategoryO Δ rd MlamDual) (_ :
IsContragredientVerma rd MlamDual lam hMlamDualO) (i : MlamDual →ₗ⁅R,𝔤⁆ E),
Function.Injective ⇑i ∧ ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
(_s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
(_hs₀ : ∀ (x : X), p (_s₀ x) = x)
:
theorem
nminus_section_lifts_to_g_section
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(_hXO : IsCategoryO Δ rd X)
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(lam : ↥Δ.𝔥 →ₗ[R] R)
{MlamDual : Type uCatO}
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ X)
(_hp : Function.Surjective ⇑p)
(_hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
(_s₀ : X →ₗ[UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg] E)
(_hs₀ : ∀ (x : X), p (_s₀ x) = x)
:
theorem
ext1_vanishing_free_nminus_axiom
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hXfree : Module.Free (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) X)
:
Ext1VanishingForContragredientVerma rd X hXO
theorem
free_nminus_splits_contragredient_verma_ses
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hXfree : Module.Free (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) X)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual)
(hContra : IsContragredientVerma rd MlamDual lam hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(hEO : IsCategoryO Δ rd E)
(i : MlamDual →ₗ⁅R,𝔤⁆ E)
(hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ X)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
:
theorem
ext_vanishing_of_standard_filtration_splitting
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hSF : HasStandardFiltration rd X hXO)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual)
(hContra : IsContragredientVerma rd MlamDual lam hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(hEO : IsCategoryO Δ rd E)
(i : MlamDual →ₗ⁅R,𝔤⁆ E)
(hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ X)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
:
theorem
ext_vanishing_of_standard_filtration
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hSF : HasStandardFiltration rd X hXO)
:
Ext1VanishingForContragredientVerma rd X hXO
theorem
standard_filtration_iff_ext_vanishing
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
:
def
IsFreeOverNMinus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(X : Type u_3)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
:
Instances For
theorem
ext1_splits_free_nminus
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hXfree : IsFreeOverNMinus X)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual)
(_hContra : IsContragredientVerma rd MlamDual lam hMlamDualO)
(E : Type uCatO)
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
(_hEO : IsCategoryO Δ rd E)
(i : MlamDual →ₗ⁅R,𝔤⁆ E)
(_hi : Function.Injective ⇑i)
(p : E →ₗ⁅R,𝔤⁆ X)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (e : E), p e = 0 ↔ ∃ (m : MlamDual), i m = e)
:
theorem
free_nminus_has_standard_filtration
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{X : Type uCatO}
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
(hXfree : IsFreeOverNMinus X)
:
HasStandardFiltration rd X hXO
theorem
projective_has_standard_filtration
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{P : Type uCatO}
[AddCommGroup P]
[Module R P]
[LieRingModule 𝔤 P]
[LieModule R 𝔤 P]
(hPO : IsCategoryO Δ rd P)
(hPproj : IsProjectiveInO rd P hPO)
:
HasStandardFiltration rd P hPO
theorem
projective_in_O_is_free_U_nminus
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{wg : WeylGroupData Δ}
{P : Type uCatO}
[AddCommGroup P]
[Module R P]
[LieRingModule 𝔤 P]
[LieModule R 𝔤 P]
(hPO : IsCategoryO Δ rd P)
(hPproj : IsProjectiveInO rd P hPO)
:
Module.Free (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) P
theorem
bgg_reciprocity
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(wg : WeylGroupData Δ)
(lam mu : ↥Δ.𝔥 →ₗ[R] R)
:
theorem
pushout_ses_in_categoryO
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
{Z : Type uCatO}
[AddCommGroup Z]
[Module R Z]
[LieRingModule 𝔤 Z]
[LieModule R 𝔤 Z]
(hZO : IsCategoryO Δ rd Z)
{M : Type uCatO}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(hMO : IsCategoryO Δ rd M)
{N : Type uCatO}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(i : K →ₗ⁅R,𝔤⁆ N)
(hi : Function.Injective ⇑i)
(p : N →ₗ⁅R,𝔤⁆ Z)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (n : N), p n = 0 ↔ ∃ (k : K), i k = n)
(f : K →ₗ⁅R,𝔤⁆ M)
:
∃ (P : Type uCatO) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔤 P) (x_3 : LieModule R 𝔤 P) (_ :
IsCategoryO Δ rd P) (j : M →ₗ⁅R,𝔤⁆ P) (_ : Function.Injective ⇑j) (qP : P →ₗ⁅R,𝔤⁆ Z) (_ : Function.Surjective ⇑qP)
(emb : N →ₗ⁅R,𝔤⁆ P),
(∀ (k : K), emb (i k) = j (f k)) ∧ (∀ (n : N), qP (emb n) = p n) ∧ ∀ (v : P), qP v = 0 → ∃ (m : M), j m = v
theorem
les_restriction_surjective
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
[Module.Finite R E]
[LieModule.IsTrivial 𝔤 E]
{Mlam : Type uCatO}
[AddCommGroup Mlam]
[Module R Mlam]
[LieRingModule 𝔤 Mlam]
[LieModule R 𝔤 Mlam]
(hMlamO : IsCategoryO Δ rd Mlam)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
{Z : Type uCatO}
[AddCommGroup Z]
[Module R Z]
[LieRingModule 𝔤 Z]
[LieModule R 𝔤 Z]
(hZO : IsCategoryO Δ rd Z)
(i : K →ₗ⁅R,𝔤⁆ TensorProduct R E Mlam)
(hi : Function.Injective ⇑i)
(p : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ Z)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (m : TensorProduct R E Mlam), p m = 0 ↔ ∃ (k : K), i k = m)
(mu : ↥Δ.𝔥 →ₗ[R] R)
(MmuDual : Type uCatO)
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
(hMmuDualO : IsCategoryO Δ rd MmuDual)
:
IsContragredientVerma rd MmuDual mu hMmuDualO →
∀
(hExtZ :
∀ (E' : Type uCatO) [inst : AddCommGroup E'] [inst_1 : Module R E'] [inst_2 : LieRingModule 𝔤 E']
[inst_3 : LieModule R 𝔤 E'],
IsCategoryO Δ rd E' →
∀ (j : MmuDual →ₗ⁅R,𝔤⁆ E'),
Function.Injective ⇑j →
∀ (q : E' →ₗ⁅R,𝔤⁆ Z), Function.Surjective ⇑q → ∃ (s : Z →ₗ⁅R,𝔤⁆ E'), ∀ (z : Z), q (s z) = z)
(f : K →ₗ⁅R,𝔤⁆ MmuDual), ∃ (g : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ MmuDual), ∀ (k : K), f k = g (i k)
theorem
bilinear_vanishing_on_hwv
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{MmuDual : Type uCatO}
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
{Mmu_inner : Type uCatO}
[AddCommGroup Mmu_inner]
[Module R Mmu_inner]
[LieRingModule 𝔤 Mmu_inner]
[LieModule R 𝔤 Mmu_inner]
(mu : ↥Δ.𝔥 →ₗ[R] R)
(hVerma : IsVermaModule Δ Mmu_inner mu)
(β : MmuDual →ₗ[R] Mmu_inner →ₗ[R] R)
(hβ_contra : ∀ (x : 𝔤) (m : MmuDual) (m' : Mmu_inner), (β ⁅x, m⁆) m' + (β m) ⁅x, m'⁆ = 0)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hmu : lam ≠ mu)
(w : MmuDual)
(hw_cartan : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = lam h • w)
(hw_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, w⁆ = 0)
(w' : MmuDual)
(hw' : w' ∈ LieSubmodule.lieSpan R 𝔤 {w})
:
theorem
contragredient_verma_no_hwv_of_ne
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(mu : ↥Δ.𝔥 →ₗ[R] R)
(MmuDual : Type uCatO)
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
(hMmuDualO : IsCategoryO Δ rd MmuDual)
(hContra : IsContragredientVerma rd MmuDual mu hMmuDualO)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hmu : lam ≠ mu)
(w : MmuDual)
(hw_cartan : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = lam h • w)
(hw_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, w⁆ = 0)
:
theorem
tensor_hom_vanishing_ne
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
[Module.Finite R E]
[LieModule.IsTrivial 𝔤 E]
{Mlam : Type uCatO}
[AddCommGroup Mlam]
[Module R Mlam]
[LieRingModule 𝔤 Mlam]
[LieModule R 𝔤 Mlam]
(hMlamO : IsCategoryO Δ rd Mlam)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hMlam_verma : IsVermaModule Δ Mlam lam)
(mu : ↥Δ.𝔥 →ₗ[R] R)
(hmu : lam ≠ mu)
(MmuDual : Type uCatO)
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
(hMmuDualO : IsCategoryO Δ rd MmuDual)
(hContra : IsContragredientVerma rd MmuDual mu hMmuDualO)
(g : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ MmuDual)
:
theorem
les_lemma_20_1_hom_vanishing_ne
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
[Module.Finite R E]
[LieModule.IsTrivial 𝔤 E]
{Mlam : Type uCatO}
[AddCommGroup Mlam]
[Module R Mlam]
[LieRingModule 𝔤 Mlam]
[LieModule R 𝔤 Mlam]
(hMlamO : IsCategoryO Δ rd Mlam)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hMlam_verma : IsVermaModule Δ Mlam lam)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
{Z : Type uCatO}
[AddCommGroup Z]
[Module R Z]
[LieRingModule 𝔤 Z]
[LieModule R 𝔤 Z]
(hZO : IsCategoryO Δ rd Z)
(i : K →ₗ⁅R,𝔤⁆ TensorProduct R E Mlam)
(hi : Function.Injective ⇑i)
(p : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ Z)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (m : TensorProduct R E Mlam), p m = 0 ↔ ∃ (k : K), i k = m)
(hExtZ :
∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (MmuDual : Type uCatO) [inst : AddCommGroup MmuDual] [inst_1 : Module R MmuDual]
[inst_2 : LieRingModule 𝔤 MmuDual] [inst_3 : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual),
IsContragredientVerma rd MmuDual mu hMmuDualO →
∀ (E' : Type uCatO) [inst_4 : AddCommGroup E'] [inst_5 : Module R E'] [inst_6 : LieRingModule 𝔤 E']
[inst_7 : LieModule R 𝔤 E'],
IsCategoryO Δ rd E' →
∀ (j : MmuDual →ₗ⁅R,𝔤⁆ E'),
Function.Injective ⇑j →
∀ (q : E' →ₗ⁅R,𝔤⁆ Z), Function.Surjective ⇑q → ∃ (s : Z →ₗ⁅R,𝔤⁆ E'), ∀ (z : Z), q (s z) = z)
(mu : ↥Δ.𝔥 →ₗ[R] R)
(hmu : mu ≠ lam)
(MmuDual : Type uCatO)
[AddCommGroup MmuDual]
[Module R MmuDual]
[LieRingModule 𝔤 MmuDual]
[LieModule R 𝔤 MmuDual]
(hMmuDualO : IsCategoryO Δ rd MmuDual)
(hContra : IsContragredientVerma rd MmuDual mu hMmuDualO)
(f : K →ₗ⁅R,𝔤⁆ MmuDual)
:
theorem
CategoryO.exists_singular_vector_in_submodule
{R : Type u_3}
[Field 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]
(hM : IsCategoryO Δ rd M)
(N : LieSubmodule R 𝔤 M)
(hN : N ≠ ⊥)
:
theorem
contragredient_verma_socle
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(lam : ↥Δ.𝔥 →ₗ[R] R)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
:
IsContragredientVerma rd MlamDual lam _hMlamDualO →
∀ (N : LieSubmodule R 𝔤 MlamDual) (hN : N ≠ ⊥), ∃ v ∈ N, v ∈ WeightSpace Δ MlamDual lam ∧ v ≠ 0
theorem
lie_hom_preserves_weight_space
{R : Type u_3}
[CommRing R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{K : Type u_5}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
{N : Type u_6}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : K →ₗ⁅R,𝔤⁆ N)
(μ : ↥Δ.𝔥 →ₗ[R] R)
{k : K}
(hk : k ∈ WeightSpace Δ K μ)
:
theorem
weight_space_sum_disjoint
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{M : Type u_5}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(lam : ↥Δ.𝔥 →ₗ[R] R)
(S : Finset (↥Δ.𝔥 →ₗ[R] R))
(hlamS : lam ∉ S)
(v : (μ : ↥Δ.𝔥 →ₗ[R] R) → ↥(WeightSpace Δ M μ))
(m : M)
(hm : m ∈ WeightSpace Δ M lam)
(hm_sum : m = ∑ μ ∈ S, ↑(v μ))
:
theorem
contragredient_verma_socle_weight_preimage
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(lam : ↥Δ.𝔥 →ₗ[R] R)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(_hKO : IsCategoryO Δ rd K)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(f : K →ₗ⁅R,𝔤⁆ MlamDual)
(hf : f ≠ 0)
:
∃ k ∈ WeightSpace Δ K lam, k ≠ 0
theorem
nonzero_hom_into_contragredient_gives_weight
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(lam : ↥Δ.𝔥 →ₗ[R] R)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(_hKO : IsCategoryO Δ rd K)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(_hMlamDualO : IsCategoryO Δ rd MlamDual)
(hContra : IsContragredientVerma rd MlamDual lam _hMlamDualO)
(f : K →ₗ⁅R,𝔤⁆ MlamDual)
(hf : f ≠ 0)
:
theorem
socle_hom_vanishing_eq
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(lam : ↥Δ.𝔥 →ₗ[R] R)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
(hK_lam : WeightSpace Δ K lam = ⊥)
(MlamDual : Type uCatO)
[AddCommGroup MlamDual]
[Module R MlamDual]
[LieRingModule 𝔤 MlamDual]
[LieModule R 𝔤 MlamDual]
(hMlamDualO : IsCategoryO Δ rd MlamDual)
(hContra : IsContragredientVerma rd MlamDual lam hMlamDualO)
(f : K →ₗ⁅R,𝔤⁆ MlamDual)
:
theorem
CategoryO.has_simple_quotient
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
[Nontrivial K]
:
∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (Lmu : Type uCatO) (x : AddCommGroup Lmu) (x_1 : Module R Lmu) (x_2 : LieRingModule 𝔤 Lmu) (x_3 :
LieModule R 𝔤 Lmu) (_ : IsCategoryO Δ rd Lmu) (_ : LieModule.IsIrreducible R 𝔤 Lmu) (x_5 :
IsHighestWeightModule Δ Lmu mu) (q : K →ₗ⁅R,𝔤⁆ Lmu), Function.Surjective ⇑q ∧ q ≠ 0
theorem
CategoryO.simple_embeds_in_contragredient_verma
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
(mu : ↥Δ.𝔥 →ₗ[R] R)
(Lmu : Type uCatO)
[AddCommGroup Lmu]
[Module R Lmu]
[LieRingModule 𝔤 Lmu]
[LieModule R 𝔤 Lmu]
(hLmuO : IsCategoryO Δ rd Lmu)
(hIrr : LieModule.IsIrreducible R 𝔤 Lmu)
(hHW : IsHighestWeightModule Δ Lmu mu)
:
∃ (MmuDual : Type uCatO) (x : AddCommGroup MmuDual) (x_1 : Module R MmuDual) (x_2 : LieRingModule 𝔤 MmuDual) (x_3 :
LieModule R 𝔤 MmuDual) (hMmuDualO : IsCategoryO Δ rd MmuDual) (_ : IsContragredientVerma rd MmuDual mu hMmuDualO) (ι :
Lmu →ₗ⁅R,𝔤⁆ MmuDual), Function.Injective ⇑ι
theorem
CategoryO.nontrivial_has_hom_to_contragredient_verma_aux
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
[Nontrivial K]
:
∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (Lmu : Type uCatO) (x : AddCommGroup Lmu) (x_1 : Module R Lmu) (x_2 : LieRingModule 𝔤 Lmu) (_ :
LieModule R 𝔤 Lmu) (MmuDual : Type uCatO) (x_4 : AddCommGroup MmuDual) (x_5 : Module R MmuDual) (x_6 :
LieRingModule 𝔤 MmuDual) (x_7 : LieModule R 𝔤 MmuDual) (hMmuDualO : IsCategoryO Δ rd MmuDual) (_ :
IsContragredientVerma rd MmuDual mu hMmuDualO) (q : K →ₗ⁅R,𝔤⁆ Lmu) (ι : Lmu →ₗ⁅R,𝔤⁆ MmuDual),
Function.Surjective ⇑q ∧ Function.Injective ⇑ι ∧ q ≠ 0
theorem
CategoryO.nonzero_admits_hom_to_contragredient_verma
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
[Nontrivial K]
:
∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (MmuDual : Type uCatO) (x : AddCommGroup MmuDual) (x_1 : Module R MmuDual) (x_2 :
LieRingModule 𝔤 MmuDual) (x_3 : LieModule R 𝔤 MmuDual) (hMmuDualO : IsCategoryO Δ rd MmuDual) (_ :
IsContragredientVerma rd MmuDual mu hMmuDualO) (f : K →ₗ⁅R,𝔤⁆ MmuDual), f ≠ 0
theorem
finite_length_hom_vanishing_implies_zero
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
(hHomVanish :
∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (MmuDual : Type uCatO) [inst : AddCommGroup MmuDual] [inst_1 : Module R MmuDual]
[inst_2 : LieRingModule 𝔤 MmuDual] [inst_3 : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual),
IsContragredientVerma rd MmuDual mu hMmuDualO → ∀ (f : K →ₗ⁅R,𝔤⁆ MmuDual), f = 0)
(k : K)
:
theorem
lemma_20_4_kernel_zero
{R : Type u_3}
[Field R]
{𝔤 : Type u_4}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
{wg : WeylGroupData Δ}
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
[Module.Finite R E]
[LieModule.IsTrivial 𝔤 E]
{Mlam : Type uCatO}
[AddCommGroup Mlam]
[Module R Mlam]
[LieRingModule 𝔤 Mlam]
[LieModule R 𝔤 Mlam]
(hMlamO : IsCategoryO Δ rd Mlam)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hMlam_verma : IsVermaModule Δ Mlam lam)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
{Z : Type uCatO}
[AddCommGroup Z]
[Module R Z]
[LieRingModule 𝔤 Z]
[LieModule R 𝔤 Z]
(hZO : IsCategoryO Δ rd Z)
(i : K →ₗ⁅R,𝔤⁆ TensorProduct R E Mlam)
(hi : Function.Injective ⇑i)
(p : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ Z)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (m : TensorProduct R E Mlam), p m = 0 ↔ ∃ (k : K), i k = m)
(hK_lam : WeightSpace Δ K lam = ⊥)
(hExtZ :
∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (MmuDual : Type uCatO) [inst : AddCommGroup MmuDual] [inst_1 : Module R MmuDual]
[inst_2 : LieRingModule 𝔤 MmuDual] [inst_3 : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual),
IsContragredientVerma rd MmuDual mu hMmuDualO →
∀ (E' : Type uCatO) [inst_4 : AddCommGroup E'] [inst_5 : Module R E'] [inst_6 : LieRingModule 𝔤 E']
[inst_7 : LieModule R 𝔤 E'],
IsCategoryO Δ rd E' →
∀ (j : MmuDual →ₗ⁅R,𝔤⁆ E'),
Function.Injective ⇑j →
∀ (q : E' →ₗ⁅R,𝔤⁆ Z), Function.Surjective ⇑q → ∃ (s : Z →ₗ⁅R,𝔤⁆ E'), ∀ (z : Z), q (s z) = z)
(k : K)
:
noncomputable def
cartanMatrixEntry
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(wg : WeylGroupData Δ)
(lam mu : ↥Δ.𝔥 →ₗ[R] R)
:
Instances For
theorem
cartan_standard_filtration_decomposition
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(wg : WeylGroupData Δ)
(lam mu : ↥Δ.𝔥 →ₗ[R] R)
(S : Finset (↥Δ.𝔥 →ₗ[R] R))
(hS : ∀ nu ∉ S, standardFiltrationMultiplicity rd wg lam nu = 0 ∨ compositionMultiplicity rd wg nu mu = 0)
:
cartanMatrixEntry rd wg lam mu = ∑ nu ∈ S, standardFiltrationMultiplicity rd wg lam nu * compositionMultiplicity rd wg nu mu
theorem
cartan_matrix_factorization
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(wg : WeylGroupData Δ)
(lam mu : ↥Δ.𝔥 →ₗ[R] R)
(S : Finset (↥Δ.𝔥 →ₗ[R] R))
(hS : ∀ nu ∉ S, compositionMultiplicity rd wg nu lam = 0 ∨ compositionMultiplicity rd wg nu mu = 0)
:
cartanMatrixEntry rd wg lam mu = ∑ nu ∈ S, compositionMultiplicity rd wg nu lam * compositionMultiplicity rd wg nu mu
theorem
bgg_theorem
{R : Type u_1}
[CommRing R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
(rd : PositiveRootData Δ)
(wg : WeylGroupData Δ)
(lam mu : ↥Δ.𝔥 →ₗ[R] R)
(hcomp : compositionMultiplicity rd wg lam mu ≠ 0)
:
BruhatLE rd mu lam