Atlas.LieGroups.code.CompositionSeries

source

structure LieModule.CompositionSeries (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] :

Type u_5

length : ℕ
series : Fin (self.length + 1) → LieSubmodule R 𝔤 M
bot : self.series ⟨0, ⋯⟩ = ⊥
top : self.series ⟨self.length, ⋯⟩ = ⊤
strictly_mono (i : Fin self.length) : self.series i.castSucc < self.series i.succ

Instances For

source

noncomputable def jordanHolder_compMult_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (_wg : WeylGroupData Δ) :

(↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ

Instances For

source

theorem compositionMultiplicity_quotient_maximal_eq_one {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] (hCatO : IsCategoryO Δ rd M) {J : LieSubmodule R 𝔤 M} (hJ_ne_top : J ≠ ⊤) (hJ_max : ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ J) (hIrr : LieModule.IsIrreducible R 𝔤 (M ⧸ J)) :

compositionMultiplicityOfModule M hCatO (M ⧸ J) hIrr = 1

source

theorem jordanHolder_compMult_diag (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) :

jordanHolder_compMult_raw R 𝔤 Δ rd wg lam lam = 1

source

theorem jantzen_radical_compMult_bound (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hne : lam ≠ mu) :

jordanHolder_compMult_raw R 𝔤 Δ rd wg lam mu ≤ ∑ α ∈ rd.posRoots, jordanHolder_compMult_raw R 𝔤 Δ rd wg (lam - rd.corootPairing lam α • α) mu

source

theorem jantzen_integrality_of_descent (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rd.posRoots) (hne : lam ≠ mu) (hd : jordanHolder_compMult_raw R 𝔤 Δ rd wg (lam - rd.corootPairing lam α • α) mu ≠ 0) :

∃ (n : ℕ), 0 < n ∧ rd.corootPairing lam α = ↑n

source

theorem jantzen_comp_factor_descent (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hne : lam ≠ mu) (hd : jordanHolder_compMult_raw R 𝔤 Δ rd wg lam mu ≠ 0) :

∃ (α : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ), α ∈ rd.posRoots ∧ 0 < n ∧ rd.corootPairing lam α = ↑n ∧ jordanHolder_compMult_raw R 𝔤 Δ rd wg (lam - n • α) mu ≠ 0

source

theorem bgg_qplus (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

jordanHolder_compMult_raw R 𝔤 Δ rd wg lam mu ≠ 0 → rd.IsInQPlus (lam - mu)

source

theorem bgg_induction_measure (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

∃ (m : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ), (∀ (lam : ↥Δ.𝔥 →ₗ[R] R), m lam lam = 0) ∧ ∀ (lam mu α : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ), α ∈ rd.posRoots → 0 < n → rd.corootPairing lam α = ↑n → jordanHolder_compMult_raw R 𝔤 Δ rd wg (lam - n • α) mu ≠ 0 → m (lam - n • α) mu < m lam mu

source

theorem bgg_jantzen_step (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hne : lam ≠ mu) (hd : jordanHolder_compMult_raw R 𝔤 Δ rd wg lam mu ≠ 0) :

∃ (α : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ), α ∈ rd.posRoots ∧ 0 < n ∧ rd.corootPairing lam α = ↑n ∧ jordanHolder_compMult_raw R 𝔤 Δ rd wg (lam - n • α) mu ≠ 0 ∧ BruhatLE rd mu (lam - n • α)

source

theorem jordanHolder_compMult_bruhat (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

jordanHolder_compMult_raw R 𝔤 Δ rd wg lam mu ≠ 0 → BruhatLE rd mu lam

source

theorem stdFiltMult_exists (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

∃ (d : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ), ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), d lam lam = 1

source

noncomputable def standardFiltration_stdMult_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

(↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ

Instances For

source

theorem prop_16_2_ii_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

jordanHolder_compMult_raw R 𝔤 Δ rd wg mu lam = standardFiltration_stdMult_raw R 𝔤 Δ rd wg lam mu

source

theorem standardFiltration_stdMult_bgg_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

standardFiltration_stdMult_raw R 𝔤 Δ rd wg lam mu = jordanHolder_compMult_raw R 𝔤 Δ rd wg mu lam

source

theorem standardFiltration_stdMult_diag (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) :

standardFiltration_stdMult_raw R 𝔤 Δ rd wg lam lam = 1

source

theorem jordanHolder_multiplicity_exists (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

∃ (compMult : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ), (∀ (lam : ↥Δ.𝔥 →ₗ[R] R), compMult lam lam = 1) ∧ ∀ (lam mu : ↥Δ.𝔥 →ₗ[R] R), compMult lam mu ≠ 0 → BruhatLE rd mu lam

source

theorem standardFiltration_multiplicity_exists (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

∃ (stdMult : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ), ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), stdMult lam lam = 1

source

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

ℕ

Instances For

source

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

ℕ

Instances For

source

noncomputable def dimHomProjectiveContragredientVerma (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

ℕ

Instances For

source

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

standardFiltrationMultiplicity rd wg lam mu = dimHomProjectiveContragredientVerma R 𝔤 Δ rd wg lam mu

source

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

compositionMultiplicity rd wg mu lam = dimHomProjectiveContragredientVerma R 𝔤 Δ rd wg lam mu

source

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

standardFiltrationMultiplicity rd wg lam mu = compositionMultiplicity rd wg mu lam

source

theorem compositionMultiplicity_finiteSupport (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) :

∃ (S : Finset (↥Δ.𝔥 →ₗ[R] R)), lam ∈ S ∧ ∀ nu ∉ S, jordanHolder_compMult_raw R 𝔤 Δ rd wg nu lam = 0

source

noncomputable def projectiveCoverCompMult_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) :

(↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → ℕ

Instances For

source

theorem projectiveCoverCompMult_diag_pos (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) :

0 < projectiveCoverCompMult_raw R 𝔤 Δ rd wg lam lam

source

theorem standard_filtration_additivity_raw (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [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) :

projectiveCoverCompMult_raw R 𝔤 Δ rd wg lam mu = ∑ nu ∈ S, standardFiltrationMultiplicity rd wg lam nu * compositionMultiplicity rd wg nu mu

source

theorem bgg_theorem_bruhat_order (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (h : compositionMultiplicity rd wg lam mu ≠ 0) :

BruhatLE rd mu lam

source

noncomputable def cartanMultiplicity {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) :

ℕ

Instances For

source

theorem corollary_20_7 {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [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) :

cartanMultiplicity rd wg lam mu = ∑ nu ∈ S, compositionMultiplicity rd wg nu lam * compositionMultiplicity rd wg nu mu

source

theorem HasWeightDecomposition_lieSubmodule_local {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) :

HasWeightDecomposition Δ ↥Z

source

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

source

theorem weightSpace_quotient_vanish_of_vanish {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) (μ : ↥Δ.𝔥 →ₗ[R] R) (hμ : WeightSpace Δ X μ = ⊥) :

WeightSpace Δ (X ⧸ Z) μ = ⊥

source

theorem IsCategoryO_quotient_commRing_local {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 (X ⧸ Z)

source

theorem composition_factor_in_O {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) (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))

source

theorem verma_composition_factor_bruhat_bound {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] (lam : ↥Δ.𝔥 →ₗ[R] R) (_hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) (hMO : IsCategoryO Δ rd Mlam) (cs : LieModule.CompositionSeriesOf rd Mlam) (i : Fin cs.length) (mu : ↥Δ.𝔥 →ₗ[R] R) (_hmu : Nonempty (IsHighestWeightModule Δ (↥(cs.series i.succ) ⧸ LieSubmodule.comap (cs.series i.succ).incl (cs.series i.castSucc)) (mu - wg.ρ))) :

BruhatLE rd mu lam