def IsDominantWeightLE {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def IsDominantWeightBruhat {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem bruhatLE_implies_weightLE {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (μ wt : ↥Δ.𝔥 →ₗ[R] R) (h : BruhatLE rd μ wt) : WeightLE rd μ wt

theorem PositiveRootData.corootPairing_self_pos {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) : rd.corootPairing α α = 2

theorem WeylGroupData.hasReflection_element_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) : ∃ (s : wg.W), ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction s μ = μ - rd.corootPairing μ α • α

theorem WeylGroupData.hasReflection_element {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) : ∃ (s : wg.W), ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction s μ = μ - rd.corootPairing μ α • α

theorem reflection_in_stabilizerModQ_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (s : wg.W) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (hs : ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction s μ = μ - rd.corootPairing μ α • α) (lam : ↥Δ.𝔥 →ₗ[R] R) : s ∈ WeylStabilizerModQ rd wg lam

theorem WeylGroupData.reflection_preserves_stabilizerModQ {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (s : wg.W) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (hs : ∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction s μ = μ - rd.corootPairing μ α • α) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg lam → s * w ∈ WeylStabilizerModQ rd wg lam

theorem WeylGroupData.hasReflection {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) : ∃ (s : wg.W), (∀ (μ : ↥Δ.𝔥 →ₗ[R] R), wg.dualAction s μ = μ - rd.corootPairing μ α • α) ∧ ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), ∀ w ∈ WeylStabilizerModQ rd wg lam, s * w ∈ WeylStabilizerModQ rd wg lam

theorem descentRoot_coxeter_input {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (c : (↥Δ.𝔥 →ₗ[R] R) → ℕ) (hc : lam - wg.dualAction w lam = ∑ α ∈ rd.posRoots, c α • α) (hne : wg.dualAction w lam ≠ lam) : ∃ (α : ↥Δ.𝔥 →ₗ[R] R) (_ : α ∈ rd.posRoots) (n : ℕ), 0 < n ∧ rd.corootPairing (wg.dualAction w lam) α = -↑n ∧ n ≤ c α

theorem WeylGroupData.descentRoot {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (hle : WeightLE rd (wg.dualAction w lam) lam) (hne : wg.dualAction w lam ≠ lam) : ∃ (α : ↥Δ.𝔥 →ₗ[R] R) (_ : α ∈ rd.posRoots) (n : ℕ), 0 < n ∧ rd.corootPairing (wg.dualAction w lam) α = -↑n ∧ WeightLE rd (wg.dualAction w lam + n • α) lam

theorem bruhat_one_step_reduction {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (hle : WeightLE rd (wg.dualAction w lam) lam) (hne : wg.dualAction w lam ≠ lam) : ∃ w' ∈ WeylStabilizerModQ rd wg lam, WeightLE rd (wg.dualAction w' lam) lam ∧ ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α (wg.dualAction w lam) (wg.dualAction w' lam)

theorem weightLE_antisymm {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (a b : ↥Δ.𝔥 →ₗ[R] R) (h1 : WeightLE rd a b) (h2 : WeightLE rd b a) : a = b

theorem reflectionLT_ne {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (α μ ν : ↥Δ.𝔥 →ₗ[R] R) (h : ReflectionLT rd α μ ν) : μ ≠ ν

theorem reflectionLT_implies_weightLE {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (α μ ν : ↥Δ.𝔥 →ₗ[R] R) (h : ReflectionLT rd α μ ν) : WeightLE rd μ ν

theorem weightLE_trans {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (a b c : ↥Δ.𝔥 →ₗ[R] R) (h1 : WeightLE rd a b) (h2 : WeightLE rd b c) : WeightLE rd a c

theorem weightLE_refl {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (a : ↥Δ.𝔥 →ₗ[R] R) : WeightLE rd a a

theorem weightLE_implies_bruhatLE_in_orbit {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (hle : WeightLE rd (wg.dualAction w lam) lam) : BruhatLE rd (wg.dualAction w lam) lam

theorem dominantLE_implies_dominantBruhat {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (h : IsDominantWeightLE rd wg lam) : IsDominantWeightBruhat rd wg lam

theorem dominance_equivalence {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : IsDominantWeightLE rd wg lam ↔ IsDominantWeightBruhat rd wg lam

def NotNegIntCorootPairing {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def IsIntegralDominantWeightBruhat {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def IsIntegralDominantWeightLE {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem integralDominance_equivalence {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : IsIntegralDominantWeightBruhat rd wg lam ↔ IsIntegralDominantWeightLE rd wg lam

theorem coxeter_descent_root_exists {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (hne : wg.dualAction w lam ≠ lam) : ∃ (α : ↥Δ.𝔥 →ₗ[R] R) (_ : α ∈ rd.posRoots) (n : ℕ), 0 < n ∧ rd.corootPairing (wg.dualAction w lam) α = -↑n

theorem coxeter_orbit_ascent {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (hdom : IsDominantWeightLE rd wg lam) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (hne : wg.dualAction w lam ≠ lam) : ∃ w' ∈ WeylStabilizerModQ rd wg lam, ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α (wg.dualAction w lam) (wg.dualAction w' lam)

theorem dominantLE_implies_integralDominantLE {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (h : IsDominantWeightLE rd wg lam) : IsIntegralDominantWeightLE rd wg lam

theorem dominantBruhat_implies_integralDominantBruhat {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (h : IsDominantWeightBruhat rd wg lam) : IsIntegralDominantWeightBruhat rd wg lam

theorem neg_zsmul_posRoot_not_in_QPlus {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (n : ℤ) (hn : n < 0) : ¬rd.IsInQPlus (n • α)

theorem stabilizer_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 stabilizer_is_weyl_group {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 stabilizer_dual_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

theorem proposition_15_12 {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) ∧ IsRootSubsystem rd wg rs (rootsOfStabilizer rd wg rs x) ∧ ∀ (h : ↥Δ.𝔥), h ∈ corootsOf rs (rootsOfStabilizer rd wg rs x) ↔ h ∈ Submodule.span ℤ (corootsOf rs (rootsOfStabilizer rd wg rs x)) ∧ h ∈ corootsOf rs ↑rs.allRoots

theorem pairing_integral_of_WeylStabilizerModQ {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : w ∈ WeylStabilizerModQ rd wg lam) (α : ↥Δ.𝔥 →ₗ[R] R) (hα_pos : α ∈ rd.posRoots) (hs : rs.reflection α ∈ WeylStabilizerModQ rd wg lam) : ∃ (n : ℤ), (wg.dualAction w lam) (rs.coroot α) = ↑n

theorem exists_reduced_expression_positive_intermediates {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (k : ℕ) (αs : Fin k → ↥Δ.𝔥 →ₗ[R] R) (_hαs_root : ∀ (i : Fin k), αs i ∈ rs.allRoots) (_hαs_pos : ∀ (i : Fin k), αs i ∈ rd.posRoots) (P : (↥Δ.𝔥 →ₗ[R] R) → Prop) (_hαs_P : ∀ (i : Fin k), P (αs i)) : ∃ (m : ℕ) (βs : Fin m → ↥Δ.𝔥 →ₗ[R] R), (∀ (i : Fin m), βs i ∈ rs.allRoots) ∧ (∀ (i : Fin m), βs i ∈ rd.posRoots) ∧ (∀ (i : Fin m), P (βs i)) ∧ (List.ofFn fun (i : Fin m) => rs.reflection (βs i)).prod = (List.ofFn fun (i : Fin k) => rs.reflection (αs i)).prod ∧ ∀ (j : Fin m), wg.dualAction (List.ofFn fun (i : Fin ↑j) => rs.reflection (βs ⟨↑i, ⋯⟩)).prod (βs j) ∈ rd.posRoots

theorem IsInQPlus_add {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (μ ν : ↥Δ.𝔥 →ₗ[R] R) (hμ : rd.IsInQPlus μ) (hν : rd.IsInQPlus ν) : rd.IsInQPlus (μ + ν)

theorem nsmul_posRoot_IsInQPlus {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (β : ↥Δ.𝔥 →ₗ[R] R) (hβ : β ∈ rd.posRoots) (n : ℕ) : rd.IsInQPlus (n • β)

theorem notNegInt_implies_integralDominantLE {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (h : NotNegIntCorootPairing rd wg rs lam) : IsIntegralDominantWeightLE rd wg lam

theorem dominance_equivalence_full {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) : IsIntegralDominantWeightLE rd wg lam ↔ NotNegIntCorootPairing rd wg rs lam

theorem corollary_16_1 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) : (IsDominantWeightLE rd wg lam ↔ IsDominantWeightBruhat rd wg lam) ∧ (IsDominantWeightBruhat rd wg lam ↔ NotNegIntCorootPairing rd wg rs lam) ∧ (NotNegIntCorootPairing rd wg rs lam ↔ IsIntegralDominantWeightBruhat rd wg lam) ∧ (IsIntegralDominantWeightBruhat rd wg lam ↔ IsIntegralDominantWeightLE rd wg lam)

def IsProjectiveInO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (P : Type uCatO) [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hP : IsCategoryO Δ rd P) : Prop

theorem weight_decomp_component_eq {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] (_hMO : IsCategoryO Δ rd M) (μ : ↥Δ.𝔥 →ₗ[R] R) (v : M) (hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = μ h • v) (S : Finset (↥Δ.𝔥 →ₗ[R] R)) (y : (↥Δ.𝔥 →ₗ[R] R) → M) (hy_wt : ∀ (ν : ↥Δ.𝔥 →ₗ[R] R) (h : ↥Δ.𝔥), ⁅↑h, y ν⁆ = ν h • y ν) (hsum : v = ∑ ν ∈ S, y ν) : ∑ ν ∈ S with ν ≠ μ, y ν = 0

theorem weight_space_surjective_of_surjective {R : Type u_3} [Field 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) {Y : Type u_6} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔤 Y] [LieModule R 𝔤 Y] (_hYO : IsCategoryO Δ rd Y) (f : X →ₗ⁅R,𝔤⁆ Y) (_hf : Function.Surjective ⇑f) (μ : ↥Δ.𝔥 →ₗ[R] R) (v : Y) (hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = μ h • v) : ∃ (w : X), (∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = μ h • w) ∧ f w = v

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

theorem dominant_weight_vectors_are_singular {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] (μ : ↥Δ.𝔥 →ₗ[R] R) (w : X) (hw_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = μ h • w) (hμ_max : ∀ (ν : ↥Δ.𝔥 →ₗ[R] R) (v : X), (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = ν h • v) → rd.IsInQPlus (ν - μ) → ν ≠ μ → v = 0) (e : ↥Δ.𝔫_pos) : ⁅↑e, w⁆ = 0

theorem singular_vector_lift_in_O {R : Type u_3} [Field 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) {Y : Type u_6} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔤 Y] [LieModule R 𝔤 Y] (hYO : IsCategoryO Δ rd Y) (f : X →ₗ⁅R,𝔤⁆ Y) (hf : Function.Surjective ⇑f) (μ : ↥Δ.𝔥 →ₗ[R] R) (hμ_max : ∀ (ν : ↥Δ.𝔥 →ₗ[R] R) (v : X), (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = ν h • v) → rd.IsInQPlus (ν - μ) → ν ≠ μ → v = 0) (v : Y) (hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = μ h • v) (_hv_sing : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) : ∃ (w : X), (∀ (h : ↥Δ.𝔥), ⁅↑h, w⁆ = μ h • w) ∧ (∀ (e : ↥Δ.𝔫_pos), ⁅↑e, w⁆ = 0) ∧ f w = v

theorem IsInQPlus_antisymm_local {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

def IsInBlockO {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] (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem block_weight_bound_in_O {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (lam : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (_hMBlock : IsInBlockO Δ rd wg M lam) (ν : ↥Δ.𝔥 →ₗ[R] R) (v : M) (hv_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = ν h • v) (hv_ne : v ≠ 0) (hν_above : rd.IsInQPlus (ν - (lam - wg.ρ))) : ∃ w ∈ WeylStabilizerModQ rd wg lam, WeightLE rd ν (wg.dualAction w lam - wg.ρ)

theorem dominant_weight_is_maximal_in_O {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (lam : ↥Δ.𝔥 →ₗ[R] R) (hdom : IsDominantWeightLE rd wg lam) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hMBlock : IsInBlockO Δ rd wg M lam) (ν : ↥Δ.𝔥 →ₗ[R] R) (v : M) : (∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = ν h • v) → rd.IsInQPlus (ν - (lam - wg.ρ)) → ν ≠ lam - wg.ρ → v = 0

theorem surjection_source_in_block_of_verma_target {R : Type u_3} [Field R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hMO : IsCategoryO Δ rd M) {N : Type u_6} [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (_hNO : IsCategoryO Δ rd N) (f : M →ₗ⁅R,𝔤⁆ N) (_hf : Function.Surjective ⇑f) {Mlam : Type u_7} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (_g : Mlam →ₗ⁅R,𝔤⁆ N) (_hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) : IsInBlockO Δ rd wg M lam

theorem verma_projective_of_dominant_aux {R : Type u_3} [Field 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] (lam : ↥Δ.𝔥 →ₗ[R] R) (hdom : IsDominantWeightLE rd wg lam) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) (hO : IsCategoryO Δ rd Mlam) : IsProjectiveInO rd Mlam hO

theorem verma_projective_of_dominant {R : Type u_3} [Field 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] (lam : ↥Δ.𝔥 →ₗ[R] R) (hdom : IsDominantWeightLE rd wg lam) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) (hO : IsCategoryO Δ rd Mlam) : IsProjectiveInO rd Mlam hO

theorem tensorHom_adjunction_data {R : Type uCatO} [CommRing R] {𝔤 : Type uCatO} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] {V : Type uCatO} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Free R V] (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] (hNO : IsCategoryO Δ rd N) (f : M →ₗ⁅R,𝔤⁆ N) (hf : Function.Surjective ⇑f) (g : TensorProduct R V P →ₗ⁅R,𝔤⁆ N) : ∃ (W_M : Type uCatO) (x : AddCommGroup W_M) (x_1 : Module R W_M) (x_2 : LieRingModule 𝔤 W_M) (x_3 : LieModule R 𝔤 W_M) (_ : IsCategoryO Δ rd W_M) (W_N : Type uCatO) (x_4 : AddCommGroup W_N) (x_5 : Module R W_N) (x_6 : LieRingModule 𝔤 W_N) (x_7 : LieModule R 𝔤 W_N) (_ : IsCategoryO Δ rd W_N) (W_f : W_M →ₗ⁅R,𝔤⁆ W_N) (_ : Function.Surjective ⇑W_f) (g' : P →ₗ⁅R,𝔤⁆ W_N), ∀ (h' : P →ₗ⁅R,𝔤⁆ W_M), (∀ (p : P), W_f (h' p) = g' p) → ∃ (h : TensorProduct R V P →ₗ⁅R,𝔤⁆ M), ∀ (x : TensorProduct R V P), f (h x) = g x

theorem tensor_product_projective_in_O_of_projective {R : Type uCatO} [CommRing R] {𝔤 : Type uCatO} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) {V : Type uCatO} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Free R V] (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] (hNO : IsCategoryO Δ rd N) (f : M →ₗ⁅R,𝔤⁆ N) (hf : Function.Surjective ⇑f) (g : TensorProduct R V P →ₗ⁅R,𝔤⁆ N) : ∃ (h : TensorProduct R V P →ₗ⁅R,𝔤⁆ M), ∀ (x : TensorProduct R V P), f (h x) = g x

theorem tensor_projective_in_O_aux {R : Type uCatO} [CommRing R] {𝔤 : Type uCatO} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) {V : Type uCatO} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Free R V] {VP : Type uCatO} [AddCommGroup VP] [Module R VP] [LieRingModule 𝔤 VP] [LieModule R 𝔤 VP] (hVPO : IsCategoryO Δ rd VP) (tensor_iso : VP ≃ₗ⁅R,𝔤⁆ TensorProduct R V P) : IsProjectiveInO rd VP hVPO

theorem tensor_projective_in_O {R : Type uCatO} [CommRing R] {𝔤 : Type uCatO} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) {V : Type uCatO} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Free R V] {VP : Type uCatO} [AddCommGroup VP] [Module R VP] [LieRingModule 𝔤 VP] [LieModule R 𝔤 VP] (hVPO : IsCategoryO Δ rd VP) (tensor_iso : VP ≃ₗ⁅R,𝔤⁆ TensorProduct R V P) : IsProjectiveInO rd VP hVPO

theorem exists_dominant_shift_for_element {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (μ : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → WeightLE rd (wg.dualAction w (μ + (N + 1) • wg.ρ)) (μ + (N + 1) • wg.ρ)

theorem exists_dominant_shift {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (μ : ↥Δ.𝔥 →ₗ[R] R) : ∃ (N : ℕ), IsDominantWeightLE rd wg (μ + (N + 1) • wg.ρ)

theorem verma_module_isCategoryO {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] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hM : IsVermaModule Δ M wt) : IsCategoryO Δ rd M

structure LieModule.CompositionSeriesOf {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] : Type u_3

• length : ℕ
• series : Fin (self.length + 1) → LieSubmodule R 𝔤 M
• bot : self.series ⟨0, ⋯⟩ = ⊥
• top : self.series ⟨self.length, ⋯⟩ = ⊤
• strictly_increasing (i : Fin self.length) : self.series i.castSucc < self.series i.succ
• quotients_irreducible (i : Fin self.length) : IsIrreducible R 𝔤 (↥(self.series i.succ) ⧸ LieSubmodule.comap (self.series i.succ).incl (self.series i.castSucc))

theorem categoryO_isNoetherian' {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) : IsNoetherian R M

theorem categoryO_isArtinian {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) : IsArtinian R M

theorem lieModule_isIrreducible_of_covBy {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {A B : LieSubmodule R 𝔤 M} (hcov : A ⋖ B) : LieModule.IsIrreducible R 𝔤 (↥B ⧸ LieSubmodule.comap B.incl A)

theorem categoryO_has_composition_series {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) : Nonempty (LieModule.CompositionSeriesOf rd M)

@[implicit_reducible]

noncomputable instance prodLieRingModule {L' : Type u_4} [LieRing L'] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup M₁] [LieRingModule L' M₁] [AddCommGroup M₂] [LieRingModule L' M₂] : LieRingModule L' (M₁ × M₂)

instance prodLieModule {R' : Type u_3} [CommRing R'] {L' : Type u_4} [LieRing L'] [LieAlgebra R' L'] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup M₁] [Module R' M₁] [LieRingModule L' M₁] [LieModule R' L' M₁] [AddCommGroup M₂] [Module R' M₂] [LieRingModule L' M₂] [LieModule R' L' M₂] : LieModule R' L' (M₁ × M₂)

noncomputable def prodLieModuleHom {R' : Type u_3} [CommRing R'] {L' : Type u_4} [LieRing L'] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup M₁] [Module R' M₁] [LieRingModule L' M₁] [AddCommGroup M₂] [Module R' M₂] [LieRingModule L' M₂] {N' : Type u_7} [AddCommGroup N'] [Module R' N'] [LieRingModule L' N'] (f₁ : M₁ →ₗ⁅R',L'⁆ N') (f₂ : M₂ →ₗ⁅R',L'⁆ N') : M₁ × M₂ →ₗ⁅R',L'⁆ N'

@[simp]

theorem prodLieModuleHom_apply {R' : Type u_3} [CommRing R'] {L' : Type u_4} [LieRing L'] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup M₁] [Module R' M₁] [LieRingModule L' M₁] [AddCommGroup M₂] [Module R' M₂] [LieRingModule L' M₂] {N' : Type u_7} [AddCommGroup N'] [Module R' N'] [LieRingModule L' N'] (f₁ : M₁ →ₗ⁅R',L'⁆ N') (f₂ : M₂ →ₗ⁅R',L'⁆ N') (m : M₁ × M₂) : (prodLieModuleHom f₁ f₂) m = f₁ m.1 + f₂ m.2

theorem IsProjectiveInO_prod {R' : Type uCatO} [CommRing R'] {𝔤' : Type uCatO} [LieRing 𝔤'] [LieAlgebra R' 𝔤'] {Δ : TriangularDecomposition R' 𝔤'} {rd : PositiveRootData Δ} {P₁ : Type uCatO} [AddCommGroup P₁] [Module R' P₁] [LieRingModule 𝔤' P₁] [LieModule R' 𝔤' P₁] {P₂ : Type uCatO} [AddCommGroup P₂] [Module R' P₂] [LieRingModule 𝔤' P₂] [LieModule R' 𝔤' P₂] {hP₁O : IsCategoryO Δ rd P₁} {hP₂O : IsCategoryO Δ rd P₂} (hP₁ : IsProjectiveInO rd P₁ hP₁O) (hP₂ : IsProjectiveInO rd P₂ hP₂O) (hProdO : IsCategoryO Δ rd (P₁ × P₂)) : IsProjectiveInO rd (P₁ × P₂) hProdO

theorem IsCategoryO_prod {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₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module R' M₂] [LieRingModule 𝔤' M₂] [LieModule R' 𝔤' M₂] (_hM₁ : IsCategoryO Δ rd M₁) (_hM₂ : IsCategoryO Δ rd M₂) : IsCategoryO Δ rd (M₁ × M₂)

theorem corollary_16_6_i_hom_nonvanishing {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (μ lam : ↥Δ.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) (VP : Type u_5) [AddCommGroup VP] [Module R VP] [LieRingModule 𝔤 VP] [LieModule R 𝔤 VP] (_hVPO : IsCategoryO Δ rd VP) (_htensor : True) (Lμ : Type u_6) [AddCommGroup Lμ] [Module R Lμ] [LieRingModule 𝔤 Lμ] [LieModule R 𝔤 Lμ] (_hLμ : IsHighestWeightModule Δ Lμ μ) (_hLμO : IsCategoryO Δ rd Lμ) : ∃ (f : VP →ₗ⁅R,𝔤⁆ Lμ), f ≠ 0

theorem corollary_16_6_i_construction {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (μ lam : ↥Δ.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) : ∃ (V : Type u_V) (x : AddCommGroup V) (x_1 : Module R V) (x_2 : LieRingModule 𝔤 V) (_ : LieModule R 𝔤 V) (_ : Module.Finite R V) (Mlam : Type u_M) (x : AddCommGroup Mlam) (x_4 : Module R Mlam) (x_5 : LieRingModule 𝔤 Mlam) (x_6 : LieModule R 𝔤 Mlam) (x : IsVermaModule Δ Mlam (lam - wg.ρ)) (VP : Type u_P) (x : AddCommGroup VP) (x_7 : Module R VP) (x_8 : LieRingModule 𝔤 VP) (x_9 : LieModule R 𝔤 VP) (hVPO : IsCategoryO Δ rd VP), IsProjectiveInO rd VP hVPO ∧ ∀ (Lμ : Type u_5) [inst : AddCommGroup Lμ] [inst_1 : Module R Lμ] [inst_2 : LieRingModule 𝔤 Lμ] [inst_3 : LieModule R 𝔤 Lμ] (a : IsHighestWeightModule Δ Lμ μ), IsCategoryO Δ rd Lμ → ∃ (f : VP →ₗ⁅R,𝔤⁆ Lμ), f ≠ 0

theorem categoryO_enough_projectives_aux {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] (hM : IsCategoryO Δ rd M) : ∃ (P : Type u_6) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔤 P) (x_3 : LieModule R 𝔤 P) (hPO : IsCategoryO Δ rd P), IsProjectiveInO rd P hPO ∧ ∃ (f : P →ₗ⁅R,𝔤⁆ M), Function.Surjective ⇑f

theorem corollary_16_6_i {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} (μ : ↥Δ.𝔥 →ₗ[R] R) : ∃ (lam : ↥Δ.𝔥 →ₗ[R] R), IsDominantWeightLE rd wg lam ∧ ∃ (V : Type u_V) (x : AddCommGroup V) (x_1 : Module R V) (x_2 : LieRingModule 𝔤 V) (_ : LieModule R 𝔤 V) (_ : Module.Finite R V) (Mlam : Type u_M) (x : AddCommGroup Mlam) (x_4 : Module R Mlam) (x_5 : LieRingModule 𝔤 Mlam) (x_6 : LieModule R 𝔤 Mlam) (x : IsVermaModule Δ Mlam (lam - wg.ρ)) (VP : Type u_P) (x : AddCommGroup VP) (x_7 : Module R VP) (x_8 : LieRingModule 𝔤 VP) (x_9 : LieModule R 𝔤 VP) (hVPO : IsCategoryO Δ rd VP), IsProjectiveInO rd VP hVPO ∧ ∀ (Lμ : Type u_5) [inst : AddCommGroup Lμ] [inst_1 : Module R Lμ] [inst_2 : LieRingModule 𝔤 Lμ] [inst_3 : LieModule R 𝔤 Lμ] (a : IsHighestWeightModule Δ Lμ μ), IsCategoryO Δ rd Lμ → ∃ (f : VP →ₗ⁅R,𝔤⁆ Lμ), f ≠ 0

theorem categoryO_enough_projectives {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : ∃ (P : Type u_4) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔤 P) (x_3 : LieModule R 𝔤 P) (hPO : IsCategoryO Δ rd P), IsProjectiveInO rd P hPO ∧ ∃ (f : P →ₗ⁅R,𝔤⁆ M), Function.Surjective ⇑f

theorem indecomposable_projective_infrastructure {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : Nontrivial P ∧ IsNoetherian R P ∧ ∀ (Q₁ Q₂ : LieSubmodule R 𝔤 P), Q₁ ≠ ⊤ → Q₂ ≠ ⊤ → Q₁ ⊔ Q₂ ≠ ⊤

theorem indecomposable_projective_nontrivial {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) (_hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : Nontrivial P

theorem proper_join_of_indecomposable_projective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) (_hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) (Q₁ Q₂ : LieSubmodule R 𝔤 P) (_hQ₁ : Q₁ ≠ ⊤) (_hQ₂ : Q₂ ≠ ⊤) : Q₁ ⊔ Q₂ ≠ ⊤

theorem categoryO_isNoetherian {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) : IsNoetherian R P

theorem indecomposable_projective_has_greatest_proper_submodule {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : ∃ (J : LieSubmodule R 𝔤 P), J ≠ ⊤ ∧ ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J

theorem projective_cover_unique_simple_quotient_aux {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : ∃ (J : LieSubmodule R 𝔤 P), J ≠ ⊤ ∧ (∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) ∧ LieModule.IsIrreducible R 𝔤 (P ⧸ J)

theorem projective_cover_unique_simple_quotient {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_3} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : ∃ (J : LieSubmodule R 𝔤 P), J ≠ ⊤ ∧ (∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) ∧ LieModule.IsIrreducible R 𝔤 (P ⧸ J)

theorem projective_hom_finiteDimensional {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : Module.Finite R (P →ₗ⁅R,𝔤⁆ M)

theorem CategoryO.block_decomposition_with_characters {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsNoetherianRing R] {Δ : TriangularDecomposition R 𝔤} [Module.Free R ↥Δ.𝔥] [Module.Finite R ↥Δ.𝔥] {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd 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 ((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 M)) (chis i)

noncomputable def LieModule.CompositionSeriesOf.countFactorsIso {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] (cs : CompositionSeriesOf rd M) (L : Type u_4) [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] : ℕ

theorem jordanHolder_composition_multiplicity_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) (L : Type u_6) [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] (_hL : LieModule.IsIrreducible R 𝔤 L) : cs₁.countFactorsIso L = cs₂.countFactorsIso L

noncomputable def compositionMultiplicityOfModule {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) (L : Type u_6) [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] (_hL : LieModule.IsIrreducible R 𝔤 L) : ℕ

noncomputable def quotTopBotLieModuleEquiv {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {L : Type u_3} [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] : ↥⊤ ⧸ LieSubmodule.comap ⊤.incl ⊥ ≃ₗ⁅R,𝔤⁆ L

theorem schur_lie_module_noniso_zero {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M₁ : Type u_5} [AddCommGroup M₁] [Module R M₁] [LieRingModule 𝔤 M₁] [LieModule R 𝔤 M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module R M₂] [LieRingModule 𝔤 M₂] [LieModule R 𝔤 M₂] (_h1 : LieModule.IsIrreducible R 𝔤 M₁) (_h2 : LieModule.IsIrreducible R 𝔤 M₂) (_hne : ¬Nonempty (M₁ ≃ₗ⁅R,𝔤⁆ M₂)) : Module.finrank R (M₁ →ₗ⁅R,𝔤⁆ M₂) = 0

theorem lie_endo_is_scalar {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hirr : LieModule.IsIrreducible R 𝔤 M) [FiniteDimensional R M] (f : M →ₗ⁅R,𝔤⁆ M) : ∃ (c : R), f = c • LieModuleHom.id

theorem schur_lie_module_iso_one {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M₁ : Type u_5} [AddCommGroup M₁] [Module R M₁] [LieRingModule 𝔤 M₁] [LieModule R 𝔤 M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module R M₂] [LieRingModule 𝔤 M₂] [LieModule R 𝔤 M₂] (_h1 : LieModule.IsIrreducible R 𝔤 M₁) (_h2 : LieModule.IsIrreducible R 𝔤 M₂) (_hiso : Nonempty (M₁ ≃ₗ⁅R,𝔤⁆ M₂)) [FiniteDimensional R M₁] : Module.finrank R (M₁ →ₗ⁅R,𝔤⁆ M₂) = 1

theorem radical_le_ker_of_hom_to_simple {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] {L : Type u_6} [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] (hL_simple : LieModule.IsIrreducible R 𝔤 L) {J : LieSubmodule R 𝔤 P} (hJ_proper : J ≠ ⊤) (hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (f : P →ₗ⁅R,𝔤⁆ L) : J ≤ f.ker

noncomputable def LieModuleHom.liftQ {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] {L : Type u_6} [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] {J : LieSubmodule R 𝔤 P} (f : P →ₗ⁅R,𝔤⁆ L) (h : J ≤ f.ker) : P ⧸ J →ₗ⁅R,𝔤⁆ L

noncomputable def homEquivThroughQuotient {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] {L : Type u_6} [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] {J : LieSubmodule R 𝔤 P} (hfact : ∀ (f : P →ₗ⁅R,𝔤⁆ L), J ≤ f.ker) : (P ⧸ J →ₗ⁅R,𝔤⁆ L) ≃ₗ[R] P →ₗ⁅R,𝔤⁆ L

theorem projective_hom_simple_kronecker_delta {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] {J : LieSubmodule R 𝔤 P} (hJ_proper : J ≠ ⊤) (hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) [FiniteDimensional R (P ⧸ J)] {L : Type u_6} [AddCommGroup L] [Module R L] [LieRingModule 𝔤 L] [LieModule R 𝔤 L] (hL_simple : LieModule.IsIrreducible R 𝔤 L) : (Nonempty (L ≃ₗ⁅R,𝔤⁆ P ⧸ J) → Module.finrank R (P →ₗ⁅R,𝔤⁆ L) = 1) ∧ (¬Nonempty (L ≃ₗ⁅R,𝔤⁆ P ⧸ J) → Module.finrank R (P →ₗ⁅R,𝔤⁆ L) = 0)

theorem hom_fin_and_finrank_additive_over_composition_series {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (cs : LieModule.CompositionSeriesOf rd M) : Module.Finite R (P →ₗ⁅R,𝔤⁆ M) ∧ Module.finrank R (P →ₗ⁅R,𝔤⁆ M) = ∑ i : Fin cs.length, Module.finrank R (P →ₗ⁅R,𝔤⁆ ↥(cs.series i.succ) ⧸ LieSubmodule.comap (cs.series i.succ).incl (cs.series i.castSucc))

theorem hom_finrank_additive_over_composition_series {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (cs : LieModule.CompositionSeriesOf rd M) : Module.finrank R (P →ₗ⁅R,𝔤⁆ M) = ∑ i : Fin cs.length, Module.finrank R (P →ₗ⁅R,𝔤⁆ ↥(cs.series i.succ) ⧸ LieSubmodule.comap (cs.series i.succ).incl (cs.series i.castSucc))

theorem compositionFactor_isCategoryO {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) (cs : LieModule.CompositionSeriesOf rd M) (i : Fin cs.length) : IsCategoryO Δ rd (↥(cs.series i.succ) ⧸ LieSubmodule.comap (cs.series i.succ).incl (cs.series i.castSucc))

theorem irreducible_in_categoryO_finiteDimensional {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] (_hMO : IsCategoryO Δ rd M) (_hM_irr : LieModule.IsIrreducible R 𝔤 M) : FiniteDimensional R M

theorem compositionFactor_finiteDimensional {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) (cs : LieModule.CompositionSeriesOf rd M) (i : Fin cs.length) : FiniteDimensional R (↥(cs.series i.succ) ⧸ LieSubmodule.comap (cs.series i.succ).incl (cs.series i.castSucc))

theorem quotient_by_radical_finiteDimensional {R : Type u_3} [Field R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) {J : LieSubmodule R 𝔤 P} (_hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) : FiniteDimensional R (P ⧸ J)

theorem hom_finrank_eq_countFactorsIso_of_projective {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) (_hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) {J : LieSubmodule R 𝔤 P} (_hJ_proper : J ≠ ⊤) (_hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (_hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (_hMO : IsCategoryO Δ rd M) (cs : LieModule.CompositionSeriesOf rd M) : Module.finrank R (P →ₗ⁅R,𝔤⁆ M) = cs.countFactorsIso (P ⧸ J)

theorem multiplicity_eq_hom_dim {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) {J : LieSubmodule R 𝔤 P} (hJ_proper : J ≠ ⊤) (hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) {M : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hMO : IsCategoryO Δ rd M) : compositionMultiplicityOfModule M hMO (P ⧸ J) hPJ_irr = Module.finrank R (P →ₗ⁅R,𝔤⁆ M)

theorem proposition_16_2 {R : Type u_3} [Field R] [IsAlgClosed R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {P : Type u_5} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hindec : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : (∃ (J : LieSubmodule R 𝔤 P), J ≠ ⊤ ∧ (∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) ∧ LieModule.IsIrreducible R 𝔤 (P ⧸ J) ∧ ∀ {L : Type u_6} [inst : AddCommGroup L] [inst_1 : Module R L] [inst_2 : LieRingModule 𝔤 L] [inst_3 : LieModule R 𝔤 L], LieModule.IsIrreducible R 𝔤 L → ∀ [FiniteDimensional R (P ⧸ J)], (Nonempty (L ≃ₗ⁅R,𝔤⁆ P ⧸ J) → Module.finrank R (P →ₗ⁅R,𝔤⁆ L) = 1) ∧ (¬Nonempty (L ≃ₗ⁅R,𝔤⁆ P ⧸ J) → Module.finrank R (P →ₗ⁅R,𝔤⁆ L) = 0)) ∧ ∃ (J : LieSubmodule R 𝔤 P) (_ : J ≠ ⊤) (_ : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)), ∀ {M : Type u_7} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : LieRingModule 𝔤 M] [inst_3 : LieModule R 𝔤 M] (hMO : IsCategoryO Δ rd M), compositionMultiplicityOfModule M hMO (P ⧸ J) hPJ_irr = Module.finrank R (P →ₗ⁅R,𝔤⁆ M)