inductive SL2IrredGKModule : Type

• finiteDim (n : ℕ) : SL2IrredGKModule
• principalSeries (ν : ℂ) (ε : ZMod 2) : SL2IrredGKModule
• discreteSeriesPlus (n : ℕ) (hn : n ≥ 2) : SL2IrredGKModule
• discreteSeriesMinus (n : ℕ) (hn : n ≥ 2) : SL2IrredGKModule
• limitDiscretePlus : SL2IrredGKModule
• limitDiscreteMinus : SL2IrredGKModule

def SL2IrredGKModule.kTypes : SL2IrredGKModule → Set ℤ

def SL2IrredGKModule.casimirEigenvalue : SL2IrredGKModule → ℂ

def GKModule.IsIsomorphicGK {𝔤 : 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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (M : GKModule 𝔤 K 𝔨 Ad V) (N : GKModule 𝔤 K 𝔨 Ad W) : Prop

theorem GKModule.IsIsomorphicGK.symm {𝔤 : 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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] {M : GKModule 𝔤 K 𝔨 Ad V} {N : GKModule 𝔤 K 𝔨 Ad W} (h : M.IsIsomorphicGK N) : N.IsIsomorphicGK M

theorem GKModule.IsIsomorphicGK.trans {𝔤 : 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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] {U : Type u_5} [AddCommGroup U] [Module ℂ U] [LieRingModule 𝔤 U] [LieModule ℂ 𝔤 U] {M : GKModule 𝔤 K 𝔨 Ad V} {N : GKModule 𝔤 K 𝔨 Ad W} {P : GKModule 𝔤 K 𝔨 Ad U} (h₁ : M.IsIsomorphicGK N) (h₂ : N.IsIsomorphicGK P) : M.IsIsomorphicGK P

structure SL2IrredGKModule.Realization (μ : SL2IrredGKModule) (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) : Type (max (max u_1 u_2) (u_3 + 1))

• W : Type u_3
• instAddCommGroup : AddCommGroup self.W
• instModule : Module ℂ self.W
• instLieRingModule : LieRingModule 𝔤 self.W
• instLieModule : LieModule ℂ 𝔤 self.W
• gkmod : GKModule 𝔤 K 𝔨 Ad self.W
• casimirScalar : ℂ
• casimir_eq : self.casimirScalar = μ.casimirEigenvalue

inductive KTypeBoundedness : Type

• boundedBoth : KTypeBoundedness
• unboundedBoth : KTypeBoundedness
• boundedBelow : KTypeBoundedness
• boundedAbove : KTypeBoundedness

noncomputable def sl2_lieRingModule_from_generators (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (W : Type u_2) [AddCommGroup W] [Module ℂ W] (ρ : 𝔤 →ₗ⁅ℂ⁆ Module.End ℂ W) : LieRingModule 𝔤 W

noncomputable def sl2_lieModule_from_generators (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (W : Type u_2) [AddCommGroup W] [Module ℂ W] (ρ : 𝔤 →ₗ⁅ℂ⁆ Module.End ℂ W) : LieModule ℂ 𝔤 W

theorem sl2_basis_exists (𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : ∃ (b : Module.Basis (Fin 3) ℂ 𝔤), b 0 = M_sl2.H ∧ b 1 = M_sl2.E ∧ b 2 = M_sl2.F

noncomputable def SL2GKModule.getBasis {𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : Module.Basis (Fin 3) ℂ 𝔤

theorem SL2GKModule.getBasis_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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : M_sl2.getBasis 0 = M_sl2.H

theorem SL2GKModule.getBasis_E {𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : M_sl2.getBasis 1 = M_sl2.E

theorem SL2GKModule.getBasis_F {𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : M_sl2.getBasis 2 = M_sl2.F

noncomputable def sl2_lieHom_from_generators (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (hb0 : b 0 = h) (hb1 : b 1 = e) (hb2 : b 2 = f_elem) (src_HE : ⁅h, e⁆ = 2 • e) (src_HF : ⁅h, f_elem⁆ = -2 • f_elem) (src_EF : ⁅e, f_elem⁆ = h) {W : Type u_2} [AddCommGroup W] [Module ℂ W] (ρH ρE ρF : Module.End ℂ W) (hHE : ρH ∘ₗ ρE - ρE ∘ₗ ρH = 2 • ρE) (hHF : ρH ∘ₗ ρF - ρF ∘ₗ ρH = -2 • ρF) (hEF : ρE ∘ₗ ρF - ρF ∘ₗ ρE = ρH) : 𝔤 →ₗ⁅ℂ⁆ Module.End ℂ W

noncomputable def sl2_adjoint_gkmod (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) [LieRingModule 𝔤 𝔤] [LieModule ℂ 𝔤 𝔤] (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) : GKModule 𝔤 K 𝔨 Ad 𝔤

noncomputable def sl2_model_gkmod_σ (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (W : Type u_3) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] : Representation ℂ K W

theorem sl2_model_gkmod_locallyFinite (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (W : Type u_3) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] : (sl2_model_gkmod_σ 𝔤 K 𝔨 Ad W).IsLocallyFinite

theorem sl2_model_gkmod_equivariance (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (W : Type u_3) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (k : K) (X : 𝔤) (v : W) : ((sl2_model_gkmod_σ 𝔤 K 𝔨 Ad W) k) ⁅X, v⁆ = ⁅(Ad k) X, ((sl2_model_gkmod_σ 𝔤 K 𝔨 Ad W) k) v⁆

noncomputable def sl2_model_gkmod (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (W : Type u_3) [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] : GKModule 𝔤 K 𝔨 Ad W

noncomputable def sl2_gk_ktype_boundedness (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) : KTypeBoundedness

theorem bddAbove_and_bddBelow_of_boundedBoth (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : BddAbove M_sl2.ktypeSet ∧ BddBelow M_sl2.ktypeSet

theorem irred_gkmod_nontrivial {𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) : Nontrivial V

theorem irred_sl2_admissible {𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (M : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) : M_sl2.IsAdmissible

theorem ktypeSet_nonempty_of_irred_admissible {𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) : M_sl2.ktypeSet.Nonempty

theorem ktypeSet_uniform_parity {𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (m : ℤ) : m ∈ M_sl2.ktypeSet → ∀ m' ∈ M_sl2.ktypeSet, m % 2 = m' % 2

theorem sl2_EF_recurrence {𝔤 : 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_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (n₀ : ℤ) (v : V) (hv : v ∈ M_sl2.weightSpace n₀) (hEv : ⁅M_sl2.E, v⁆ = 0) (k : ℕ) : ⁅M_sl2.E, SL2GKModule.iterLie M_sl2.F v (k + 1)⁆ = (↑(k + 1) * (↑n₀ - ↑k)) • SL2GKModule.iterLie M_sl2.F v k

theorem ktypeSet_max_nonneg {𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (S : Finset ℤ) (hS : ↑S = M_sl2.ktypeSet) (hne : S.Nonempty) : 0 ≤ S.max' hne

theorem sl2_gk_ktype_set_exists (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : ∃ (S : Finset ℤ), ↑S = M_sl2.ktypeSet ∧ S.Nonempty ∧ (∀ m ∈ S, ∀ m' ∈ S, m % 2 = m' % 2) ∧ ∃ (n : ℕ), ↑n ∈ S ∧ ∀ m ∈ S, m ≤ ↑n

noncomputable def sl2_gk_finiteDim_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : SL2IrredGKModule

noncomputable def sl2_finiteDim_ρH (n : ℕ) : (Fin (n + 1) → ℂ) →ₗ[ℂ] Fin (n + 1) → ℂ

noncomputable def sl2_finiteDim_ρE (n : ℕ) : (Fin (n + 1) → ℂ) →ₗ[ℂ] Fin (n + 1) → ℂ

noncomputable def sl2_finiteDim_ρF (n : ℕ) : (Fin (n + 1) → ℂ) →ₗ[ℂ] Fin (n + 1) → ℂ

theorem sl2_finiteDim_bracket_HE (n : ℕ) : sl2_finiteDim_ρH n ∘ₗ sl2_finiteDim_ρE n - sl2_finiteDim_ρE n ∘ₗ sl2_finiteDim_ρH n = 2 • sl2_finiteDim_ρE n

theorem sl2_finiteDim_bracket_HF (n : ℕ) : sl2_finiteDim_ρH n ∘ₗ sl2_finiteDim_ρF n - sl2_finiteDim_ρF n ∘ₗ sl2_finiteDim_ρH n = -2 • sl2_finiteDim_ρF n

theorem sl2_finiteDim_bracket_EF (n : ℕ) : sl2_finiteDim_ρE n ∘ₗ sl2_finiteDim_ρF n - sl2_finiteDim_ρF n ∘ₗ sl2_finiteDim_ρE n = sl2_finiteDim_ρH n

noncomputable def sl2_gk_finiteDim_realization (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : (sl2_gk_finiteDim_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad

theorem sl2_nonzero_gk_hom_of_irred_injective (𝔤 : 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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (M : GKModule 𝔤 K 𝔨 Ad V) (N : GKModule 𝔤 K 𝔨 Ad W) (hirr : M.IsIrreducibleGKModule) (φ : GKModuleHom M N) (hφ : φ.toLinearMap ≠ 0) : Function.Injective ⇑φ.toLinearMap

theorem sl2_finiteDim_highest_weight_hom (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : ∃ (φ : GKModuleHom M (sl2_gk_finiteDim_realization 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).gkmod), φ.toLinearMap ≠ 0

theorem sl2_finiteDim_gk_hom_surjective (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) (φ : GKModuleHom M (sl2_gk_finiteDim_realization 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).gkmod) (hφ_inj : Function.Injective ⇑φ.toLinearMap) : Function.Surjective ⇑φ.toLinearMap

theorem sl2_gk_finiteDim_iso (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : M.IsIsomorphicGK (sl2_gk_finiteDim_realization 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).gkmod

theorem sl2_gk_classification_finiteDim (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBoth) : ∃ (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod

noncomputable def principalSeries_ρH (ν : ℂ) (ε : ZMod 2) : (ℤ → ℂ) →ₗ[ℂ] ℤ → ℂ

noncomputable def principalSeries_ρE (ν : ℂ) (ε : ZMod 2) : (ℤ → ℂ) →ₗ[ℂ] ℤ → ℂ

noncomputable def principalSeries_ρF (ν : ℂ) (ε : ZMod 2) : (ℤ → ℂ) →ₗ[ℂ] ℤ → ℂ

theorem principalSeries_bracket_HE (ν : ℂ) (ε : ZMod 2) : principalSeries_ρH ν ε ∘ₗ principalSeries_ρE ν ε - principalSeries_ρE ν ε ∘ₗ principalSeries_ρH ν ε = 2 • principalSeries_ρE ν ε

theorem principalSeries_bracket_HF (ν : ℂ) (ε : ZMod 2) : principalSeries_ρH ν ε ∘ₗ principalSeries_ρF ν ε - principalSeries_ρF ν ε ∘ₗ principalSeries_ρH ν ε = -2 • principalSeries_ρF ν ε

theorem principalSeries_bracket_EF (ν : ℂ) (ε : ZMod 2) : principalSeries_ρE ν ε ∘ₗ principalSeries_ρF ν ε - principalSeries_ρF ν ε ∘ₗ principalSeries_ρE ν ε = principalSeries_ρH ν ε

noncomputable def sl2_gk_principalSeries_realization (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (bH : b 0 = h) (bE : b 1 = e) (bF : b 2 = f_elem) (hHE_src : ⁅h, e⁆ = 2 • e) (hHF_src : ⁅h, f_elem⁆ = -2 • f_elem) (hEF_src : ⁅e, f_elem⁆ = h) (ν : ℂ) (ε : ZMod 2) : (SL2IrredGKModule.principalSeries ν ε).Realization 𝔤 K 𝔨 Ad

opaque sl2_gk_principalSeries_params_exists (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : ℂ × ZMod 2

noncomputable def sl2_gk_principalSeries_nu (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : ℂ

noncomputable def sl2_gk_principalSeries_epsilon (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : ZMod 2

noncomputable def sl2_gk_principalSeries_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : SL2IrredGKModule

noncomputable def sl2_gk_principalSeries_realization_from_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : (sl2_gk_principalSeries_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad

theorem sl2_principalSeries_weight_space_hom (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) (R : (sl2_gk_principalSeries_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : ∃ (φ : GKModuleHom M R.gkmod), φ.toLinearMap ≠ 0

theorem sl2_principalSeries_gk_hom_surjective (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) (R : (sl2_gk_principalSeries_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) (φ : GKModuleHom M R.gkmod) (hφ_inj : Function.Injective ⇑φ.toLinearMap) : Function.Surjective ⇑φ.toLinearMap

theorem sl2_gk_principalSeries_iso (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) (R : (sl2_gk_principalSeries_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : M.IsIsomorphicGK R.gkmod

theorem sl2_gk_classification_principalSeries (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.unboundedBoth) : ∃ (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod

noncomputable def sl2_gk_discreteSeriesPlus_minKType_exists (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) : { n : ℕ // n ≥ 1 }

noncomputable def sl2_gk_discreteSeriesPlus_minKType (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) : ℕ

noncomputable def discreteSeriesPlus_ρH (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

noncomputable def discreteSeriesPlus_ρE (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

noncomputable def discreteSeriesPlus_ρF (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

theorem discreteSeriesPlus_bracket_HE (n : ℕ) : discreteSeriesPlus_ρH n ∘ₗ discreteSeriesPlus_ρE n - discreteSeriesPlus_ρE n ∘ₗ discreteSeriesPlus_ρH n = 2 • discreteSeriesPlus_ρE n

theorem discreteSeriesPlus_bracket_HF (n : ℕ) : discreteSeriesPlus_ρH n ∘ₗ discreteSeriesPlus_ρF n - discreteSeriesPlus_ρF n ∘ₗ discreteSeriesPlus_ρH n = -2 • discreteSeriesPlus_ρF n

theorem discreteSeriesPlus_bracket_EF (n : ℕ) : discreteSeriesPlus_ρE n ∘ₗ discreteSeriesPlus_ρF n - discreteSeriesPlus_ρF n ∘ₗ discreteSeriesPlus_ρE n = discreteSeriesPlus_ρH n

noncomputable def sl2_gk_discreteSeriesPlus_realization (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (bH : b 0 = h) (bE : b 1 = e) (bF : b 2 = f_elem) (hHE_src : ⁅h, e⁆ = 2 • e) (hHF_src : ⁅h, f_elem⁆ = -2 • f_elem) (hEF_src : ⁅e, f_elem⁆ = h) (n : ℕ) (hn : n ≥ 2) : (SL2IrredGKModule.discreteSeriesPlus n hn).Realization 𝔤 K 𝔨 Ad

noncomputable def sl2_gk_limitDiscretePlus_realization (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (bH : b 0 = h) (bE : b 1 = e) (bF : b 2 = f_elem) (hHE_src : ⁅h, e⁆ = 2 • e) (hHF_src : ⁅h, f_elem⁆ = -2 • f_elem) (hEF_src : ⁅e, f_elem⁆ = h) : SL2IrredGKModule.limitDiscretePlus.Realization 𝔤 K 𝔨 Ad

noncomputable def sl2_gk_discreteSeriesPlus_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) : SL2IrredGKModule

noncomputable def sl2_gk_discreteSeriesPlus_realization_from_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) : (sl2_gk_discreteSeriesPlus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad

theorem sl2_discreteSeriesPlus_lowest_weight_hom (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) (R : (sl2_gk_discreteSeriesPlus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : ∃ (φ : GKModuleHom M R.gkmod), φ.toLinearMap ≠ 0

theorem sl2_discreteSeriesPlus_gk_hom_surjective (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) (R : (sl2_gk_discreteSeriesPlus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) (φ : GKModuleHom M R.gkmod) (hφ_inj : Function.Injective ⇑φ.toLinearMap) : Function.Surjective ⇑φ.toLinearMap

theorem sl2_gk_discreteSeriesPlus_iso (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) (R : (sl2_gk_discreteSeriesPlus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : M.IsIsomorphicGK R.gkmod

theorem sl2_gk_classification_discreteSeriesPlus (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedBelow) : ∃ (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod

noncomputable def sl2_gk_discreteSeriesMinus_maxKType_exists (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) : { n : ℕ // n ≥ 1 }

noncomputable def sl2_gk_discreteSeriesMinus_maxKType (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) : ℕ

noncomputable def sl2_gk_discreteSeriesMinus_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) : SL2IrredGKModule

noncomputable def discreteSeriesMinus_ρH (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

noncomputable def discreteSeriesMinus_ρE (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

noncomputable def discreteSeriesMinus_ρF (n : ℕ) : (ℕ → ℂ) →ₗ[ℂ] ℕ → ℂ

theorem discreteSeriesMinus_bracket_HE (n : ℕ) : discreteSeriesMinus_ρH n ∘ₗ discreteSeriesMinus_ρE n - discreteSeriesMinus_ρE n ∘ₗ discreteSeriesMinus_ρH n = 2 • discreteSeriesMinus_ρE n

theorem discreteSeriesMinus_bracket_HF (n : ℕ) : discreteSeriesMinus_ρH n ∘ₗ discreteSeriesMinus_ρF n - discreteSeriesMinus_ρF n ∘ₗ discreteSeriesMinus_ρH n = -2 • discreteSeriesMinus_ρF n

theorem discreteSeriesMinus_bracket_EF (n : ℕ) : discreteSeriesMinus_ρE n ∘ₗ discreteSeriesMinus_ρF n - discreteSeriesMinus_ρF n ∘ₗ discreteSeriesMinus_ρE n = discreteSeriesMinus_ρH n

noncomputable def sl2_gk_discreteSeriesMinus_realization (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (bH : b 0 = h) (bE : b 1 = e) (bF : b 2 = f_elem) (hHE_src : ⁅h, e⁆ = 2 • e) (hHF_src : ⁅h, f_elem⁆ = -2 • f_elem) (hEF_src : ⁅e, f_elem⁆ = h) (n : ℕ) (hn : n ≥ 2) : (SL2IrredGKModule.discreteSeriesMinus n hn).Realization 𝔤 K 𝔨 Ad

noncomputable def sl2_gk_limitDiscreteMinus_realization (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [FiniteDimensional ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (hAd_lie : ∀ (k : K) (X Y : 𝔤), (Ad k) ⁅X, Y⁆ = ⁅(Ad k) X, (Ad k) Y⁆) (h e f_elem : 𝔤) (b : Module.Basis (Fin 3) ℂ 𝔤) (bH : b 0 = h) (bE : b 1 = e) (bF : b 2 = f_elem) (hHE_src : ⁅h, e⁆ = 2 • e) (hHF_src : ⁅h, f_elem⁆ = -2 • f_elem) (hEF_src : ⁅e, f_elem⁆ = h) : SL2IrredGKModule.limitDiscreteMinus.Realization 𝔤 K 𝔨 Ad

noncomputable def sl2_gk_discreteSeriesMinus_realization_from_label (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) : (sl2_gk_discreteSeriesMinus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad

theorem sl2_discreteSeriesMinus_highest_weight_hom (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) (R : (sl2_gk_discreteSeriesMinus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : ∃ (φ : GKModuleHom M R.gkmod), φ.toLinearMap ≠ 0

theorem sl2_discreteSeriesMinus_gk_hom_surjective (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) (R : (sl2_gk_discreteSeriesMinus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) (φ : GKModuleHom M R.gkmod) (hφ_inj : Function.Injective ⇑φ.toLinearMap) : Function.Surjective ⇑φ.toLinearMap

theorem sl2_gk_discreteSeriesMinus_iso (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) (R : (sl2_gk_discreteSeriesMinus_label 𝔤 K 𝔨 Ad V M hirr hadm M_sl2 hbdd).Realization 𝔤 K 𝔨 Ad) : M.IsIsomorphicGK R.gkmod

theorem sl2_gk_classification_discreteSeriesMinus (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hbdd : sl2_gk_ktype_boundedness 𝔤 K 𝔨 Ad V M M_sl2 hirr hadm = KTypeBoundedness.boundedAbove) : ∃ (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod

theorem sl2_gk_classification (𝔤 : 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 : GKModule 𝔤 K 𝔨 Ad V) (M_sl2 : SL2GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hadm : M.IsAdmissible) : ∃ (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod

theorem sl2IrredGKModule_realization_exists (μ : SL2IrredGKModule) (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) : Nonempty (μ.Realization 𝔤 K 𝔨 Ad)

theorem principalSeries_even_irreducible_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (R : (SL2IrredGKModule.principalSeries s 0).Realization 𝔤 K 𝔨 Ad) : R.gkmod.IsIrreducibleGKModule ↔ ¬∃ (k : ℤ), s = 2 * ↑k + 1

theorem principalSeries_odd_irreducible_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (R : (SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) : R.gkmod.IsIrreducibleGKModule ↔ ¬∃ (k : ℤ), s = 2 * ↑k

noncomputable def principalSeries_neg_map (c : ℤ → ℂ) : (ℤ → ℂ) →ₗ[ℂ] ℤ → ℂ

theorem principalSeries_neg_map_intertwine_H (c : ℤ → ℂ) (ν : ℂ) (ε : ZMod 2) : principalSeries_neg_map c ∘ₗ principalSeries_ρH ν ε = principalSeries_ρH (-ν) ε ∘ₗ principalSeries_neg_map c

def PrincipalSeries_neg_recurrence (c : ℤ → ℂ) (ν : ℂ) : Prop

theorem principalSeries_neg_map_intertwine_E (c : ℤ → ℂ) (ν : ℂ) (ε : ZMod 2) (hc : PrincipalSeries_neg_recurrence c ν) : principalSeries_neg_map c ∘ₗ principalSeries_ρE ν ε = principalSeries_ρE (-ν) ε ∘ₗ principalSeries_neg_map c

theorem principalSeries_neg_map_intertwine_F (c : ℤ → ℂ) (ν : ℂ) (ε : ZMod 2) (hc : PrincipalSeries_neg_recurrence c ν) : principalSeries_neg_map c ∘ₗ principalSeries_ρF ν ε = principalSeries_ρF (-ν) ε ∘ₗ principalSeries_neg_map c

theorem principalSeries_neg_iso {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (ε : ZMod 2) (R₁ : (SL2IrredGKModule.principalSeries s ε).Realization 𝔤 K 𝔨 Ad) (R₂ : (SL2IrredGKModule.principalSeries (-s) ε).Realization 𝔤 K 𝔨 Ad) : R₁.gkmod.IsIsomorphicGK R₂.gkmod

noncomputable def casimirEnd {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (H E F : 𝔤) : Module.End ℂ V

theorem casimirEnd_equivariant {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (φ : V →ₗ[ℂ] W) (hcomm : ∀ (X : 𝔤) (v : V), φ ⁅X, v⁆ = ⁅X, φ v⁆) (H E F : 𝔤) (v : V) : φ ((casimirEnd H E F) v) = (casimirEnd H E F) (φ v)

def casimirEigenvalues {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (H E F : 𝔤) : Set ℂ

theorem casimirEigenvalues_iso_invariant {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (φ : V →ₗ[ℂ] W) (hcomm : ∀ (X : 𝔤) (v : V), φ ⁅X, v⁆ = ⁅X, φ v⁆) (hbij : Function.Bijective ⇑φ) (H E F : 𝔤) : casimirEigenvalues H E F = casimirEigenvalues H E F

def kTypesWrtH {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (H : 𝔤) : Set ℤ

theorem kTypesWrtH_iso_invariant {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] {W : Type u_3} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (φ : V →ₗ[ℂ] W) (hcomm : ∀ (X : 𝔤) (v : V), φ ⁅X, v⁆ = ⁅X, φ v⁆) (hbij : Function.Bijective ⇑φ) (H : 𝔤) : kTypesWrtH H = kTypesWrtH H

noncomputable def sl2_canonical_H (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] : 𝔤

noncomputable def sl2_canonical_E (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] : 𝔤

noncomputable def sl2_canonical_F (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] : 𝔤

theorem sl2_casimir_match_at_canonical {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad) : casimirEigenvalues (sl2_canonical_H 𝔤) (sl2_canonical_E 𝔤) (sl2_canonical_F 𝔤) = {μ.casimirEigenvalue}

theorem realization_iso_casimir_eq {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (μ ν : SL2IrredGKModule) (Rμ : μ.Realization 𝔤 K 𝔨 Ad) (Rν : ν.Realization 𝔤 K 𝔨 Ad) (hiso : Rμ.gkmod.IsIsomorphicGK Rν.gkmod) : μ.casimirEigenvalue = ν.casimirEigenvalue

theorem sl2_kTypes_match_at_canonical_H {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (μ : SL2IrredGKModule) (R : μ.Realization 𝔤 K 𝔨 Ad) : kTypesWrtH (sl2_canonical_H 𝔤) = μ.kTypes

theorem realization_iso_kTypes_eq {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (μ ν : SL2IrredGKModule) (Rμ : μ.Realization 𝔤 K 𝔨 Ad) (Rν : ν.Realization 𝔤 K 𝔨 Ad) (hiso : Rμ.gkmod.IsIsomorphicGK Rν.gkmod) : μ.kTypes = ν.kTypes

theorem label_eq_of_invariants_match (μ ν : SL2IrredGKModule) (hcas : μ.casimirEigenvalue = ν.casimirEigenvalue) (hkt : μ.kTypes = ν.kTypes) : μ = ν ∨ ∃ (s : ℂ) (ε : ZMod 2), μ = SL2IrredGKModule.principalSeries s ε ∧ ν = SL2IrredGKModule.principalSeries (-s) ε

theorem sl2_iso_implies_label_match {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (μ ν : SL2IrredGKModule) (Rμ : μ.Realization 𝔤 K 𝔨 Ad) (Rν : ν.Realization 𝔤 K 𝔨 Ad) (hiso : Rμ.gkmod.IsIsomorphicGK Rν.gkmod) : μ = ν ∨ ∃ (s : ℂ) (ε : ZMod 2), μ = SL2IrredGKModule.principalSeries s ε ∧ ν = SL2IrredGKModule.principalSeries (-s) ε

theorem principalSeries_even_irreducible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (hs : ¬∃ (k : ℤ), s = 2 * ↑k + 1) (R : (SL2IrredGKModule.principalSeries s 0).Realization 𝔤 K 𝔨 Ad) : R.gkmod.IsIrreducibleGKModule

theorem principalSeries_even_reducible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (hs : ∃ (k : ℤ), s = 2 * ↑k + 1) (R : (SL2IrredGKModule.principalSeries s 0).Realization 𝔤 K 𝔨 Ad) : ¬R.gkmod.IsIrreducibleGKModule

theorem principalSeries_odd_irreducible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (hs : ¬∃ (k : ℤ), s = 2 * ↑k) (R : (SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) : R.gkmod.IsIrreducibleGKModule

theorem principalSeries_odd_reducible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} (s : ℂ) (hs : ∃ (k : ℤ), s = 2 * ↑k) (R : (SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) : ¬R.gkmod.IsIrreducibleGKModule