def HasWeightDecomposition {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] : Prop

structure IsCategoryO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] : Prop

• finitely_generated : ∃ (S : Finset M), LieSubmodule.lieSpan R 𝔤 ↑S = ⊤
• weight_decomp : HasWeightDecomposition Δ M
• weight_bound : ∃ (bds : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ μ ∈ weights Δ M, ∃ wt ∈ bds, rd.IsInQPlus (wt - μ)

theorem PositiveRootData.IsInQPlus_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) : rd.IsInQPlus 0

theorem PositiveRootData.IsInQPlus_trans {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wt0 μ ν : ↥Δ.𝔥 →ₗ[R] R) (h1 : rd.IsInQPlus (wt0 - μ)) (h2 : rd.IsInQPlus (μ - ν)) : rd.IsInQPlus (wt0 - ν)

def WeightLE {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (μ wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

def ReflectionLT {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (α μ wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

def BruhatLE {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (μ wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem PBW.weightSpace_spanFinite {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_4} [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 CategoryO.weightSpace_finiteDimensional {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (μ : ↥Δ.𝔥 →ₗ[R] R) : Module.Finite R ↥(WeightSpace Δ M μ)

noncomputable def pbw_abelian_iso (R : Type u_4) [CommRing R] (L : Type u_5) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] : UniversalEnvelopingAlgebra R L ≃ₐ[R] SymmetricAlgebra R L

theorem hilbert_noether_commRing {R : Type u_4} [CommRing R] [IsNoetherianRing R] {A : Type u_5} [CommRing A] [Algebra R A] {G : Type u_6} [Group G] [Fintype G] (algAct : G →* A ≃ₐ[R] A) (hA_fg : ⊤.FG) : (Subalgebra.invariants G algAct).FG

theorem symmetric_algebra_fg_top (R : Type u_4) [CommRing R] (L : Type u_5) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] [Module.Free R L] [Module.Finite R L] : ⊤.FG

noncomputable def conjActionThroughPBW {R : Type u_4} [CommRing R] {L : Type u_5} [LieRing L] [LieAlgebra R L] [IsLieAbelian L] {G : Type u_6} [Group G] (act : G →* UniversalEnvelopingAlgebra R L ≃ₐ[R] UniversalEnvelopingAlgebra R L) : G →* SymmetricAlgebra R L ≃ₐ[R] SymmetricAlgebra R L

theorem invariantSubalgebra_fg_of_abelian_finiteGroup {R : Type u_4} [CommRing R] [IsNoetherianRing R] {L : Type u_5} [LieRing L] [LieAlgebra R L] [IsLieAbelian L] [Module.Free R L] [Module.Finite R L] {G : Type u_6} [Group G] [Fintype G] (act : G →* UniversalEnvelopingAlgebra R L ≃ₐ[R] UniversalEnvelopingAlgebra R L) : (Subalgebra.invariants G act).FG

theorem chevalley_invariant_finiteType {R : Type u_4} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] (wg : WeylGroupData Δ) : Algebra.FiniteType R ↥wg.invariantSubalgebra

theorem center_UEA_finitelyGenerated_of_HC {R : Type u_4} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] (wg : WeylGroupData Δ) : ∃ (S : Finset ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), z ∈ Algebra.adjoin R ↑S

theorem center_UEA_finitelyGenerated {R : Type u_4} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] (wg : WeylGroupData Δ) : ∃ (S : Finset ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), z ∈ Algebra.adjoin R ↑S

theorem center_element_integral_on_catO {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) : ∃ (p : Polynomial R), p.Monic ∧ (Polynomial.aeval (ueaAct ↑z)) p = 0

theorem CategoryO.center_acts_through_finiteDim_quotient {R : Type u_4} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ueaAct ↑z ∈ S

def GeneralizedEigenspaceCenter {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) : Submodule R M

def IsInCategoryOChi {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) : Prop

def GeneralizedEigenspaceCenter.toLieSubmodule {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) : LieSubmodule R 𝔤 M

theorem GeneralizedEigenspaceCenter.toLieSubmodule_coe {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) : ↑(toLieSubmodule M ueaAct hcompat chi) = GeneralizedEigenspaceCenter M ueaAct chi

theorem commute_pow_sub_smul_id {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (f g : Module.End R M) (hcomm : g * f = f * g) (c : R) (k : ℕ) (x : M) : ((f - c • LinearMap.id) ^ k) (g x) = g (((f - c • LinearMap.id) ^ k) x)

theorem orthogonal_idempotent_decomposition_core {R : Type u_4} [CommRing R] {A : Type u_5} [CommRing A] [Algebra R A] {M : Type u_6} [AddCommGroup M] [Module R M] (actA : A →ₐ[R] Module.End R M) (hfg : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (a : A), actA a ∈ S) : ∃ (n : ℕ) (es : Fin n → Module.End R M) (chis : Fin n → A →ₐ[R] R), (∀ (i : Fin n), es i * es i = es i) ∧ (∀ (i j : Fin n), i ≠ j → es i * es j = 0) ∧ (∀ (m : M), (∑ i : Fin n, es i) m = m) ∧ (∀ (i : Fin n) (a : A), ∃ (N : ℕ), ∀ (m : M), ((actA a - (chis i) a • LinearMap.id) ^ N) ((es i) m) = 0) ∧ (∀ (i : Fin n) (a : A), es i * actA a = actA a * es i) ∧ ∀ (i j : Fin n), i ≠ j → ∃ (a : A), IsUnit ((chis i) a - (chis j) a)

theorem orthogonal_idempotent_decomposition_of_fg_center_action {R : Type u_4} [CommRing R] {A : Type u_5} [CommRing A] [Algebra R A] {M : Type u_6} [AddCommGroup M] [Module R M] (actA : A →ₐ[R] Module.End R M) (hfg : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (a : A), actA a ∈ S) : ∃ (n : ℕ) (es : Fin n → Module.End R M) (chis : Fin n → A →ₐ[R] R), (∀ (i : Fin n), es i * es i = es i) ∧ (∀ (i j : Fin n), i ≠ j → es i * es j = 0) ∧ (∀ (m : M), (∑ i : Fin n, es i) m = m) ∧ (∀ (i : Fin n) (a : A), ∃ (N : ℕ), ∀ (m : M), ((actA a - (chis i) a • LinearMap.id) ^ N) ((es i) m) = 0) ∧ (∀ (i : Fin n) (a : A), es i * actA a = actA a * es i) ∧ ∀ (i : Fin n) (m : M), (∀ (a : A), ∃ (N : ℕ), ((actA a - (chis i) a • LinearMap.id) ^ N) m = 0) → (es i) m = m

theorem artinian_generalized_eigenspace_decomposition {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hfindim : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ueaAct ↑z ∈ S) : ∃ (n : ℕ) (chis : Fin n → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R), (∀ (i j : Fin n), i ≠ j → Disjoint (GeneralizedEigenspaceCenter M ueaAct (chis i)) (GeneralizedEigenspaceCenter M ueaAct (chis j))) ∧ ⨆ (i : Fin n), GeneralizedEigenspaceCenter M ueaAct (chis i) = ⊤

theorem CategoryO.infinitesimalCharacter_decomposition {R : Type u_4} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) : ∃ (n : ℕ) (chis : Fin n → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (N : Fin n → LieSubmodule R 𝔤 M), (∀ (i j : Fin n), i ≠ j → Disjoint (N i) (N j)) ∧ ⨆ (i : Fin n), N i = ⊤ ∧ ∀ (i : Fin n), ↑(N i) = GeneralizedEigenspaceCenter M ueaAct (chis i)

noncomputable def idealStepFilt {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {ι : Type u_6} (T : ι → Module.End R M) (N : Submodule R M) : Submodule R M

noncomputable def idealChainFilt {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {ι : Type u_6} (T : ι → Module.End R M) : ℕ → Submodule R M

theorem locally_nilpotent_ideal_chain_terminates {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {ι : Type u_6} (T : ι → Module.End R M) (hcomm : ∀ (z₁ z₂ : ι), T z₁ ∘ₗ T z₂ = T z₂ ∘ₗ T z₁) (hfin : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (z : ι), T z ∈ S) (hnil : ∀ (z : ι) (m : M), ∃ (n : ℕ), (T z ^ n) m = 0) : ∃ (N : ℕ), idealChainFilt T N = ⊥

theorem idealChainFilt_antitone {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {ι : Type u_6} (T : ι → Module.End R M) (n : ℕ) : idealChainFilt T (n + 1) ≤ idealChainFilt T n

theorem mem_idealChainFilt_succ {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {ι : Type u_6} (T : ι → Module.End R M) (n : ℕ) (z : ι) (m : M) (hm : m ∈ idealChainFilt T n) : (T z) m ∈ idealChainFilt T (n + 1)

theorem idealChainFilt_lie_stable {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {ι : Type u_7} (T : ι → Module.End R M) (hcomm : ∀ (x : 𝔤) (z : ι) (m : M), ⁅x, (T z) m⁆ = (T z) ⁅x, m⁆) (n : ℕ) (x : 𝔤) (m : M) : m ∈ idealChainFilt T n → ⁅x, m⁆ ∈ idealChainFilt T n

theorem artinian_madic_filtration {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (hfindim : ∃ (S : Submodule R (Module.End R M)), Module.Finite R ↥S ∧ ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ueaAct ↑z ∈ S) (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (hchi : GeneralizedEigenspaceCenter M ueaAct chi = ⊤) : ∃ (k : ℕ) (F : Fin (k + 1) → Submodule R M), F ⟨0, ⋯⟩ = ⊤ ∧ F ⟨k, ⋯⟩ = ⊥ ∧ (∀ (i : Fin k), F i.castSucc ≥ F i.succ) ∧ (∀ (i : Fin (k + 1)) (x : 𝔤), ∀ m ∈ F i, ⁅x, m⁆ ∈ F i) ∧ ∀ (i : Fin k) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), ∀ m ∈ F i.castSucc, (ueaAct ↑z) m - chi z • m ∈ F i.succ

theorem CategoryO.detecting_submodule_gives_chain_bound {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (E : Submodule R M) (hdetect : ∀ (N₁ N₂ : LieSubmodule R 𝔤 M), N₁ < N₂ → ∃ x ∈ ↑N₂ ⊓ E, x ∉ ↑N₁) (n : ℕ) (hE_bound : ∀ (chain : Fin (n + 2) → Submodule R M), (∀ (i : Fin (n + 2)), chain i ≤ E) → StrictMono chain → False) (chain : Fin (n + 2) → LieSubmodule R 𝔤 M) : StrictMono chain → False

theorem section4_weightSpace_iSupIndep {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] : iSupIndep fun (μ : ↥Δ.𝔥 →ₗ[R] R) => WeightSpace Δ M μ

theorem weightSpace_iSupIndep {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] : iSupIndep fun (μ : ↥Δ.𝔥 →ₗ[R] R) => WeightSpace Δ M μ

theorem weightSpace_sum_eq_zero_components {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (S : Finset (↥Δ.𝔥 →ₗ[R] R)) (v : (μ : ↥Δ.𝔥 →ₗ[R] R) → ↥(WeightSpace Δ M μ)) (hsum : ∑ μ ∈ S, ↑(v μ) = 0) (μ : ↥Δ.𝔥 →ₗ[R] R) (hμ : μ ∈ S) : ↑(v μ) = 0

theorem lieSubmodule_weight_decomp {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hwd : HasWeightDecomposition Δ M) (N : LieSubmodule R 𝔤 M) (m : M) (hm : m ∈ N) : ∃ (T : Finset (↥Δ.𝔥 →ₗ[R] R)) (w : (μ : ↥Δ.𝔥 →ₗ[R] R) → ↥(WeightSpace Δ M μ)), m = ∑ μ ∈ T, ↑(w μ) ∧ ∀ μ ∈ T, ↑(w μ) ∈ N

theorem weightDecomp_component_mem_lieSubmodule {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hwd : HasWeightDecomposition Δ M) (N : LieSubmodule R 𝔤 M) (m : M) (hm : m ∈ N) (S : Finset (↥Δ.𝔥 →ₗ[R] R)) (v : (μ : ↥Δ.𝔥 →ₗ[R] R) → ↥(WeightSpace Δ M μ)) (hdecomp : m = ∑ μ ∈ S, ↑(v μ)) (μ : ↥Δ.𝔥 →ₗ[R] R) (hμ : μ ∈ S) : ↑(v μ) ∈ N

theorem pbw_lieSubmodule_wellFoundedGT {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hfg : ∃ (S : Finset M), LieSubmodule.lieSpan R 𝔤 ↑S = ⊤) : WellFoundedGT (LieSubmodule R 𝔤 M)

theorem lieSubmodule_finitelyGenerated {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hfg : ∃ (S : Finset M), LieSubmodule.lieSpan R 𝔤 ↑S = ⊤) (N : LieSubmodule R 𝔤 M) : ∃ (S : Finset ↥N), LieSubmodule.lieSpan R 𝔤 ↑S = ⊤

theorem IsCategoryO_lieSubmodule {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (N : LieSubmodule R 𝔤 M) : IsCategoryO Δ rd ↥N

theorem IsCategoryO_quotient {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {X : Type u_6} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hXO : IsCategoryO Δ rd X) (Z : LieSubmodule R 𝔤 X) : IsCategoryO Δ rd (X ⧸ Z)

theorem CategoryO.subquotient_has_weight_vector {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (N₁ N₂ : LieSubmodule R 𝔤 M) (hlt : N₁ < N₂) : ∃ (γ : ↥Δ.𝔥 →ₗ[R] R), ∃ x ∈ ↑N₂ ⊓ WeightSpace Δ M γ, x ∉ ↑N₁

theorem PositiveRootData.qPlus_cone_inter_finite {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (a b : ↥Δ.𝔥 →ₗ[R] R) : ∃ (T : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ (γ : ↥Δ.𝔥 →ₗ[R] R), rd.IsInQPlus (a - γ) → rd.IsInQPlus (b - γ) → γ ∈ T

theorem casimir_coset_weight_finite {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (wt : ↥Δ.𝔥 →ₗ[R] R) : ∃ (T : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ γ ∈ weights Δ M, rd.IsInQPlus (wt - γ) → γ ∈ T

theorem CategoryO.casimir_weight_finiteness {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : ∃ (S : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ (γ : ↥Δ.𝔥 →ₗ[R] R), (∃ (N₁ : LieSubmodule R 𝔤 M) (N₂ : LieSubmodule R 𝔤 M), N₁ < N₂ ∧ ∃ x ∈ ↑N₂ ⊓ WeightSpace Δ M γ, x ∉ ↑N₁) → γ ∈ S

theorem CategoryO.casimir_singular_weight_detection {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : ∃ (S : Finset (↥Δ.𝔥 →ₗ[R] R)), ∀ (N₁ N₂ : LieSubmodule R 𝔤 M), N₁ < N₂ → ∃ γ ∈ S, ∃ x ∈ ↑N₂ ⊓ WeightSpace Δ M γ, x ∉ ↑N₁

theorem strictMono_fin_le_val {n : ℕ} {f : Fin n → ℕ} (hf : StrictMono f) (i : Fin n) : ↑i ≤ f i

theorem findim_submodule_chain_bound {K : Type u_4} [DivisionRing K] {V : Type u_5} [AddCommGroup V] [Module K V] (E : Submodule K V) [FiniteDimensional K ↥E] (chain : Fin (Module.finrank K ↥E + 2) → Submodule K V) : (∀ (i : Fin (Module.finrank K ↥E + 2)), chain i ≤ E) → StrictMono chain → False

theorem CategoryO.weightSpaceSum_chain_bound {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) (S : Finset (↥Δ.𝔥 →ₗ[R] R)) : ∃ (n : ℕ), ∀ (chain : Fin (n + 2) → Submodule R M), (∀ (i : Fin (n + 2)), chain i ≤ ⨆ μ ∈ S, WeightSpace Δ M μ) → StrictMono chain → False

theorem CategoryO.casimir_detecting_submodule {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : ∃ (E : Submodule R M) (n : ℕ), (∀ (N₁ N₂ : LieSubmodule R 𝔤 M), N₁ < N₂ → ∃ x ∈ ↑N₂ ⊓ E, x ∉ ↑N₁) ∧ ∀ (chain : Fin (n + 2) → Submodule R M), (∀ (i : Fin (n + 2)), chain i ≤ E) → StrictMono chain → False

theorem CategoryO.finite_length {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : ∃ (n : ℕ), ∀ (chain : Fin (n + 2) → LieSubmodule R 𝔤 M), StrictMono chain → False

theorem CategoryO.wellFoundedGT {R : Type u_4} [Field R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : WellFoundedGT (LieSubmodule R 𝔤 M)

theorem lie_hom_commutes_uea_act {R : Type u_3} [CommRing R] {L : Type u_4} [LieRing L] [LieAlgebra R L] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : Type u_6} [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L⁆ N) (u : UniversalEnvelopingAlgebra R L) (m : M) : f ((((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R L M)) u) m) = (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R L N)) u) (f m)

theorem uea_pbw_degree_function (R : Type u_3) [CommRing R] (L : Type u_4) [LieRing L] [LieAlgebra R L] : ∃ (v : UniversalEnvelopingAlgebra R L → WithBot ℤ), v 0 = ⊥ ∧ (∀ (a : UniversalEnvelopingAlgebra R L), a ≠ 0 → v a ≠ ⊥) ∧ ∀ (a b : UniversalEnvelopingAlgebra R L), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b

theorem uea_noZeroDivisors_of_pbw (R : Type u_3) [CommRing R] (L : Type u_4) [LieRing L] [LieAlgebra R L] : NoZeroDivisors (UniversalEnvelopingAlgebra R L)

theorem verma_hom_injective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {Mmu : Type u_5} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_6} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (wt_mu wt_lam : ↥Δ.𝔥 →ₗ[R] R) (hMmu : IsVermaModule Δ Mmu wt_mu) (hMlam : IsVermaModule Δ Mlam wt_lam) (eta : Mmu →ₗ⁅R,𝔤⁆ Mlam) (hne : eta ≠ 0) : Function.Injective ⇑eta

theorem verma_singular_one_dim {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) (v₁ v₂ : M) (hv₁_ne : v₁ ≠ 0) (hv₁_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v₁⁆ = μ h • v₁) (hv₁_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v₁⁆ = 0) (hv₂_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v₂⁆ = μ h • v₂) (hv₂_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v₂⁆ = 0) : ∃ (c : R), v₂ = c • v₁

theorem verma_hom_unique_up_to_scalar {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {Mmu : Type u_5} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_6} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (wt_mu wt_lam : ↥Δ.𝔥 →ₗ[R] R) (hMmu : IsVermaModule Δ Mmu wt_mu) (hMlam : IsVermaModule Δ Mlam wt_lam) (eta eta' : Mmu →ₗ⁅R,𝔤⁆ Mlam) (heta_ne : eta ≠ 0) : ∃ (c : R), ∀ (m : Mmu), eta' m = c • eta m

theorem IsVermaModule.universal_map' {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_vm} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} (hM : IsVermaModule Δ M wt) {V : Type u_vm} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (v : V) (hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = wt h • v) (hv_npos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) : ∃ (η : M →ₗ⁅R,𝔤⁆ V), η hM.highestWeightVec = v

theorem verma_hom_same_weight {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {Mmu : Type u_vhsw} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_vhsw} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (wt : ↥Δ.𝔥 →ₗ[R] R) (hMmu : IsVermaModule Δ Mmu wt) (hMlam : IsVermaModule Δ Mlam wt) : ∃ (eta : Mmu →ₗ⁅R,𝔤⁆ Mlam), eta ≠ 0

theorem exercise_8_15_weight_space_has_singular {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hM : IsVermaModule Δ M wt) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (n : ℕ) (hn : 0 < n) (hcoroot : rd.corootPairing (wt + wg.ρ) α = ↑n) : ∃ (v : ↥(Δ.weightSubspace M (wt - n • α))), ↑v ≠ 0 ∧ ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, ↑v⁆ = 0

theorem exercise_8_15_singular_vector {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hM : IsVermaModule Δ M wt) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (n : ℕ) (hn : 0 < n) (hcoroot : rd.corootPairing (wt + wg.ρ) α = ↑n) : ∃ (v : M), v ≠ 0 ∧ (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = (wt - n • α) h • v) ∧ ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0

theorem shapovalov_singular_vector_step {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mlam : Type u_5} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α mu lam) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : ∃ (v : Mlam), v ≠ 0 ∧ (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = (mu - wg.ρ) h • v) ∧ ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0

theorem verma_hom_single_step {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mmu : Type u_vhss} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_vhss} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α mu lam) (hMmu : IsVermaModule Δ Mmu (mu - wg.ρ)) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : ∃ (eta : Mmu →ₗ⁅R,𝔤⁆ Mlam), eta ≠ 0

theorem verma_hom_exists {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mmu : Type u_vhe} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_vhe} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hle : BruhatLE rd mu lam) (hMmu : IsVermaModule Δ Mmu (mu - wg.ρ)) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : ∃ (eta : Mmu →ₗ⁅R,𝔤⁆ Mlam), eta ≠ 0

theorem verma_theorem {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mmu : Type u_vt} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔤 Mmu] [LieModule R 𝔤 Mmu] {Mlam : Type u_vt} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hle : BruhatLE rd mu lam) (hMmu : IsVermaModule Δ Mmu (mu - wg.ρ)) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : ∃ (eta : Mmu →ₗ⁅R,𝔤⁆ Mlam), eta ≠ 0 ∧ Function.Injective ⇑eta ∧ ∀ (eta' : Mmu →ₗ⁅R,𝔤⁆ Mlam), ∃ (c : R), ∀ (m : Mmu), eta' m = c • eta m

theorem verma_composition_factor {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mlam : Type u_5} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hle : BruhatLE rd mu lam) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : ∃ (N : LieSubmodule R 𝔤 Mlam), ∃ N' < N, Nonempty (IsHighestWeightModule Δ (↥N ⧸ LieSubmodule.comap N.incl N') (mu - wg.ρ))

theorem IsInQPlus_antisymm_catO {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (μ : ↥Δ.𝔥 →ₗ[R] R) (hpos : rd.IsInQPlus μ) (hneg : rd.IsInQPlus (-μ)) : μ = 0

theorem CategoryO.exists_maximal_weight_vector {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] (hM : IsCategoryO Δ rd M) [Nontrivial M] : ∃ (v : M) (μ : ↥Δ.𝔥 →ₗ[R] R), v ≠ 0 ∧ (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = μ h • v) ∧ ∀ (ν : ↥Δ.𝔥 →ₗ[R] R) (w : M), (∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = ν h • w) → rd.IsInQPlus (ν - μ) → ν ≠ μ → w = 0

theorem root_vec_raises_weight_local {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] (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (μ : ↥Δ.𝔥 →ₗ[R] R) (w : M) (hw_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = μ h • w) (h : ↥Δ.𝔥) : ⁅↑h, ⁅↑(rd.posRootVec α hα), w⁆⁆ = (α + μ) h • ⁅↑(rd.posRootVec α hα), w⁆

theorem CategoryO.exists_singular_vector {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] (hM : IsCategoryO Δ rd M) [Nontrivial M] : ∃ (v : M) (lam : ↥Δ.𝔥 →ₗ[R] R), v ≠ 0 ∧ (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) ∧ ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0

theorem CategoryO.simple_objects_are_highest_weight {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] (hM : IsCategoryO Δ rd M) (hirr : LieModule.IsIrreducible R 𝔤 M) : ∃ (lam : ↥Δ.𝔥 →ₗ[R] R), Nonempty (IsHighestWeightModule Δ M lam)

def WeylStabilizerModQ {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (x : ↥Δ.𝔥 →ₗ[R] R) : Set wg.W

def WeylStabilizer {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (x : ↥Δ.𝔥 →ₗ[R] R) : Set wg.W

theorem WeylStabilizer_mul_closed {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (x : ↥Δ.𝔥 →ₗ[R] R) {w₁ w₂ : wg.W} (h₁ : w₁ ∈ WeylStabilizer rd wg x) (h₂ : w₂ ∈ WeylStabilizer rd wg x) : w₁ * w₂ ∈ WeylStabilizer rd wg x

structure RootSystemWithReflections {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) : Type (max (max u_3 u_4) u_5)

• allRoots : Finset (↥Δ.𝔥 →ₗ[R] R)
• posRoots_sub (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ rd.posRoots → α ∈ self.allRoots
• roots_pos_or_neg (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → α ∈ rd.posRoots ∨ -α ∈ rd.posRoots
• reflection : (↥Δ.𝔥 →ₗ[R] R) → wg.W
• coroot : (↥Δ.𝔥 →ₗ[R] R) → ↥Δ.𝔥
• corootPairing_eq_eval (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), rd.corootPairing μ α = μ (self.coroot α)
• reflection_formula (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction (self.reflection α) μ = μ - μ (self.coroot α) • α
• reflection_order_two (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → self.reflection α * self.reflection α = 1
• allRoots_neg_closed (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → -α ∈ self.allRoots
• reflection_neg (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → self.reflection (-α) = self.reflection α
• reflection_conjugation (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → ∀ β ∈ self.allRoots, self.reflection α * self.reflection β * self.reflection α = self.reflection (wg.dualAction (self.reflection α) β)
• allRoots_reflection_closed (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → ∀ β ∈ self.allRoots, wg.dualAction (self.reflection α) β ∈ self.allRoots
• dualAction_sub (w : wg.W) (μ ν : ↥Δ.𝔥 →ₗ[R] R) : wg.dualAction w (μ - ν) = wg.dualAction w μ - wg.dualAction w ν
• dualAction_zsmul (w : wg.W) (n : ℤ) (μ : ↥Δ.𝔥 →ₗ[R] R) : wg.dualAction w (n • μ) = n • wg.dualAction w μ
• dualAction_rootLattice (w : wg.W) (c : (↥Δ.𝔥 →ₗ[R] R) → ℤ) : ∃ (c' : (↥Δ.𝔥 →ₗ[R] R) → ℤ), wg.dualAction w (∑ α ∈ rd.posRoots, c α • α) = ∑ α ∈ rd.posRoots, c' α • α
• pairing_integral (α : ↥Δ.𝔥 →ₗ[R] R) : α ∈ self.allRoots → ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), (∃ (c : (↥Δ.𝔥 →ₗ[R] R) → ℤ), -μ (self.coroot α) • α = ∑ γ ∈ rd.posRoots, c γ • γ) → ∃ (n : ℤ), μ (self.coroot α) = ↑n
• generated_by_reflections (w : wg.W) : ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ self.allRoots) ∧ w = (List.ofFn fun (i : Fin n) => self.reflection (αs i)).prod
• ρ_eq_half_sum : 2 • wg.ρ = rd.sumPosRoots

theorem RootSystemWithReflections.stabilizer_gen_by_reflections {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg x) : ∃ (m : ℕ) (βs : Fin m → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin m), βs i ∈ rs.allRoots ∧ rs.reflection (βs i) ∈ WeylStabilizerModQ rd wg x) ∧ w = (List.ofFn fun (i : Fin m) => rs.reflection (βs i)).prod

theorem RootSystemWithReflections.dualAction_mul {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (_rs : RootSystemWithReflections rd wg) (w₁ w₂ : wg.W) (μ : ↥Δ.𝔥 →ₗ[R] R) : wg.dualAction (w₁ * w₂) μ = wg.dualAction w₁ (wg.dualAction w₂ μ)

def rootsOfStabilizer {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) : Set (↥Δ.𝔥 →ₗ[R] R)

def IsRootSubsystem {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (S : Set (↥Δ.𝔥 →ₗ[R] R)) : Prop

def corootsOf {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (rs : RootSystemWithReflections rd wg) (S : Set (↥Δ.𝔥 →ₗ[R] R)) : Set ↥Δ.𝔥

theorem WeylStabilizerModQ_mul_closed {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) {w₁ w₂ : wg.W} (h₁ : w₁ ∈ WeylStabilizerModQ rd wg x) (h₂ : w₂ ∈ WeylStabilizerModQ rd wg x) : w₁ * w₂ ∈ WeylStabilizerModQ rd wg x

theorem weyl_generated_by_root_reflections {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (w : wg.W) : ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rs.allRoots) ∧ w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod

theorem cst_stabilizer_generation_aux {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg x → ∀ (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rs.allRoots) → w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod → ∃ (m : ℕ) (βs : Fin m → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin m), βs i ∈ rs.allRoots ∧ rs.reflection (βs i) ∈ WeylStabilizerModQ rd wg x) ∧ w = (List.ofFn fun (i : Fin m) => rs.reflection (βs i)).prod

theorem cst_stabilizer_generation {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg x) : ∃ (m : ℕ) (βs : Fin m → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin m), βs i ∈ rs.allRoots ∧ rs.reflection (βs i) ∈ WeylStabilizerModQ rd wg x) ∧ w = (List.ofFn fun (i : Fin m) => rs.reflection (βs i)).prod

theorem cst_stabilizer_refine {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg x → ∀ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rs.allRoots) → w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod → ∃ (m : ℕ) (βs : Fin m → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin m), βs i ∈ rs.allRoots ∧ rs.reflection (βs i) ∈ WeylStabilizerModQ rd wg x) ∧ w = (List.ofFn fun (i : Fin m) => rs.reflection (βs i)).prod

theorem chevalley_shephard_todd_raw {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg x → ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rs.allRoots ∧ rs.reflection (αs i) ∈ WeylStabilizerModQ rd wg x) ∧ w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod

theorem chevalley_shephard_todd_stabilizer {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg x → ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rootsOfStabilizer rd wg rs x) ∧ w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod

theorem Wx_generated_by_reflections {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg x → ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rootsOfStabilizer rd wg rs x) ∧ w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod

theorem Wx_roots_form_root_system {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) : IsRootSubsystem rd wg rs (rootsOfStabilizer rd wg rs x)

theorem Wx_is_weyl_group_of_Rx {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) : (∀ w ∈ WeylStabilizerModQ rd wg x, ∃ (n : ℕ) (αs : Fin n → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin n), αs i ∈ rootsOfStabilizer rd wg rs x) ∧ w = (List.ofFn fun (i : Fin n) => rs.reflection (αs i)).prod) ∧ ∀ α ∈ rootsOfStabilizer rd wg rs x, rs.reflection α ∈ WeylStabilizerModQ rd wg x

theorem Rx_dual_is_root_subsystem {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (x : ↥Δ.𝔥 →ₗ[R] R) (h : ↥Δ.𝔥) : h ∈ corootsOf rs (rootsOfStabilizer rd wg rs x) ↔ h ∈ Submodule.span ℤ (corootsOf rs (rootsOfStabilizer rd wg rs x)) ∧ h ∈ corootsOf rs ↑rs.allRoots