Atlas.LieGroups.code.MaximalQuotients

structure LieBimodule (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] :

Type (max (max u_3 u_4) (u_5 + 1))

carrier : Type u_5
instAddCommGroup : AddCommGroup self.carrier
instModule : Module R self.carrier
leftAction : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R self.carrier
rightAction : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ →ₐ[R] Module.End R self.carrier
actions_commute (u : UniversalEnvelopingAlgebra R 𝔤) (v : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (m : self.carrier) : (self.leftAction u) ((self.rightAction v) m) = (self.rightAction v) ((self.leftAction u) m)

Instances For

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

Module.End R M.carrier

Instances For

source

def LieBimodule.IsSubBimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (S : Submodule R M.carrier) :

Prop

Instances For

source

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

Prop

Instances For

source

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

Prop

locally_finite (m : M.carrier) : ∃ (S : Submodule R M.carrier), Module.Finite R ↥S ∧ m ∈ S ∧ ∀ (x : 𝔤), ∀ s ∈ S, (M.adjointAction x) s ∈ S

Instances For

source

structure LieBimodule.HasInfinitesimalCharacterPair {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (θ χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

Prop

left_char (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (m : M.carrier) : (M.leftAction ↑z) m = θ z • m
right_char (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (m : M.carrier) : (M.rightAction (MulOpposite.op ↑z)) m = χ z • m

Instances For

source

def HomAdEquivariant {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] (M : LieBimodule R 𝔤) :

Submodule R (V →ₗ[R] M.carrier)

Instances For

source

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

Prop

isHC : IsHarishChandraBimodule M
admissible (V : Type) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [LieModule.IsIrreducible R 𝔤 V] : Module.Finite R ↥(HomAdEquivariant V M)

Instances For

source

def maximalQuotientIdeal {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

TwoSidedIdeal (UniversalEnvelopingAlgebra R 𝔤)

Instances For

source

@[reducible, inline]

abbrev MaximalQuotient {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

Type (max u_1 u_2)

Instances For

source

def MaximalQuotient.proj {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] MaximalQuotient χ

Instances For

source

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

𝔤 →ₗ⁅R⁆ (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ

Instances For

source

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

UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ

Instances For

source

def rmulAlgHom {R : Type u_1} [CommRing R] (A : Type u_3) [Ring A] [Algebra R A] :

Aᵐᵒᵖ →ₐ[R] Module.End R A

Instances For

source

def MaximalQuotient.bimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

LieBimodule R 𝔤

Instances For

source

theorem MaximalQuotient.factors_through {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hic : HasInfinitesimalCharacter M χ) :

∃ (act : MaximalQuotient χ →ₐ[R] Module.End R M), ∀ (u : UniversalEnvelopingAlgebra R 𝔤) (m : M), (hic.ueaAction u) m = (act ((proj χ) u)) m

source

theorem UniversalEnvelopingAlgebra.lift_centralizes {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {A : Type u_3} [Ring A] [Algebra R A] (f : 𝔤 →ₗ⁅R⁆ A) (E : A) (hf : ∀ (x : 𝔤), f x * E = E * f x) (u : UniversalEnvelopingAlgebra R 𝔤) :

((lift R) f) u * E = E * ((lift R) f) u

source

def tensorBimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : LieBimodule R 𝔤) (χ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

LieBimodule R 𝔤

Instances For

source

def kostant_base_change_equiv_of_thm135 {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ ] ↥(WeightSpace Δ V 0)

Instances For

source

theorem kostant_base_change_finiteDim_core {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

Module.Finite ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ))

source

theorem kostant_base_change_finrank_core {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

Module.finrank ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) = Module.finrank ℂ ↥(WeightSpace Δ V 0)

source

noncomputable def kostant_base_change_equiv {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ ] ↥(WeightSpace Δ V 0)

Instances For

source

noncomputable def kostant_base_change_linearEquiv {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ ] ↥(WeightSpace Δ V 0)

Instances For

source

theorem kostant_base_change_finiteDim {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

Module.Finite ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ))

source

theorem kostant_base_change_finrank_eq {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

Module.finrank ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) = Module.finrank ℂ ↥(WeightSpace Δ V 0)

source

noncomputable def kostant_base_change_embedding {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ ] ↥(WeightSpace Δ V 0)

Instances For

source

noncomputable def kostant_base_change_iso {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_4) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

↥(HomAdEquivariant V (MaximalQuotient.bimodule χ)) ≃ₗ[ℂ ] ↥(WeightSpace Δ V 0)

Instances For

source

theorem HomAdEquivariant_finiteDimensional {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_4) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (hirr : LieModule.IsIrreducible ℂ 𝔤 V) :

Module.Finite ℂ ↥(HomAdEquivariant V (MaximalQuotient.bimodule χ))

source

theorem uea_ad_stable_mul (R : Type u_4) [CommRing R] (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra R 𝔤] (Sa Sb : Submodule R (UniversalEnvelopingAlgebra R 𝔤)) (hSa : ∀ (x : 𝔤), ∀ s ∈ Sa, (UniversalEnvelopingAlgebra.ι R) x * s - s * (UniversalEnvelopingAlgebra.ι R) x ∈ Sa) (hSb : ∀ (x : 𝔤), ∀ s ∈ Sb, (UniversalEnvelopingAlgebra.ι R) x * s - s * (UniversalEnvelopingAlgebra.ι R) x ∈ Sb) (x : 𝔤) (s : UniversalEnvelopingAlgebra R 𝔤) :

s ∈ Sa * Sb → (UniversalEnvelopingAlgebra.ι R) x * s - s * (UniversalEnvelopingAlgebra.ι R) x ∈ Sa * Sb

source

theorem uea_adjoint_locally_finite (R : Type u_4) [CommRing R] (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra R 𝔤] [Module.Finite R 𝔤] (u : UniversalEnvelopingAlgebra R 𝔤) :

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

source

theorem corollary_14_3_HC {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) :

IsHarishChandraBimodule (MaximalQuotient.bimodule χ)

source

theorem exercise_5_12 {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (V : LieBimodule ℂ 𝔤) [Module.Finite ℂ V.carrier] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (hAdm : IsAdmissibleBimodule (MaximalQuotient.bimodule χ)) :

IsAdmissibleBimodule (tensorBimodule V χ)

source

theorem corollary_14_4 {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (V : LieBimodule ℂ 𝔤) [Module.Finite ℂ V.carrier] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) :

IsAdmissibleBimodule (tensorBimodule V χ)

source

theorem dixmier_ker_nontrivial {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (T : Module.End ℂ M.carrier) (hT_left : ∀ (u : UniversalEnvelopingAlgebra ℂ 𝔤) (m : M.carrier), T ((M.leftAction u) m) = (M.leftAction u) (T m)) (hT_right : ∀ (w : (UniversalEnvelopingAlgebra ℂ 𝔤)ᵐᵒᵖ) (m : M.carrier), T ((M.rightAction w) m) = (M.rightAction w) (T m)) :

∃ (c : ℂ), (T - c • LinearMap.id).ker ≠ ⊥

source

theorem center_element_algebraic {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) :

∃ (p : Polynomial ℂ), p ≠ 0 ∧ (Polynomial.aeval (M.rightAction (MulOpposite.op ↑z))) p = 0

source

@[irreducible]

theorem algebraic_end_has_eigenvalue {K : Type u_4} {V : Type u_5} [Field K] [IsAlgClosed K] [AddCommGroup V] [Module K V] (T : Module.End K V) (p : Polynomial K) (hp : p ≠ 0) (hpT : (Polynomial.aeval T) p = 0) (hV : ∃ (v : V), v ≠ 0) :

∃ (c : K) (v : V), v ≠ 0 ∧ T v = c • v

source

theorem center_right_action_has_eigenvalue {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) :

∃ (c₀ : ℂ) (v : M.carrier), v ≠ 0 ∧ (M.rightAction (MulOpposite.op ↑z)) v = c₀ • v

source

theorem bimod_center_acts_as_scalar {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) :

∃ (c : ℂ), ∀ (m : M.carrier), (M.rightAction (MulOpposite.op ↑z)) m = c • m

source

theorem dixmier_right_character {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) :

∃ (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ), ∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (m : M.carrier), (M.rightAction (MulOpposite.op ↑z)) m = χ z • m

source

@[reducible]

def LieBimodule.toLieRingModule' {R' : Type u_4} [CommRing R'] {𝔤' : Type u_5} [LieRing 𝔤'] [LieAlgebra R' 𝔤'] (M : LieBimodule R' 𝔤') :

LieRingModule 𝔤' M.carrier

Instances For

source

@[reducible]

def LieBimodule.toLieModule' {R' : Type u_4} [CommRing R'] {𝔤' : Type u_5} [LieRing 𝔤'] [LieAlgebra R' 𝔤'] (M : LieBimodule R' 𝔤') :

LieModule R' 𝔤' M.carrier

Instances For

source

theorem isIrreducible_of_isAtom_lieSubmodule {𝔤' : Type u_4} [LieRing 𝔤'] {V : Type u_5} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤' V] (N : LieSubmodule ℂ 𝔤' V) (hN : IsAtom N) :

LieModule.IsIrreducible ℂ 𝔤' ↥N

source

theorem weyl_irred_submodule_of_ad_stable {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (S : Submodule ℂ M.carrier) (hS_fin : Module.Finite ℂ ↥S) (hS_ne : ∃ s ∈ S, s ≠ 0) (hS_stable : ∀ (x : 𝔤), ∀ s ∈ S, (M.adjointAction x) s ∈ S) :

∃ (V : Type u_bimod_carrier) (x : AddCommGroup V) (x_1 : Module ℂ V) (x_2 : LieRingModule 𝔤 V) (_ : LieModule ℂ 𝔤 V) (_ : Module.Finite ℂ V) (_ : LieModule.IsIrreducible ℂ 𝔤 V) (ι : V →ₗ[ℂ ] M.carrier), Function.Injective ⇑ι ∧ ∀ (x_6 : 𝔤) (v : V), ι ⁅x_6, v⁆ = (M.adjointAction x_6) (ι v)

source

theorem adjoint_irred_submodule {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (hlocfin : IsHarishChandraBimodule M) :

source

def UniversalEnvelopingAlgebra.counit {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] :

UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] R

Instances For

source

def UniversalEnvelopingAlgebra.counitOp {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] :

(UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ →ₐ[R] R

Instances For

source

def LieBimodule.trivial {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_6) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] :

LieBimodule R 𝔤

Instances For

source

instance LieBimodule.trivial_finiteDimensional {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_6) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] :

Module.Finite R (trivial V).carrier

source

theorem canonical_element_map_exists {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (hχ : ∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (m : M.carrier), (M.rightAction (MulOpposite.op ↑z)) m = χ z • m) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] [Nontrivial V] (ι : V →ₗ[ℂ ] M.carrier) (hι : Function.Injective ⇑ι) (hι_lie : ∀ (x : 𝔤) (v : V), ι ⁅x, v⁆ = (M.adjointAction x) (ι v)) :

∃ (ξ : TensorProduct ℂ V (MaximalQuotient χ) →ₗ[ℂ ] M.carrier), ξ ≠ 0 ∧ (∀ (x : 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), ξ (((tensorBimodule (LieBimodule.trivial V) χ).adjointAction x) t) = (M.adjointAction x) (ξ t)) ∧ (∀ (u : UniversalEnvelopingAlgebra ℂ 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), ξ (((tensorBimodule (LieBimodule.trivial V) χ).leftAction u) t) = (M.leftAction u) (ξ t)) ∧ ∀ (u : (UniversalEnvelopingAlgebra ℂ 𝔤)ᵐᵒᵖ) (t : TensorProduct ℂ V (MaximalQuotient χ)), ξ (((tensorBimodule (LieBimodule.trivial V) χ).rightAction u) t) = (M.rightAction u) (ξ t)

source

theorem canonical_element_image_is_subbimodule {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (_hχ : ∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (m : M.carrier), (M.rightAction (MulOpposite.op ↑z)) m = χ z • m) (V : Type u_5) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (_ι : V →ₗ[ℂ ] M.carrier) (_hι : Function.Injective ⇑_ι) (ξ : TensorProduct ℂ V (MaximalQuotient χ) →ₗ[ℂ ] M.carrier) (_hξ_ne : ξ ≠ 0) (hξ_left : ∀ (u : UniversalEnvelopingAlgebra ℂ 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), ξ (((tensorBimodule (LieBimodule.trivial V) χ).leftAction u) t) = (M.leftAction u) (ξ t)) (hξ_right : ∀ (u : (UniversalEnvelopingAlgebra ℂ 𝔤)ᵐᵒᵖ) (t : TensorProduct ℂ V (MaximalQuotient χ)), ξ (((tensorBimodule (LieBimodule.trivial V) χ).rightAction u) t) = (M.rightAction u) (ξ t)) :

M.IsSubBimodule ξ.range

source

theorem canonical_element_surjection {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (hχ : ∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (m : M.carrier), (M.rightAction (MulOpposite.op ↑z)) m = χ z • m) (V : Type u_4) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [Module.Finite ℂ V] (_hirr_V : LieModule.IsIrreducible ℂ 𝔤 V) (ι : V →ₗ[ℂ ] M.carrier) (hι : Function.Injective ⇑ι) (hι_lie : ∀ (x : 𝔤) (v : V), ι ⁅x, v⁆ = (M.adjointAction x) (ι v)) :

∃ (surj : TensorProduct ℂ V (MaximalQuotient χ) →ₗ[ℂ ] M.carrier), Function.Surjective ⇑surj ∧ ∀ (x : 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), surj (((tensorBimodule (LieBimodule.trivial V) χ).adjointAction x) t) = (M.adjointAction x) (surj t)

source

theorem corollary_14_5_i {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (M : LieBimodule ℂ 𝔤) (hirr : M.IsIrreducible) (hlocfin : IsHarishChandraBimodule M) :

∃ (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V : Type u_bimod_carrier) (x : AddCommGroup V) (x_1 : Module ℂ V) (x_2 : LieRingModule 𝔤 V) (x_3 : LieModule ℂ 𝔤 V) (_ : Module.Finite ℂ V) (_ : LieModule.IsIrreducible ℂ 𝔤 V) (surj : TensorProduct ℂ V (MaximalQuotient χ) →ₗ[ℂ ] M.carrier), Function.Surjective ⇑surj ∧ ∀ (x_6 : 𝔤) (t : TensorProduct ℂ V (MaximalQuotient χ)), surj (((tensorBimodule (LieBimodule.trivial V) χ).adjointAction x_6) t) = (M.adjointAction x_6) (surj t)

source

theorem weyl_complete_reducibility_lift {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] {V : Type u_5} {M : Type u_6} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] [AddCommGroup M] [Module ℂ M] [LieRingModule 𝔤 M] [LieModule ℂ 𝔤 M] (W : Type u_7) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] [Module.Finite ℂ W] (hirr : LieModule.IsIrreducible ℂ 𝔤 W) (f : V →ₗ⁅ℂ ,𝔤⁆ M) (hf_surj : Function.Surjective ⇑f) (φ : W →ₗ⁅ℂ ,𝔤⁆ M) :

∃ (ψ : W →ₗ⁅ℂ ,𝔤⁆ V), ∀ (w : W), f (ψ w) = φ w

source

theorem weyl_equivariant_lift {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (N : LieBimodule ℂ 𝔤) (M : LieBimodule ℂ 𝔤) (f : N.carrier →ₗ[ℂ ] M.carrier) (hf_surj : Function.Surjective ⇑f) (hf_equivar : ∀ (x : 𝔤) (n : N.carrier), f ((N.adjointAction x) n) = (M.adjointAction x) (f n)) (W : Type u_5) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] [Module.Finite ℂ W] (hirr : LieModule.IsIrreducible ℂ 𝔤 W) (φ : ↥(HomAdEquivariant W M)) :

∃ (ψ : ↥(HomAdEquivariant W N)), ∀ (w : W), f (↑ψ w) = ↑φ w

source

theorem hc_hom_finite {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (N : LieBimodule ℂ 𝔤) (hN : IsAdmissibleBimodule N) (W : Type) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] [Module.Finite ℂ W] (hirr : LieModule.IsIrreducible ℂ 𝔤 W) :

Module.Finite ℂ ↥(HomAdEquivariant W N)

source

theorem hc_quotient_admissible {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] (N : LieBimodule ℂ 𝔤) (M : LieBimodule ℂ 𝔤) (hN : IsAdmissibleBimodule N) (f : N.carrier →ₗ[ℂ ] M.carrier) (hf_surj : Function.Surjective ⇑f) (hf_equivar : ∀ (x : 𝔤) (n : N.carrier), f ((N.adjointAction x) n) = (M.adjointAction x) (f n)) (W : Type) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] [Module.Finite ℂ W] :

LieModule.IsIrreducible ℂ 𝔤 W → Module.Finite ℂ ↥(HomAdEquivariant W M)

source

theorem tensor_quotient_admissible {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] (Δ : TriangularDecomposition ℂ 𝔤) (M : LieBimodule ℂ 𝔤) (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ ] ℂ) (V₀ : Type u_4) [AddCommGroup V₀] [Module ℂ V₀] [LieRingModule 𝔤 V₀] [LieModule ℂ 𝔤 V₀] [Module.Finite ℂ V₀] (_hirr_V₀ : LieModule.IsIrreducible ℂ 𝔤 V₀) (surj : TensorProduct ℂ V₀ (MaximalQuotient χ) →ₗ[ℂ ] M.carrier) (hsurj : Function.Surjective ⇑surj) (hequivar : ∀ (x : 𝔤) (t : TensorProduct ℂ V₀ (MaximalQuotient χ)), surj (((tensorBimodule (LieBimodule.trivial V₀) χ).adjointAction x) t) = (M.adjointAction x) (surj t)) (W : Type) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] [Module.Finite ℂ W] :

LieModule.IsIrreducible ℂ 𝔤 W → Module.Finite ℂ ↥(HomAdEquivariant W M)