Documentation

Atlas.LieGroups.code.SL2Classification

source
theorem SL2IrredGKModule.Realization.exists' (μ : SL2IrredGKModule) (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) :
Nonempty (μ.Realization 𝔤 K 𝔨 Ad)
source
theorem GKModule.isIrreducibleGKModule_of_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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] {M : GKModule 𝔤 K 𝔨 Ad V} {N : GKModule 𝔤 K 𝔨 Ad W} (hiso : M.IsIsomorphicGK N) (hirr : M.IsIrreducibleGKModule) :
N.IsIrreducibleGKModule
source
def IsOddInteger (s : ℂ) :
Prop
Instances For
    source
    def IsEvenInteger (s : ℂ) :
    Prop
    Instances For
      source
      inductive SL2SimpleModule :
      Type
      Instances For
        source
        def SL2SimpleModule.kTypes :
        SL2SimpleModule → Set ℤ
        Instances For
          source
          noncomputable def SL2SimpleModule.casimirEigenvalue :
          SL2SimpleModule → ℂ
          Instances For
            source
            def SL2SimpleModule.IsIsomorphic :
            SL2SimpleModule → SL2SimpleModule → Prop
            Instances For
              source
              theorem sl2_classification_existence (𝔤 : 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) :
              ∃ (μ : SL2SimpleModule) (R : (match μ with | SL2SimpleModule.finiteDim m => SL2IrredGKModule.finiteDim m | SL2SimpleModule.discreteSeriesMinus m _hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesMinus m h2 else SL2IrredGKModule.limitDiscreteMinus | SL2SimpleModule.discreteSeriesPlus m _hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesPlus m h2 else SL2IrredGKModule.limitDiscretePlus | SL2SimpleModule.principalSeriesEven s hs => SL2IrredGKModule.principalSeries s 0 | SL2SimpleModule.principalSeriesOdd s hs => SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad), M.IsIsomorphicGK R.gkmod
              source
              theorem sl2_principalSeriesEven_neg_iso (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (s : ℂ) (hs : ¬IsOddInteger s) (hs' : ¬IsOddInteger (-s)) (R₁ : (SL2IrredGKModule.principalSeries s 0).Realization 𝔤 K 𝔨 Ad) (R₂ : (SL2IrredGKModule.principalSeries (-s) 0).Realization 𝔤 K 𝔨 Ad) :
              R₁.gkmod.IsIsomorphicGK R₂.gkmod
              source
              theorem sl2_principalSeriesOdd_neg_iso (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (s : ℂ) (hs : ¬IsEvenInteger s) (hs' : ¬IsEvenInteger (-s)) (R₁ : (SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) (R₂ : (SL2IrredGKModule.principalSeries (-s) 1).Realization 𝔤 K 𝔨 Ad) :
              R₁.gkmod.IsIsomorphicGK R₂.gkmod
              source
              def SL2SimpleModule.toIrredGK :
              SL2SimpleModule → SL2IrredGKModule
              Instances For
                source
                theorem sl2_classification_uniqueness (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (μ ν : SL2SimpleModule) (Rμ : (match μ with | SL2SimpleModule.finiteDim m => SL2IrredGKModule.finiteDim m | SL2SimpleModule.discreteSeriesMinus m hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesMinus m h2 else SL2IrredGKModule.limitDiscreteMinus | SL2SimpleModule.discreteSeriesPlus m hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesPlus m h2 else SL2IrredGKModule.limitDiscretePlus | SL2SimpleModule.principalSeriesEven s hs => SL2IrredGKModule.principalSeries s 0 | SL2SimpleModule.principalSeriesOdd s hs => SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) (Rν : (match ν with | SL2SimpleModule.finiteDim m => SL2IrredGKModule.finiteDim m | SL2SimpleModule.discreteSeriesMinus m hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesMinus m h2 else SL2IrredGKModule.limitDiscreteMinus | SL2SimpleModule.discreteSeriesPlus m hm => if h2 : m ≥ 2 then SL2IrredGKModule.discreteSeriesPlus m h2 else SL2IrredGKModule.limitDiscretePlus | SL2SimpleModule.principalSeriesEven s hs => SL2IrredGKModule.principalSeries s 0 | SL2SimpleModule.principalSeriesOdd s hs => SL2IrredGKModule.principalSeries s 1).Realization 𝔤 K 𝔨 Ad) (hiso : Rμ.gkmod.IsIsomorphicGK Rν.gkmod) :
                μ.IsIsomorphic ν