Atlas.LieGroups.code.HarishChandraIsomorphism

source

def Subalgebra.invariants {R : Type u_3} [CommSemiring R] {A : Type u_4} [Semiring A] [Algebra R A] (G : Type u_5) [Group G] (act : G →* A ≃ₐ[R] A) :

Subalgebra R A

Instances For

source

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

IsLieAbelian ↥Δ.𝔥

source

def weightToLieHom {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (wt : L →ₗ[R] R) :

L →ₗ⁅R⁆ R

Instances For

source

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

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

Instances For

source

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

Type (max (max u_1 u_2) (u_3 + 1))

W : Type u_3
instGroup : Group self.W
instFintype : Fintype self.W
algAction : self.W →* UniversalEnvelopingAlgebra R ↥Δ.𝔥 ≃ₐ[R] UniversalEnvelopingAlgebra R ↥Δ.𝔥
ρ : ↥Δ.𝔥 →ₗ[R] R
dualAction : self.W → (↥Δ.𝔥 →ₗ[R] R) → ↥Δ.𝔥 →ₗ[R] R
dualAction_one (μ : ↥Δ.𝔥 →ₗ[R] R) : self.dualAction 1 μ = μ
dualAction_mul (w₁ w₂ : self.W) (μ : ↥Δ.𝔥 →ₗ[R] R) : self.dualAction (w₁ * w₂) μ = self.dualAction w₁ (self.dualAction w₂ μ)
dualAction_add (w : self.W) (μ ν : ↥Δ.𝔥 →ₗ[R] R) : self.dualAction w (μ + ν) = self.dualAction w μ + self.dualAction w ν
dualAction_smul (w : self.W) (c : R) (μ : ↥Δ.𝔥 →ₗ[R] R) : self.dualAction w (c • μ) = c • self.dualAction w μ
algDualCompat (g : self.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (p : UniversalEnvelopingAlgebra R ↥Δ.𝔥) : (evalWeight Δ wt) ((self.algAction g) p) = (evalWeight Δ (self.dualAction g⁻¹ wt)) p
orbitSeparation (mu nu : ↥Δ.𝔥 →ₗ[R] R) : (∀ (p : UniversalEnvelopingAlgebra R ↥Δ.𝔥), (∀ (g : self.W), (self.algAction g) p = p) → (evalWeight Δ mu) p = (evalWeight Δ nu) p) → ∃ (w : self.W), nu = self.dualAction w mu

Instances For

source

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

Subalgebra R (UniversalEnvelopingAlgebra R ↥Δ.𝔥)

Instances For

source

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

↥Δ.𝔥 →ₗ[R] R

Instances For

source

def PositiveRootData.sumPosRoots {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) :

↥Δ.𝔥 →ₗ[R] R

Instances For

source

def augmentation (R : Type u_3) [CommRing R] (L : Type u_4) [LieRing L] [LieAlgebra R L] :

UniversalEnvelopingAlgebra R L →ₐ[R] R

Instances For

source

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

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

Instances For

source

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

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

Instances For

source

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

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

Instances For

source

theorem uea_algHom_separates {R : Type u_3} [CommRing R] {L : Type u_4} [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (p q : UniversalEnvelopingAlgebra R L) (h : ∀ (f : UniversalEnvelopingAlgebra R L →ₐ[R] R), f p = f q) :

p = q

source

theorem evalWeight_separates {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (p q : UniversalEnvelopingAlgebra R ↥Δ.𝔥) (h : ∀ (wt : ↥Δ.𝔥 →ₗ[R] R), (evalWeight Δ wt) p = (evalWeight Δ wt) q) :

p = q

source

theorem LinearMap.exists_factor_of_surjective_ker_le {R' : Type u_3} [CommRing R'] {A : Type u_4} {B : Type u_5} {C : Type u_6} [AddCommGroup A] [Module R' A] [AddCommGroup B] [Module R' B] [AddCommGroup C] [Module R' C] (p : A →ₗ[R'] B) (f : A →ₗ[R'] C) (hsurj : Function.Surjective ⇑p) (hker : p.ker ≤ f.ker) :

∃ (ℓ : B →ₗ[R'] C), ∀ (a : A), ℓ (p a) = f a

source

theorem pbw_hc_eval_kernel_vanishing {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (u : UniversalEnvelopingAlgebra R 𝔤) (hu : (ueaAct u) hM.highestWeightVec = 0) :

(evalWeight Δ wt) ((HarishChandraMap Δ) u) = 0

source

theorem pbw_ueaAct_surjective {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) :

Function.Surjective fun (u : UniversalEnvelopingAlgebra R 𝔤) => (ueaAct u) hM.highestWeightVec

source

theorem pbw_hc_eval_factors_through_action {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) :

∃ (ℓ : M →ₗ[R] R), ∀ (u : UniversalEnvelopingAlgebra R 𝔤), (evalWeight Δ wt) ((HarishChandraMap Δ) u) = ℓ ((ueaAct u) hM.highestWeightVec)

source

theorem pbw_eval_hc_vanishes_on_annihilator {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (u : UniversalEnvelopingAlgebra R 𝔤) (hu : (ueaAct u) hM.highestWeightVec = 0) :

(evalWeight Δ wt) ((HarishChandraMap Δ) u) = 0

source

theorem pbw_hc_map_one {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) :

(HarishChandraMap Δ) 1 = 1

source

theorem pbw_verma_eval_any_hwm {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) :

∃ (phi : M →ₗ[R] R), phi hM.highestWeightVec = 1 ∧ ∀ (u : UniversalEnvelopingAlgebra R 𝔤), phi ((ueaAct u) hM.highestWeightVec) = (evalWeight Δ wt) ((HarishChandraMap Δ) u)

source

theorem pbw_verma_eval {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt : ↥Δ.𝔥 →ₗ[R] R) :

∃ (M : Type) (x : AddCommGroup M) (x_1 : Module R M) (x_2 : LieRingModule 𝔤 M) (x_3 : LieModule R 𝔤 M) (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (_ : ∀ (x_4 : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x_4)) m = ⁅x_4, m⁆) (phi : M →ₗ[R] R), phi hM.highestWeightVec = 1 ∧ ∀ (u : UniversalEnvelopingAlgebra R 𝔤), phi ((ueaAct u) hM.highestWeightVec) = (evalWeight Δ wt) ((HarishChandraMap Δ) u)

source

theorem hc_eval_mul_central {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (b : UniversalEnvelopingAlgebra R 𝔤) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (wt : ↥Δ.𝔥 →ₗ[R] R) :

(evalWeight Δ wt) ((HarishChandraMap Δ) (b * ↑c)) = (evalWeight Δ wt) ((HarishChandraMap Δ) b) * (evalWeight Δ wt) ((HarishChandraMap Δ) ↑c)

source

theorem harishChandra_mul_central {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (b : UniversalEnvelopingAlgebra R 𝔤) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(HarishChandraMap Δ) (b * ↑c) = (HarishChandraMap Δ) b * (HarishChandraMap Δ) ↑c

source

theorem center_acts_by_scalar_on_hwm {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) (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

∃ (c : R), ∀ (m : M), (ueaAct ↑z) m = c • m

source

theorem evalWeight_algAction_eq {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (p : UniversalEnvelopingAlgebra R ↥Δ.𝔥) :

(evalWeight Δ wt) ((wg.algAction g) p) = (evalWeight Δ (wg.dualAction g⁻¹ wt)) p

source

theorem hwm_central_scalar_eq_evalWeight {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hM : IsHighestWeightModule Δ M wt) (ueaAct : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M) (hcompat : ∀ (x : 𝔤) (m : M), (ueaAct ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (s : R) (hs : ∀ (m : M), (ueaAct ↑c) m = s • m) :

s = (evalWeight Δ wt) ((HarishChandraMap Δ) ↑c)

source

theorem hc_W_invariance_axiom {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(HarishChandraMap Δ) ↑c ∈ wg.invariantSubalgebra

source

theorem verma_embedding_scalar_invariance {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₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module R M₂] [LieRingModule 𝔤 M₂] [LieModule R 𝔤 M₂] (wt : ↥Δ.𝔥 →ₗ[R] R) (g : wg.W) (hM₁ : IsHighestWeightModule Δ M₁ wt) (hM₂ : IsHighestWeightModule Δ M₂ (wg.dualAction g wt)) (ueaAct₁ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₁) (ueaAct₂ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₂) (hcompat₁ : ∀ (x : 𝔤) (m : M₁), (ueaAct₁ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (hcompat₂ : ∀ (x : 𝔤) (m : M₂), (ueaAct₂ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (s₁ s₂ : R) (hs₁ : ∀ (m : M₁), (ueaAct₁ ↑c) m = s₁ • m) (hs₂ : ∀ (m : M₂), (ueaAct₂ ↑c) m = s₂ • m) :

s₁ = s₂

source

theorem harishChandra_verma_eval_invariance {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalWeight Δ (wg.dualAction g wt)) ((HarishChandraMap Δ) ↑c) = (evalWeight Δ wt) ((HarishChandraMap Δ) ↑c)

source

theorem filtered_graded_principle_for_hc {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

(∀ (c₁ c₂ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraMap Δ) ↑c₁ = (HarishChandraMap Δ) ↑c₂ → c₁ = c₂) ∧ ∀ p ∈ wg.invariantSubalgebra, ∃ (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraMap Δ) ↑c = p

source

theorem harishChandra_bijectivity {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

source

theorem harishChandra_isomorphism_sorry {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

(∀ (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraMap Δ) ↑c ∈ wg.invariantSubalgebra) ∧ (∀ (c₁ c₂ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraMap Δ) ↑c₁ = (HarishChandraMap Δ) ↑c₂ → c₁ = c₂) ∧ ∀ p ∈ wg.invariantSubalgebra, ∃ (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraMap Δ) ↑c = p

source

theorem WeylGroupData.dualAction_inv_cancel_left {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) :

wg.dualAction g⁻¹ (wg.dualAction g wt) = wt

source

theorem harishChandra_W_invariant {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (g : wg.W) :

(wg.algAction g) ((HarishChandraMap Δ) ↑c) = (HarishChandraMap Δ) ↑c

source

theorem hc_eval_weyl_invariant_from_isomorphism {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalWeight Δ (wg.dualAction g wt)) ((HarishChandraMap Δ) ↑c) = (evalWeight Δ wt) ((HarishChandraMap Δ) ↑c)

source

theorem weyl_linked_central_scalar_eq {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₁] (M₂ : Type u_6) [AddCommGroup M₂] [Module R M₂] [LieRingModule 𝔤 M₂] [LieModule R 𝔤 M₂] (wt : ↥Δ.𝔥 →ₗ[R] R) (g : wg.W) (hM₁ : IsHighestWeightModule Δ M₁ wt) (hM₂ : IsHighestWeightModule Δ M₂ (wg.dualAction g wt)) (ueaAct₁ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₁) (ueaAct₂ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₂) (hcompat₁ : ∀ (x : 𝔤) (m : M₁), (ueaAct₁ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (hcompat₂ : ∀ (x : 𝔤) (m : M₂), (ueaAct₂ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (s₁ s₂ : R) (hs₁ : ∀ (m : M₁), (ueaAct₁ ↑c) m = s₁ • m) (hs₂ : ∀ (m : M₂), (ueaAct₂ ↑c) m = s₂ • m) :

s₁ = s₂

source

theorem verma_embedding_evalWeight_invariant {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalWeight Δ wt) ((HarishChandraMap Δ) ↑c) = (evalWeight Δ (wg.dualAction g wt)) ((HarishChandraMap Δ) ↑c)

source

theorem verma_embedding_central_scalar_invariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalWeight Δ wt) ((HarishChandraMap Δ) ↑c) = (evalWeight Δ (wg.dualAction g wt)) ((HarishChandraMap Δ) ↑c)

source

theorem weyl_linked_same_central_scalar {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₁] (M₂ : Type u_4) [AddCommGroup M₂] [Module R M₂] [LieRingModule 𝔤 M₂] [LieModule R 𝔤 M₂] (wt : ↥Δ.𝔥 →ₗ[R] R) (g : wg.W) (hM₁ : IsHighestWeightModule Δ M₁ wt) (hM₂ : IsHighestWeightModule Δ M₂ (wg.dualAction g wt)) (ueaAct₁ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₁) (ueaAct₂ : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M₂) (hcompat₁ : ∀ (x : 𝔤) (m : M₁), (ueaAct₁ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (hcompat₂ : ∀ (x : 𝔤) (m : M₂), (ueaAct₂ ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (s₁ s₂ : R) (hs₁ : ∀ (m : M₁), (ueaAct₁ ↑c) m = s₁ • m) (hs₂ : ∀ (m : M₂), (ueaAct₂ ↑c) m = s₂ • m) :

s₂ = s₁

source

theorem hc_eval_weyl_invariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (g : wg.W) (wt : ↥Δ.𝔥 →ₗ[R] R) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalWeight Δ (wg.dualAction g wt)) ((HarishChandraMap Δ) ↑c) = (evalWeight Δ wt) ((HarishChandraMap Δ) ↑c)

source

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

(HarishChandraMap Δ) ↑c ∈ wg.invariantSubalgebra

source

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

(HarishChandraMap Δ) 1 = 1

source

theorem harishChandra_map_algebraMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (r : R) :

(HarishChandraMap Δ) ((algebraMap R (UniversalEnvelopingAlgebra R 𝔤)) r) = (algebraMap R (UniversalEnvelopingAlgebra R ↥Δ.𝔥)) r

source

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

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

Instances For

source

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

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

Instances For

source

theorem chevalley_and_filtered_graded {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

Function.Bijective ⇑(HarishChandraAlgHomToInvariant Δ wg)

source

theorem hc_injective_of_filtered_graded {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

Function.Injective ⇑(HarishChandraAlgHomToInvariant Δ wg)

source

theorem hc_surjective_of_filtered_graded {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

Function.Surjective ⇑(HarishChandraAlgHomToInvariant Δ wg)

source

theorem filtered_graded_bijectivity_principle {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

Function.Bijective ⇑(HarishChandraAlgHomToInvariant Δ wg)

source

theorem harishChandra_bijective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) :

Function.Bijective ⇑(HarishChandraAlgHomToInvariant Δ wg)

source

theorem harishChandra_injective_of_chevalley {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (h : (HarishChandraMap Δ) ↑c = 0) :

↑c = 0

source

theorem harishChandra_center_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (c₁ c₂ : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (h : (HarishChandraMap Δ) ↑c₁ = (HarishChandraMap Δ) ↑c₂) :

c₁ = c₂

source

theorem chevalley_restriction_surjectivity (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (p : UniversalEnvelopingAlgebra R ↥Δ.𝔥) (hp : p ∈ wg.invariantSubalgebra) :

∃ (c : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (HarishChandraAlgHom Δ) c = p

source

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

↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ≃ₐ[R] ↥wg.invariantSubalgebra

Instances For

source

@[reducible, inline]

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

↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ≃ₐ[R] ↥wg.invariantSubalgebra

Instances For

source

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

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

Instances For

source

structure HasInfinitesimalCharacter {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] (chi : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) :

Type (max (max u_1 u_2) u_3)

ueaAction : UniversalEnvelopingAlgebra R 𝔤 →ₐ[R] Module.End R M
compat (x : 𝔤) (m : M) : (self.ueaAction ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆
center_acts_by_scalar (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (m : M) : (self.ueaAction ↑z) m = chi z • m

Instances For

source

theorem schur_lie_module_scalar {k : Type u_3} [Field k] [IsAlgClosed k] {𝔤' : Type u_4} [LieRing 𝔤'] [LieAlgebra k 𝔤'] {M : Type u_5} [AddCommGroup M] [Module k M] [LieRingModule 𝔤' M] [LieModule k 𝔤' M] [Module.Finite k M] (hirr : LieModule.IsIrreducible k 𝔤' M) (T : Module.End k M) (hT : ∀ (x : 𝔤') (m : M), T ⁅x, m⁆ = ⁅x, T m⁆) :

∃ (c : k), ∀ (m : M), T m = c • m

source

theorem weyl_orbit_separation {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (mu nu : ↥Δ.𝔥 →ₗ[R] R) (h : ∀ (p : ↥wg.invariantSubalgebra), (evalWeight Δ mu) ↑p = (evalWeight Δ nu) ↑p) :

∃ (w : wg.W), nu = wg.dualAction w mu

source

theorem evalWeight_weyl_invariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (w : wg.W) (mu : ↥Δ.𝔥 →ₗ[R] R) (p : ↥wg.invariantSubalgebra) :

(evalWeight Δ (wg.dualAction w mu)) ↑p = (evalWeight Δ mu) ↑p

source

theorem evalHC_eq_evalWeight_comp_hcIso {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (evalHC : (↥Δ.𝔥 →ₗ[R] R) → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (hdef : ∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (evalHC mu) z = (evalWeight Δ (mu + wg.ρ)) ↑((chevalley_restriction_hc_iso Δ wg) z)) (mu : ↥Δ.𝔥 →ₗ[R] R) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) :

(evalHC mu) z = (evalWeight Δ (mu + wg.ρ)) ↑((chevalley_restriction_hc_iso Δ wg) z)

source

theorem infinitesimalCharacter_eq_iff_shiftedWeylOrbit {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (evalHC : (↥Δ.𝔥 →ₗ[R] R) → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₐ[R] R) (hdef : ∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), (evalHC mu) z = (evalWeight Δ (mu + wg.ρ)) ↑((chevalley_restriction_hc_iso Δ wg) z)) (mu nu : ↥Δ.𝔥 →ₗ[R] R) :

evalHC mu = evalHC nu ↔ ∃ (w : wg.W), nu = wg.shiftedAction w mu