Atlas.LieGroups.code.DufloJoseph

source

noncomputable def evalHC {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

(↥Δ.𝔥 →ₗ[R] R) → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R

Instances For

source

def adjointActionOnHom {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (x : 𝔤) (T : M →ₗ[R] N) :

M →ₗ[R] N

Instances For

source

def IsFiniteTypeMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (T : M →ₗ[R] N) :

Prop

Instances For

source

def HomFin {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] :

Submodule R (M →ₗ[R] N)

Instances For

source

def homLeftComp {R : Type u_1} [CommRing R] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :

Module.End R N →ₐ[R] Module.End R (M →ₗ[R] N)

Instances For

source

def homRightComp {R : Type u_1} [CommRing R] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] :

(Module.End R M)ᵐᵒᵖ →ₐ[R] Module.End R (M →ₗ[R] N)

Instances For

source

def HomBimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] :

LieBimodule R 𝔤

Instances For

source

theorem UniversalEnvelopingAlgebra.induction {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {motive : UniversalEnvelopingAlgebra R 𝔤 → Prop} (halg : ∀ (r : R), motive ((algebraMap R (UniversalEnvelopingAlgebra R 𝔤)) r)) (hι : ∀ (x : 𝔤), motive ((ι R) x)) (hmul : ∀ (a b : UniversalEnvelopingAlgebra R 𝔤), motive a → motive b → motive (a * b)) (hadd : ∀ (a b : UniversalEnvelopingAlgebra R 𝔤), motive a → motive b → motive (a + b)) (u : UniversalEnvelopingAlgebra R 𝔤) :

motive u

source

theorem uea_ad_leibniz {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (x : 𝔤) (a b : UniversalEnvelopingAlgebra R 𝔤) :

(UniversalEnvelopingAlgebra.ι R) x * (a * b) - a * b * (UniversalEnvelopingAlgebra.ι R) x = ((UniversalEnvelopingAlgebra.ι R) x * a - a * (UniversalEnvelopingAlgebra.ι R) x) * b + a * ((UniversalEnvelopingAlgebra.ι R) x * b - b * (UniversalEnvelopingAlgebra.ι R) x)

source

theorem uea_ad_add {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (x : 𝔤) (v₁ v₂ : UniversalEnvelopingAlgebra R 𝔤) :

(UniversalEnvelopingAlgebra.ι R) x * (v₁ + v₂) - (v₁ + v₂) * (UniversalEnvelopingAlgebra.ι R) x = (UniversalEnvelopingAlgebra.ι R) x * v₁ - v₁ * (UniversalEnvelopingAlgebra.ι R) x + ((UniversalEnvelopingAlgebra.ι R) x * v₂ - v₂ * (UniversalEnvelopingAlgebra.ι R) x)

source

theorem uea_comm_rel {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (x y : 𝔤) :

(UniversalEnvelopingAlgebra.ι R) x * (UniversalEnvelopingAlgebra.ι R) y - (UniversalEnvelopingAlgebra.ι R) y * (UniversalEnvelopingAlgebra.ι R) x = (UniversalEnvelopingAlgebra.ι R) ⁅x, y⁆

source

def ueaIotaRange {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] :

Submodule R (UniversalEnvelopingAlgebra R 𝔤)

Instances For

source

def ueaScalarsSubmodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] :

Submodule R (UniversalEnvelopingAlgebra R 𝔤)

Instances For

source

theorem ueaScalarsSubmodule_fg {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] :

ueaScalarsSubmodule.FG

source

theorem ueaIotaRange_fg {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] :

ueaIotaRange.FG

source

theorem ueaAdLocallyFinite {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (u : UniversalEnvelopingAlgebra R 𝔤) :

∃ (S : Submodule R (UniversalEnvelopingAlgebra R 𝔤)), Module.Finite R ↥S ∧ u ∈ S ∧ ∀ (x : 𝔤), ∀ v ∈ S, (UniversalEnvelopingAlgebra.ι R) x * v - v * (UniversalEnvelopingAlgebra.ι R) x ∈ S

source

theorem ueaAction_adjoint_intertwine {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (act : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (act ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (x : 𝔤) (u : UniversalEnvelopingAlgebra R 𝔤) :

adjointActionOnHom M M x (act u) = act ((UniversalEnvelopingAlgebra.ι R) x * u - u * (UniversalEnvelopingAlgebra.ι R) x)

source

theorem adjointActionOnHom_left_comp {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (x : 𝔤) (f : N →ₗ[R] N) (T : M →ₗ[R] N) :

adjointActionOnHom M N x (f ∘ₗ T) = adjointActionOnHom N N x f ∘ₗ T + f ∘ₗ adjointActionOnHom M N x T

source

theorem adjointActionOnHom_right_comp {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (x : 𝔤) (T : M →ₗ[R] N) (g : M →ₗ[R] M) :

adjointActionOnHom M N x (T ∘ₗ g) = adjointActionOnHom M N x T ∘ₗ g + T ∘ₗ adjointActionOnHom M M x g

source

theorem ueaAction_preserves_HomFin {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (u : UniversalEnvelopingAlgebra R 𝔤) (T : M →ₗ[R] N) (hT : T ∈ HomFin M N) :

((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 N)) u ∘ₗ T ∈ HomFin M N ∧ T ∘ₗ ((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 M)) u ∈ HomFin M N

source

theorem leftAction_preserves_HomFin {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (u : UniversalEnvelopingAlgebra R 𝔤) (T : M →ₗ[R] N) (hT : T ∈ HomFin M N) :

((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 N)) u ∘ₗ T ∈ HomFin M N

source

theorem rightAction_preserves_HomFin {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (u : UniversalEnvelopingAlgebra R 𝔤) (T : M →ₗ[R] N) (hT : T ∈ HomFin M N) :

T ∘ₗ ((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 M)) u ∈ HomFin M N

source

def HomFinBimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] :

LieBimodule R 𝔤

Instances For

source

theorem exercise_8_13_hom_locally_finite_verma {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] (wtM : ↥Δ.𝔥 →ₗ[R] R) (hM : IsVermaModule Δ M wtM) (N : Type u_6) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (wtN : ↥Δ.𝔥 →ₗ[R] R) (hN : IsVermaModule Δ N wtN) (T : M →ₗ[R] N) :

∃ (S : Submodule R (M →ₗ[R] N)), Module.Finite R ↥S ∧ T ∈ S ∧ ∀ (x : 𝔤), ∀ f ∈ S, adjointActionOnHom M N x f ∈ S

source

theorem exercise_8_13_hom_admissible_verma {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wtM : ↥Δ.𝔥 →ₗ[R] R) (hM : IsVermaModule Δ M wtM) (N : Type u_6) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (wtN : ↥Δ.𝔥 →ₗ[R] R) (hN : IsVermaModule Δ N wtN) (V : Type u_7) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [LieModule.IsIrreducible R 𝔤 V] :

Module.Finite R ↥(HomAdEquivariant V (HomFinBimodule M N))

source

theorem catO_hom_equivariant_injection_into_verma {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_5) (N : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) :

source

theorem catO_hom_bimodule_injection_into_verma {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_5) (N : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) :

∃ (M' : Type) (N' : Type) (x : AddCommGroup M') (x_1 : Module R M') (x_2 : LieRingModule 𝔤 M') (x_3 : LieModule R 𝔤 M') (x_4 : AddCommGroup N') (x_5 : Module R N') (x_6 : LieRingModule 𝔤 N') (x_7 : LieModule R 𝔤 N') (wtM : ↥Δ.𝔥 →ₗ[R] R) (hVM : IsVermaModule Δ M' wtM) (wtN : ↥Δ.𝔥 →ₗ[R] R) (hVN : IsVermaModule Δ N' wtN) (ι : (HomFinBimodule M N).carrier →ₗ[R] (HomFinBimodule M' N').carrier), Function.Injective ⇑ι ∧ (∀ (u : UniversalEnvelopingAlgebra R 𝔤) (m : (HomFinBimodule M N).carrier), ι (((HomFinBimodule M N).leftAction u) m) = ((HomFinBimodule M' N').leftAction u) (ι m)) ∧ ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (m : (HomFinBimodule M N).carrier), ι (((HomFinBimodule M N).rightAction u) m) = ((HomFinBimodule M' N').rightAction u) (ι m)

source

theorem hom_locally_finite_catO {R : Type u_3} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_5) (N : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) (T : M →ₗ[R] N) :

∃ (S : Submodule R (M →ₗ[R] N)), Module.Finite R ↥S ∧ T ∈ S ∧ ∀ (x : 𝔤), ∀ f ∈ S, adjointActionOnHom M N x f ∈ S

source

theorem HomAdEquivariant.finite_of_injection {R : Type u_3} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {V : Type u_5} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] {M : LieBimodule R 𝔤} {N : LieBimodule R 𝔤} (ι : M.carrier →ₗ[R] N.carrier) (hι_inj : Function.Injective ⇑ι) (hι_left : ∀ (u : UniversalEnvelopingAlgebra R 𝔤) (m : M.carrier), ι ((M.leftAction u) m) = (N.leftAction u) (ι m)) (hι_right : ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (m : M.carrier), ι ((M.rightAction u) m) = (N.rightAction u) (ι m)) (hN_fin : Module.Finite R ↥(HomAdEquivariant V N)) :

Module.Finite R ↥(HomAdEquivariant V M)

source

theorem hom_admissible_catO {R : Type u_3} [CommRing R] [IsNoetherianRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_5) (N : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) (V : Type u_7) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [LieModule.IsIrreducible R 𝔤 V] :

Module.Finite R ↥(HomAdEquivariant V (HomFinBimodule M N))

source

theorem homFinBimodule_adjointAction_val {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (x : 𝔤) (T : ↥(HomFin M N)) :

↑(((HomFinBimodule M N).adjointAction x) T) = adjointActionOnHom M N x ↑T

source

theorem proposition_18_2 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] [IsNoetherianRing R] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_3) (N : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) :

IsAdmissibleBimodule (HomFinBimodule M N)

source

theorem postcomp_tensor_finiteType_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_5} {N : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] {V : Type u_7} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] {VN : Type u_8} [AddCommGroup VN] [Module R VN] [LieRingModule 𝔤 VN] [LieModule R 𝔤 VN] (tensor_VN : V →ₗ[R] N →ₗ[R] VN) (hiso_VN : Function.Bijective ⇑(TensorProduct.lift tensor_VN)) (v : V) (f : ↥(HomFin M N)) :

tensor_VN v ∘ₗ ↑f ∈ HomFin M VN

source

theorem proposition_18_3_bijective_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_5} {N : Type u_6} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] {V : Type u_7} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] {VN : Type u_8} [AddCommGroup VN] [Module R VN] [LieRingModule 𝔤 VN] [LieModule R 𝔤 VN] (tensor_VN : V →ₗ[R] N →ₗ[R] VN) (hiso_VN : Function.Bijective ⇑(TensorProduct.lift tensor_VN)) (φ : TensorProduct R V ↥(HomFin M N) →ₗ[R] ↥(HomFin M VN)) (hφ_nat : ∀ (f : ↥(HomFin M N)) (v : V) (m : M), ↑(φ (v ⊗ₜ[R] f)) m = (tensor_VN v) (↑f m)) :

Function.Bijective ⇑φ

source

theorem proposition_18_3 {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_5) (N : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (hM : IsCategoryO Δ rd M) (hN : IsCategoryO Δ rd N) (V : Type u_7) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (VN : Type u_8) [AddCommGroup VN] [Module R VN] [LieRingModule 𝔤 VN] [LieModule R 𝔤 VN] (tensor_VN : V →ₗ[R] N →ₗ[R] VN) (hiso_VN : Function.Bijective ⇑(TensorProduct.lift tensor_VN)) :

∃ (φ : TensorProduct R V ↥(HomFin M N) →ₗ[R] ↥(HomFin M VN)), Function.Bijective ⇑φ ∧ ∀ (f : ↥(HomFin M N)) (v : V) (m : M), ↑(φ (v ⊗ₜ[R] f)) m = (tensor_VN v) (↑f m)

source

def HomEquivariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (N : Type u_4) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] :

Submodule R (M →ₗ[R] N)

Instances For

source

theorem exercise_8_14_simpleVermaSubmodule_exists {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) (hVerma : IsVermaModule Δ M wt) :

∃ (M' : Type u_6) (x : AddCommGroup M') (x_1 : Module R M') (x_2 : LieRingModule 𝔤 M') (x_3 : LieModule R 𝔤 M') (_ : LieModule.IsIrreducible R 𝔤 M') (wt' : ↥Δ.𝔥 →ₗ[R] R) (x_5 : IsVermaModule Δ M' wt'), Nonempty (M' →ₗ[R] M)

source

theorem prop_8_5_tensor_retraction {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (N : Type u_7) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) :

∃ (r : N →ₗ[R] V), (∀ (v : V), r ((tensor v) hVerma.highestWeightVec) = v) ∧ (∀ (f : M →ₗ[R] N), (∀ (x : 𝔤) (m : M), f ⁅x, m⁆ = ⁅x, f m⁆) → r (f hVerma.highestWeightVec) ∈ WeightSpace Δ V 0 ∧ f hVerma.highestWeightVec = (tensor (r (f hVerma.highestWeightVec))) hVerma.highestWeightVec) ∧ ∀ (f₁ f₂ : M →ₗ[R] N), (∀ (x : 𝔤) (m : M), f₁ ⁅x, m⁆ = ⁅x, f₁ m⁆) → (∀ (x : 𝔤) (m : M), f₂ ⁅x, m⁆ = ⁅x, f₂ m⁆) → f₁ hVerma.highestWeightVec = f₂ hVerma.highestWeightVec → f₁ = f₂

source

theorem prop_18_5_restriction_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (_tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift _tensor)) :

∃ (φ : ↥(HomEquivariant M N) →ₗ[R] ↥(WeightSpace Δ V 0)), Function.Injective ⇑φ

source

theorem tensor_hwv_is_highest_weight {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (N : Type u_7) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) (v : V) (hv : v ∈ WeightSpace Δ V 0) :

(∀ (h : ↥Δ.𝔥), ⁅↑h, (tensor v) hVerma.highestWeightVec⁆ = wt h • (tensor v) hVerma.highestWeightVec) ∧ ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, (tensor v) hVerma.highestWeightVec⁆ = 0

source

theorem tensor_hwv_injective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (N : Type u_7) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) (v : V) (hv : (tensor v) hVerma.highestWeightVec = 0) :

v = 0

source

theorem homEquivariant_finite {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (N : Type u_7) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) :

Module.Finite R ↥(HomEquivariant M N)

source

theorem verma_universal_map_to_N {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) (hVerma : IsVermaModule Δ M wt) (N : Type u_6) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (n : N) (hn_wt : ∀ (h : ↥Δ.𝔥), ⁅↑h, n⁆ = wt h • n) (hn_pos : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, n⁆ = 0) :

∃ (η : M →ₗ[R] N), (∀ (x : 𝔤) (m : M), η ⁅x, m⁆ = ⁅x, η m⁆) ∧ η hVerma.highestWeightVec = n ∧ ∀ (η' : M →ₗ[R] N), (∀ (x : 𝔤) (m : M), η' ⁅x, m⁆ = ⁅x, η' m⁆) → η' hVerma.highestWeightVec = n → η' = η

source

theorem prop_18_5_ge_injection {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) :

∃ (φ : ↥(WeightSpace Δ V 0) →ₗ[R] ↥(HomEquivariant M N)), Function.Injective ⇑φ ∧ Module.Finite R ↥(HomEquivariant M N)

source

theorem prop_18_5_ge {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) :

Module.finrank R ↥(WeightSpace Δ V 0) ≤ Module.finrank R ↥(HomEquivariant M N)

source

theorem prop_18_5_le {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (_hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) [IsNoetherianRing R] :

Module.finrank R ↥(HomEquivariant M N) ≤ Module.finrank R ↥(WeightSpace Δ V 0)

source

theorem proposition_18_5 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (tensor : V →ₗ[R] M →ₗ[R] N) (hiso : Function.Surjective ⇑(TensorProduct.lift tensor)) [IsNoetherianRing R] :

Module.finrank R ↥(HomEquivariant M N) = Module.finrank R ↥(WeightSpace Δ V 0)

source

theorem exercise_18_4_equivariant_finrank {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Finite R 𝔤] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (N : Type u_5) [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] :

Module.finrank R ↥(HomAdEquivariant V (HomFinBimodule M N)) = Module.finrank R ↥(HomEquivariant M (TensorProduct R V N))

source

def ueaActionFromLieModule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] :

UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M

Instances For

source

theorem ueaActionFromLieModule_compat {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (x : 𝔤) (m : M) :

((ueaActionFromLieModule M) ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆

source

theorem center_scalar_eq_evalHC {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hHW : IsHighestWeightModule Δ M wt) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (c : R) (hscal : ∀ (m : M), ((ueaActionFromLieModule M) ↑z) m = c • m) :

c = (evalHC Δ wg (wt + wg.ρ)) z

source

def vermaHasInfinitesimalCharacter {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

HasInfinitesimalCharacter M (evalHC Δ wg (wt + wg.ρ))

Instances For

source

theorem actionHom_image_in_HomFin {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hVerma : IsVermaModule Δ M wt) (act : MaximalQuotient (evalHC Δ wg (wt + wg.ρ)) →ₐ[R] Module.End R M) (hcompat_act : ∀ (y : 𝔤) (m : M), (act ((MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) ((UniversalEnvelopingAlgebra.ι R) y))) m = ⁅y, m⁆) (q : MaximalQuotient (evalHC Δ wg (wt + wg.ρ))) :

act q ∈ HomFin M M

source

noncomputable def actionHom {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

MaximalQuotient (evalHC Δ wg (wt + wg.ρ)) →ₗ[R] ↥(HomFin M M)

Instances For

source

def ueaIncl_neg {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) :

UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg →ₐ[R] UniversalEnvelopingAlgebra R 𝔤

Instances For

source

def ueaIncl_pos {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) :

UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos →ₐ[R] UniversalEnvelopingAlgebra R 𝔤

Instances For

source

noncomputable def multMap_xi {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) :

TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) →ₗ[R] MaximalQuotient (evalHC Δ wg (wt + wg.ρ))

Instances For

source

noncomputable def multMap_ug {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) :

TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) →ₗ[R] UniversalEnvelopingAlgebra R 𝔤

Instances For

source

theorem multMap_xi_eq_proj_comp_multMap_ug {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (x : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) :

(multMap_xi Δ wg wt) x = (MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) ((multMap_ug Δ) x)

source

theorem shapovalov_ueaAction_multMap_ug_ne_zero {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (x : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) (hx : x ≠ 0) :

have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; hic.ueaAction ((multMap_ug Δ) x) ≠ 0

source

theorem shapovalov_nondeg_act_ne_zero {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (x : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) (hx : x ≠ 0) :

let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; have act := ⋯.choose; act ((multMap_xi Δ wg wt) x) ≠ 0

source

theorem shapovalov_composition_injective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; have act := ⋯.choose; Function.Injective fun (x : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) => act ((multMap_xi Δ wg wt) x)

source

def ueaIncl_h {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) :

UniversalEnvelopingAlgebra R ↥Δ.𝔥 →ₐ[R] UniversalEnvelopingAlgebra R 𝔤

Instances For

source

theorem pbw_triangular_iso_tmul {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (a : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (h : UniversalEnvelopingAlgebra R ↥Δ.𝔥) (b : UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) :

(pbw_triangular_iso R 𝔤 Δ) (a ⊗ₜ[R] (h ⊗ₜ[R] b)) = (ueaIncl_neg Δ) a * (ueaIncl_h Δ) h * (ueaIncl_pos Δ) b

source

theorem hc_cartan_acts_scalar_in_quotient {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (a : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (h : UniversalEnvelopingAlgebra R ↥Δ.𝔥) (b : UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) :

∃ (s : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)), (multMap_xi Δ wg wt) s = (MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) ((ueaIncl_neg Δ) a * (ueaIncl_h Δ) h * (ueaIncl_pos Δ) b)

source

theorem pbw_proj_pure {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (a : UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (h : UniversalEnvelopingAlgebra R ↥Δ.𝔥) (b : UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos) :

∃ (s : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)), (multMap_xi Δ wg wt) s = (MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) ((pbw_triangular_iso R 𝔤 Δ) (a ⊗ₜ[R] (h ⊗ₜ[R] b)))

source

theorem pbw_proj_factors_through_multMap_xi {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (t : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔥) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos))) :

source

theorem multMap_xi_surjective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) :

Function.Surjective ⇑(multMap_xi Δ wg wt)

source

theorem nilpotent_cone_domain_contradiction {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (h_xi_inj : let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; have act := ⋯.choose; Function.Injective fun (x : TensorProduct R (UniversalEnvelopingAlgebra R ↥Δ.𝔫_neg) (UniversalEnvelopingAlgebra R ↥Δ.𝔫_pos)) => act ((multMap_xi Δ wg wt) x)) :

let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; have act := ⋯.choose; Function.Injective ⇑act

source

theorem shapovalov_nondeg_annihilator_axiom {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (u : UniversalEnvelopingAlgebra R 𝔤) (hzero : ∀ (m : M), ((vermaHasInfinitesimalCharacter Δ wg M wt hVerma).ueaAction u) m = 0) :

(MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) u = 0

source

theorem shapovalov_pbw_injectivity {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; Function.Injective ⇑⋯.choose

source

theorem verma_factoredAction_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

let χ := evalHC Δ wg (wt + wg.ρ); have hic := vermaHasInfinitesimalCharacter Δ wg M wt hVerma; Function.Injective ⇑⋯.choose

source

theorem verma_ueaAction_zero_implies_proj_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (u : UniversalEnvelopingAlgebra R 𝔤) (hzero : (vermaHasInfinitesimalCharacter Δ wg M wt hVerma).ueaAction u = 0) :

(MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) u = 0

source

theorem verma_ueaAction_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (act : MaximalQuotient (evalHC Δ wg (wt + wg.ρ)) →ₐ[R] Module.End R M) (hact : ∀ (u : UniversalEnvelopingAlgebra R 𝔤) (m : M), ((vermaHasInfinitesimalCharacter Δ wg M wt hVerma).ueaAction u) m = (act ((MaximalQuotient.proj (evalHC Δ wg (wt + wg.ρ))) u)) m) :

Function.Injective ⇑act

source

theorem proposition_18_7 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

Function.Injective ⇑(actionHom Δ wg M wt hVerma)

source

theorem ueaAction_surjective_onto_HomFin {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (f : ↥(HomFin M M)) :

∃ (u : UniversalEnvelopingAlgebra R 𝔤), (vermaHasInfinitesimalCharacter Δ wg M wt hVerma).ueaAction u = ↑f

source

theorem kostant_actionHom_surjective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

Function.Surjective ⇑(actionHom Δ wg M wt hVerma)

source

theorem actionHom_surjective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

Function.Surjective ⇑(actionHom Δ wg M wt hVerma)

source

theorem actionHom_linearEquiv_of_dimension_argument {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) (hinj : Function.Injective ⇑(actionHom Δ wg M wt hVerma)) :

∃ (e : MaximalQuotient (evalHC Δ wg (wt + wg.ρ)) ≃ₗ[R] ↥(HomFin M M)), ↑e = actionHom Δ wg M wt hVerma

source

theorem corollary_18_8 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

Function.Bijective ⇑(actionHom Δ wg M wt hVerma)

source

noncomputable def dufloJosephIso {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

MaximalQuotient (evalHC Δ wg (wt + wg.ρ)) ≃ₗ[R] ↥(HomFin M M)

Instances For

source

theorem isFiniteTypeMap_comp_mk_tensor {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔤 N] [LieModule R 𝔤 N] (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (v : V) (T : M →ₗ[R] N) (hT : IsFiniteTypeMap M N T) :

IsFiniteTypeMap M (TensorProduct R V N) ((TensorProduct.mk R V N) v ∘ₗ T)

source

noncomputable def tensorActionMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

TensorProduct R V (MaximalQuotient (evalHC Δ wg (wt + wg.ρ))) →ₗ[R] ↥(HomFin M (TensorProduct R V M))

Instances For

source

def tensorHomMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] :

TensorProduct R V ↥(HomFin M M) →ₗ[R] ↥(HomFin M (TensorProduct R V M))

Instances For

source

theorem tensorHomMap_bijective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_5) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] :

Function.Bijective ⇑(tensorHomMap V M)

source

theorem corollary_18_9 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

Function.Bijective ⇑(tensorActionMap Δ wg V M wt hVerma)

source

noncomputable def corollary_18_9_iso {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVerma : IsVermaModule Δ M wt) :

TensorProduct R V (MaximalQuotient (evalHC Δ wg (wt + wg.ρ))) ≃ₗ[R] ↥(HomFin M (TensorProduct R V M))

Instances For

source

def leftInfChars {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) :

Set (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R)

Instances For

source

theorem corollary_18_9_leftInfChars_subset {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_5) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (lam : ↥Δ.𝔥 →ₗ[R] R) :

leftInfChars (tensorBimodule (LieBimodule.trivial V) (evalHC Δ wg lam)) ⊆ {θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R | ∃ ν ∈ weights Δ V, θ = evalHC Δ wg (lam + ν)}

source

theorem corollary_18_9_leftInfChars_supset {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_5) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (lam : ↥Δ.𝔥 →ₗ[R] R) :

{θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R | ∃ ν ∈ weights Δ V, θ = evalHC Δ wg (lam + ν)} ⊆ leftInfChars (tensorBimodule (LieBimodule.trivial V) (evalHC Δ wg lam))

source

theorem corollary_18_10_i {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (lam : ↥Δ.𝔥 →ₗ[R] R) :

source

def infCharsOfModule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] :

Set (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R)

Instances For

source

theorem infCharsOfModule_tensor_subset_leftInfChars {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_5) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (lam : ↥Δ.𝔥 →ₗ[R] R) (hchar : HasInfinitesimalCharacter M (evalHC Δ wg lam)) :

infCharsOfModule (TensorProduct R V M) ⊆ leftInfChars (tensorBimodule (LieBimodule.trivial V) (evalHC Δ wg lam))

source

theorem corollary_18_10_ii {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (lam : ↥Δ.𝔥 →ₗ[R] R) (hchar : HasInfinitesimalCharacter M (evalHC Δ wg lam)) :

infCharsOfModule (TensorProduct R V M) ⊆ {θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R | ∃ ν ∈ weights Δ V, θ = evalHC Δ wg (lam + ν)}

source

theorem corollary_14_5_hc_bimodule_left_char_in_tensor_ax {R : Type u_3} [CommRing R] [IsDomain R] [CharZero R] [IsNoetherianRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hne : ∃ (m : M.carrier), m ≠ 0) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hchar : M.HasInfinitesimalCharacterPair (evalHC Δ wg lam) (evalHC Δ wg mu)) :

∃ (V : Type) (iACG : AddCommGroup V) (iMod : Module R V) (_ : Module.Finite R V) (iLRM : LieRingModule 𝔤 V) (iLM : LieModule R 𝔤 V) (_ : IsNoetherian R V) (_ : Module.IsTorsionFree R V), evalHC Δ wg lam ∈ leftInfChars (tensorBimodule (LieBimodule.trivial V) (evalHC Δ wg mu))

source

theorem corollary_14_5_left_char_from_weight {R : Type u_3} [CommRing R] [IsDomain R] [CharZero R] [IsNoetherianRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hne : ∃ (m : M.carrier), m ≠ 0) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hchar : M.HasInfinitesimalCharacterPair (evalHC Δ wg lam) (evalHC Δ wg mu)) :

∃ (ν : ↥Δ.𝔥 →ₗ[R] R), (∃ (V : Type) (x : AddCommGroup V) (x_1 : Module R V) (_ : Module.Finite R V) (x_3 : LieRingModule 𝔤 V) (x_4 : LieModule R 𝔤 V) (_ : IsNoetherian R V) (_ : Module.IsTorsionFree R V), ν ∈ weights Δ V) ∧ evalHC Δ wg lam = evalHC Δ wg (mu + ν)

source

theorem weights_in_weightLattice {R : Type u_3} [CommRing R] [IsDomain R] [CharZero R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (chev : ChevalleyData Δ) (V : Type u_5) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [IsNoetherian R V] [Module.IsTorsionFree R V] (ν : ↥Δ.𝔥 →ₗ[R] R) (hν : ν ∈ weights Δ V) :

chev.IsInWeightLattice ν

source

theorem hc_bimodule_weight_shift {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (chev : ChevalleyData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hne : ∃ (m : M.carrier), m ≠ 0) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hchar : M.HasInfinitesimalCharacterPair (evalHC Δ wg lam) (evalHC Δ wg mu)) :

∃ (ν : ↥Δ.𝔥 →ₗ[R] R), chev.IsInWeightLattice ν ∧ evalHC Δ wg lam = evalHC Δ wg (mu + ν)

source

theorem corollary_18_10_iii {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (chev : ChevalleyData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hne : ∃ (m : M.carrier), m ≠ 0) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hchar : M.HasInfinitesimalCharacterPair (evalHC Δ wg lam) (evalHC Δ wg mu)) :

∃ (w : wg.W), chev.IsInWeightLattice (wg.shiftedAction w lam - mu)

source

theorem corollary_18_10_full {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (chev : ChevalleyData Δ) (V : Type u_3) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (lam : ↥Δ.𝔥 →ₗ[R] R) (M_ii : Type u_4) [AddCommGroup M_ii] [Module R M_ii] [LieRingModule 𝔤 M_ii] [LieModule R 𝔤 M_ii] (hchar_ii : HasInfinitesimalCharacter M_ii (evalHC Δ wg lam)) (M_iii : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M_iii) (hne : ∃ (m : M_iii.carrier), m ≠ 0) (lam_iii mu_iii : ↥Δ.𝔥 →ₗ[R] R) (hchar_iii : M_iii.HasInfinitesimalCharacterPair (evalHC Δ wg lam_iii) (evalHC Δ wg mu_iii)) :

leftInfChars (tensorBimodule (LieBimodule.trivial V) (evalHC Δ wg lam)) = {θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R | ∃ ν ∈ weights Δ V, θ = evalHC Δ wg (lam + ν)} ∧ infCharsOfModule (TensorProduct R V M_ii) ⊆ {θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R | ∃ ν ∈ weights Δ V, θ = evalHC Δ wg (lam + ν)} ∧ ∃ (w : wg.W), chev.IsInWeightLattice (wg.shiftedAction w lam_iii - mu_iii)

source

def IsDominantIntegralWeight {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (_rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (γ : ↥Δ.𝔥 →ₗ[R] R) :

Prop

Instances For

source

@[reducible, inline]

abbrev CentralCharacter (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] :

Type (max (max u_3 u_4) u_3)

Instances For

source

def DominantWeights {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) :

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

Instances For

source

structure IsInHCBimod {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (θ χ : CentralCharacter R 𝔤) :

Prop

isHC : IsHarishChandraBimodule M
charPair : M.HasInfinitesimalCharacterPair θ χ

Instances For

source

def IsInHCBimod.ofEvalHC {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hchar : M.HasInfinitesimalCharacterPair (evalHC Δ wg lam) (evalHC Δ wg mu)) :

IsInHCBimod M (evalHC Δ wg lam) (evalHC Δ wg mu)

Instances For

source

theorem exercise_15_5 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) (hw : chev.IsInWeightLattice (wg.shiftedAction w lam - mu)) :

∃ (lam' : ↥Δ.𝔥 →ₗ[R] R) (γ : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ ∧ evalHC Δ wg lam = evalHC Δ wg (lam' + γ) ∧ evalHC Δ wg mu = evalHC Δ wg lam'

source

theorem character_extension_invariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (θ' : ↥wg.invariantSubalgebra →ₐ[R] R) :

∃ (wt : ↥Δ.𝔥 →ₗ[R] R), θ' = (evalWeight Δ wt).comp wg.invariantSubalgebra.val

source

theorem evalHC_surjective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (θ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

∃ (mu : ↥Δ.𝔥 →ₗ[R] R), θ = evalHC Δ wg mu

source

def stabilizerOfWeight {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (γ : ↥Δ.𝔥 →ₗ[R] R) :

Subgroup wg.W

Instances For

source

def equivModStab {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (γ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R) :

Prop

Instances For

source

theorem corollary_18_11_decomposition {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hne : ∃ (m : M.carrier), m ≠ 0) (θ χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (hchar : M.HasInfinitesimalCharacterPair θ χ) :

∃ (γ : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ ∧ θ = evalHC Δ wg (lam + γ) ∧ χ = evalHC Δ wg lam

source

theorem corollary_18_11_vanishing {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (θ χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (h : ∀ (lam γ : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ → ¬(θ = evalHC Δ wg (lam + γ) ∧ χ = evalHC Δ wg lam)) (M : LieBimodule R 𝔤) (hHC : IsHarishChandraBimodule M) (hchar : M.HasInfinitesimalCharacterPair θ χ) (m : M.carrier) :

m = 0

source

theorem dominant_weights_eq_of_shifted_orbit_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (γ₁ γ₂ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R) (hγ₁ : IsDominantIntegralWeight Δ rd chev γ₁) (hγ₂ : IsDominantIntegralWeight Δ rd chev γ₂) (w : wg.W) (hw : lam₂ = wg.shiftedAction w lam₁) (w' : wg.W) (hw' : lam₂ + γ₂ = wg.shiftedAction w' (lam₁ + γ₁)) :

γ₁ = γ₂

source

theorem equivModStab_of_shifted_orbit_ax {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (γ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R) (hγ : IsDominantIntegralWeight Δ rd chev γ) (w : wg.W) (hw : lam₂ = wg.shiftedAction w lam₁) (w' : wg.W) (hw' : lam₂ + γ = wg.shiftedAction w' (lam₁ + γ)) :

equivModStab Δ wg γ lam₁ lam₂

source

theorem dominant_weight_uniqueness_in_shifted_orbit {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (γ₁ γ₂ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R) (hγ₁ : IsDominantIntegralWeight Δ rd chev γ₁) (hγ₂ : IsDominantIntegralWeight Δ rd chev γ₂) (w : wg.W) (hw : lam₂ = wg.shiftedAction w lam₁) (w' : wg.W) (hw' : lam₂ + γ₂ = wg.shiftedAction w' (lam₁ + γ₁)) :

γ₁ = γ₂ ∧ equivModStab Δ wg γ₁ lam₁ lam₂

source

theorem corollary_18_11_uniqueness {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) (γ₁ γ₂ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R) (hγ₁ : IsDominantIntegralWeight Δ rd chev γ₁) (hγ₂ : IsDominantIntegralWeight Δ rd chev γ₂) (hθ : evalHC Δ wg (lam₁ + γ₁) = evalHC Δ wg (lam₂ + γ₂)) (hχ : evalHC Δ wg lam₁ = evalHC Δ wg lam₂) :

γ₁ = γ₂ ∧ equivModStab Δ wg γ₁ lam₁ lam₂

source

theorem corollary_18_11 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [IsDomain R] [CharZero R] [IsNoetherianRing R] [Module.Finite R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (chev : ChevalleyData Δ) :

(∀ (M : LieBimodule R 𝔤), IsHarishChandraBimodule M → (∃ (m : M.carrier), m ≠ 0) → ∀ (θ χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R), M.HasInfinitesimalCharacterPair θ χ → ∃ (γ : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ ∧ θ = evalHC Δ wg (lam + γ) ∧ χ = evalHC Δ wg lam) ∧ (∀ (θ χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R), (∀ (lam γ : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ → ¬(θ = evalHC Δ wg (lam + γ) ∧ χ = evalHC Δ wg lam)) → ∀ (M : LieBimodule R 𝔤), IsHarishChandraBimodule M → M.HasInfinitesimalCharacterPair θ χ → ∀ (m : M.carrier), m = 0) ∧ ∀ (γ₁ γ₂ lam₁ lam₂ : ↥Δ.𝔥 →ₗ[R] R), IsDominantIntegralWeight Δ rd chev γ₁ → IsDominantIntegralWeight Δ rd chev γ₂ → evalHC Δ wg (lam₁ + γ₁) = evalHC Δ wg (lam₂ + γ₂) → evalHC Δ wg lam₁ = evalHC Δ wg lam₂ → γ₁ = γ₂ ∧ equivModStab Δ wg γ₁ lam₁ lam₂