Atlas.LieGroups.code.KTypeDecomposition

source

structure SL2GKModule (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤) (V : Type u_3) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] extends GKModule 𝔤 K 𝔨 Ad V :

Type (max (max u_1 u_2) u_3)

σ : Representation ℂ K V
locallyFinite : self.σ.IsLocallyFinite
diffσ : ↥𝔨 →ₗ[ℂ ] V →ₗ[ℂ ] V
diff_eq_lie (X : ↥𝔨) (v : V) : (self.diffσ X) v = ⁅↑X, v⁆
equivariance (k : K) (X : 𝔤) (v : V) : (self.σ k) ⁅X, v⁆ = ⁅(Ad k) X, (self.σ k) v⁆
H : 𝔤
E : 𝔤
F : 𝔤
bracket_HE : ⁅self.H, self.E⁆ = 2 • self.E
bracket_HF : ⁅self.H, self.F⁆ = -2 • self.F
bracket_EF : ⁅self.E, self.F⁆ = self.H
sl2_span (X : 𝔤) : ∃ (a : ℂ) (b : ℂ) (c : ℂ), X = a • self.H + b • self.E + c • self.F
K_centralizes (k : K) : (Ad k) self.H = self.H

Instances For

source

def SL2GKModule.hEnd {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) :

Module.End ℂ V

Instances For

source

def SL2GKModule.weightSpace {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) :

Submodule ℂ V

Instances For

source

theorem SL2GKModule.mem_weightSpace_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) :

v ∈ M.weightSpace n ↔ ⁅M.H, v⁆ = ↑n • v

source

theorem SL2GKModule.H_acts_as_scalar_on_weight_space {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) :

⁅M.H, v⁆ = ↑n • v

source

theorem SL2GKModule.E_shifts_weight {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) :

⁅M.E, v⁆ ∈ M.weightSpace (n + 2)

source

theorem SL2GKModule.F_shifts_weight {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) :

⁅M.F, v⁆ ∈ M.weightSpace (n - 2)

source

theorem SL2GKModule.weightSpaceDecomposition {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_5} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_6} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (hAdm : M.IsAdmissible) :

⨆ (n : ℤ), M.weightSpace n = ⊤

source

def SL2GKModule.iterLie {𝔤 : Type u_1} [LieRing 𝔤] {V : Type u_3} [AddCommGroup V] [LieRingModule 𝔤 V] (X : 𝔤) (v : V) :

ℕ → V

Instances For

source

@[simp]

theorem SL2GKModule.iterLie_zero {𝔤 : Type u_1} [LieRing 𝔤] {V : Type u_3} [AddCommGroup V] [LieRingModule 𝔤 V] (X : 𝔤) (v : V) :

iterLie X v 0 = v

source

@[simp]

theorem SL2GKModule.iterLie_succ {𝔤 : Type u_1} [LieRing 𝔤] {V : Type u_3} [AddCommGroup V] [LieRingModule 𝔤 V] (X : 𝔤) (v : V) (k : ℕ) :

iterLie X v (k + 1) = ⁅X, iterLie X v k⁆

source

theorem SL2GKModule.iterLie_E_weight_shift {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) (k : ℕ) :

iterLie M.E v k ∈ M.weightSpace (n + 2 * ↑k)

source

theorem SL2GKModule.iterLie_F_weight_shift {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) (k : ℕ) :

iterLie M.F v k ∈ M.weightSpace (n - 2 * ↑k)

source

theorem SL2GKModule.pbw_spanning {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_5} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_6} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (hIrr : M.IsIrreducibleGKModule) (hAdm : M.IsAdmissible) (n : ℤ) (v : V) (hv : v ∈ M.weightSpace n) (hv_ne : v ≠ 0) :

Submodule.span ℂ (Set.range (iterLie M.E v) ∪ Set.range (iterLie M.F v)) = ⊤

source

theorem SL2GKModule.submodule_eq_of_le_sup_disjoint {V : Type u_3} [AddCommGroup V] [Module ℂ V] (A B C : Submodule ℂ V) (hB_le_A : B ≤ A) (hBC_top : B ⊔ C = ⊤) (hAC_bot : A ⊓ C = ⊥) :

A = B

source

theorem SL2GKModule.eigenspace_inf_span_other_eq_bot {V : Type u_3} [AddCommGroup V] [Module ℂ V] (f : Module.End ℂ V) (μ : ℂ) (S : Set V) (hS : ∀ s ∈ S, ∃ (m : ℂ), m ≠ μ ∧ s ∈ f.eigenspace m) :

f.eigenspace μ ⊓ Submodule.span ℂ S = ⊥

source

theorem SL2GKModule.pbw_weight_space_proportional {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_5} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_6} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (hIrr : M.IsIrreducibleGKModule) (hAdm : M.IsAdmissible) (n : ℤ) (v w : V) (hv : v ∈ M.weightSpace n) (hw : w ∈ M.weightSpace n) (hv_ne : v ≠ 0) :

∃ (c : ℂ), w = c • v

source

def SL2GKModule.ktypeSet {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) :

Set ℤ

Instances For

source

theorem SL2GKModule.sl2_generates {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (X : 𝔤) :

∃ (a : ℂ) (b : ℂ) (c : ℂ), X = a • M.H + b • M.E + c • M.F

source

theorem SL2GKModule.K_centralizes_H {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (k : K) :

(Ad k) M.H = M.H

source

theorem SL2GKModule.K_preserves_weightSpace {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (j : ℤ) (k : K) (v : V) (hv : v ∈ M.weightSpace j) :

(M.σ k) v ∈ M.weightSpace j

source

theorem SL2GKModule.lie_action_preserves_parity_submodule {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (hAdm : M.IsAdmissible) (n₀ : ℤ) (X : 𝔤) (v : V) (j : ℤ) (hv : v ∈ M.weightSpace j) (hparity : ∃ (k : ℤ), j = n₀ + 2 * k) :

⁅X, v⁆ ∈ ⨆ (k : ℤ), M.weightSpace (n₀ + 2 * k)

source

theorem SL2GKModule.pbw_weight_same_parity {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_5} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ ] 𝔤} {V : Type u_6} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) (hIrr : M.IsIrreducibleGKModule) (hAdm : M.IsAdmissible) (n m : ℤ) (hn : n ∈ M.ktypeSet) (hm : m ∈ M.ktypeSet) :

Even n ↔ Even m

source

theorem sl2_linearIndependent :

LinearIndependent ℂ ![sl2H , sl2E , sl2F ]

source

noncomputable def sl2Basis :

Module.Basis (Fin 3) ℂ ↥sl2C

Instances For