structure SmoothVarietyWithGroupAction : Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))

• X : Type u_1
• K : Type u_2
• grpK : Group self.K
• topK : TopologicalSpace self.K
• connK : ConnectedSpace self.K
• actKX : MulAction self.K self.X
• DX : Type u_3
• ringDX : Ring self.DX
• algebraDX : Algebra ℂ self.DX
• actKDX : MulAction self.K self.DX
• orbits : Set (Set self.X)
• orbit_is_orbit (O : Set self.X) : O ∈ self.orbits → O.Nonempty ∧ ∀ x ∈ O, ∀ (k : self.K), k • x ∈ O
• orbits_cover (x : self.X) : ∃ O ∈ self.orbits, x ∈ O
• orbits_disjoint (O₁ : Set self.X) : O₁ ∈ self.orbits → ∀ O₂ ∈ self.orbits, O₁ ≠ O₂ → Disjoint O₁ O₂
• orbits_finite : self.orbits.Finite

def SmoothVarietyWithGroupAction.stabilizer (S : SmoothVarietyWithGroupAction) (x : S.X) : Subgroup S.K

structure OrbitRepPair (S : SmoothVarietyWithGroupAction) : Type (max (max (max (u_1 + 1) (u_2 + 1)) u_3) u_4)

• orbit : Set S.X
• orbit_mem : self.orbit ∈ S.orbits
• basepoint : S.X
• basepoint_mem : self.basepoint ∈ self.orbit
• ComponentGroup : Type u_1
• compGrpGroup : Group self.ComponentGroup
• quotientMap : ↥(MulAction.stabilizer S.K self.basepoint) →* self.ComponentGroup
• quotientMap_surjective : Function.Surjective ⇑self.quotientMap
• V : Type u_2
• addCommGroupV : AddCommGroup self.V
• moduleV : Module ℂ self.V
• compGroupRep : Representation ℂ self.ComponentGroup self.V
• V_irreducible : self.compGroupRep.IsIrreducible

structure IrredKEquivDModule (S : SmoothVarietyWithGroupAction) : Type (max (max (u_1 + 1) u_3) u_4)

• carrier : Type u_1
• addCommGroup : AddCommGroup self.carrier
• moduleC : Module ℂ self.carrier
• moduleDX : Module S.DX self.carrier
• mulActionK : MulAction S.K self.carrier
• equivariance (k : S.K) (d : S.DX) (m : self.carrier) : k • d • m = (k • d) • k • m
• isIrreducible : IsSimpleModule S.DX self.carrier

def IrredKEquivDModule.IsIsomorphic (S : SmoothVarietyWithGroupAction) (M : IrredKEquivDModule S) (N : IrredKEquivDModule S) : Prop

theorem kashiwarasTheorem (S : SmoothVarietyWithGroupAction) (M : IrredKEquivDModule S) (O : Set S.X) (hO : O ∈ S.orbits) : ∃ (restrict : IrredKEquivDModule S → IrredKEquivDModule S) (extend : IrredKEquivDModule S → IrredKEquivDModule S), (∀ (N : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S (extend (restrict N)) N) ∧ ∀ (L : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S (restrict (extend L)) L

noncomputable def associatedBundleDModule (S : SmoothVarietyWithGroupAction) (O : Set S.X) (hO : O ∈ S.orbits) (x : S.X) (hx : x ∈ O) (ComponentGroup : Type u_1) [Group ComponentGroup] (quotientMap : ↥(MulAction.stabilizer S.K x) →* ComponentGroup) (hSurj : Function.Surjective ⇑quotientMap) (V : Type u_2) [AddCommGroup V] [Module ℂ V] (compGroupRep : Representation ℂ ComponentGroup V) (hIrred : compGroupRep.IsIrreducible) : IrredKEquivDModule S

@[reducible, inline]

noncomputable abbrev associated_bundle_dmodule (S : SmoothVarietyWithGroupAction) (O : Set S.X) (hO : O ∈ S.orbits) (x : S.X) (hx : x ∈ O) (ComponentGroup : Type u_4) [Group ComponentGroup] (quotientMap : ↥(MulAction.stabilizer S.K x) →* ComponentGroup) (hSurj : Function.Surjective ⇑quotientMap) (V : Type u_5) [AddCommGroup V] [Module ℂ V] (compGroupRep : Representation ℂ ComponentGroup V) (hIrred : compGroupRep.IsIrreducible) : IrredKEquivDModule S

@[reducible, inline]

abbrev kashiwaras_theorem (S : SmoothVarietyWithGroupAction) (M : IrredKEquivDModule S) (O : Set S.X) (hO : O ∈ S.orbits) : ∃ (restrict : IrredKEquivDModule S → IrredKEquivDModule S) (extend : IrredKEquivDModule S → IrredKEquivDModule S), (∀ (N : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S (extend (restrict N)) N) ∧ ∀ (L : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S (restrict (extend L)) L

theorem associatedBundleDModule_support_orbit (S : SmoothVarietyWithGroupAction) (p : OrbitRepPair S) (inSupport : Set S.X → Prop) : inSupport p.orbit → ∀ O ∈ S.orbits, inSupport O → O = p.orbit

theorem associatedBundleDModule_injective (S : SmoothVarietyWithGroupAction) (p₁ p₂ : OrbitRepPair S) (h : associatedBundleDModule S p₁.orbit ⋯ p₁.basepoint ⋯ p₁.ComponentGroup p₁.quotientMap ⋯ p₁.V p₁.compGroupRep ⋯ = associatedBundleDModule S p₂.orbit ⋯ p₂.basepoint ⋯ p₂.ComponentGroup p₂.quotientMap ⋯ p₂.V p₂.compGroupRep ⋯) : p₁ = p₂

theorem associatedBundleDModule_surjective (S : SmoothVarietyWithGroupAction) (M : IrredKEquivDModule S) : ∃ (p : OrbitRepPair S), IrredKEquivDModule.IsIsomorphic S M (associatedBundleDModule S p.orbit ⋯ p.basepoint ⋯ p.ComponentGroup p.quotientMap ⋯ p.V p.compGroupRep ⋯)

theorem theorem_31_1 (S : SmoothVarietyWithGroupAction) : ∃ (param : OrbitRepPair S → IrredKEquivDModule S), Function.Injective param ∧ ∀ (M : IrredKEquivDModule S), ∃ (p : OrbitRepPair S), IrredKEquivDModule.IsIsomorphic S M (param p)

structure HarishChandraData : Type (max (max (max (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1)) (u_6 + 1))

• G : Type u_1
• grpG : Group self.G
• K : Type u_2
• grpK : Group self.K
• 𝔤 : Type u_3
• lieRing𝔤 : LieRing self.𝔤
• lieAlgebra𝔤 : LieAlgebra ℂ self.𝔤
• 𝓕 : Type u_4
• actK𝓕 : MulAction self.K self.𝓕
• W : Type u_5
• grpW : Group self.W
• fintypeW : Fintype self.W
• Z_Ug : Type u_6
• commRingZ : CommRing self.Z_Ug
• algebraZ : Algebra ℂ self.Z_Ug
• dotActionW : MulAction self.W (self.Z_Ug →ₐ[ℂ] ℂ)
• antidominance_pred : (self.Z_Ug →ₐ[ℂ] ℂ) → Prop

def HarishChandraData.IsRegularChar (D : HarishChandraData) (χ : D.Z_Ug →ₐ[ℂ] ℂ) : Prop

class HarishChandraData.IsAntidominantChar (D : HarishChandraData) (χ : D.Z_Ug →ₐ[ℂ] ℂ) : Prop

• antidominant_rep_exists : D.antidominance_pred χ

theorem prop_31_3 (D : HarishChandraData) : Finite (MulAction.orbitRel.Quotient D.K D.𝓕)

structure HCGKModule (D : HarishChandraData) : Type (max (max (max (u_1 + 1) u_3) u_4) u_7)

• carrier : Type u_1
• addCommGroup : AddCommGroup self.carrier
• module : Module ℂ self.carrier
• lieRingModule : LieRingModule D.𝔤 self.carrier
• lieModule : LieModule ℂ D.𝔤 self.carrier
• mulAction : MulAction D.K self.carrier
• χ : D.Z_Ug →ₐ[ℂ] ℂ

def HCGKModule.IsGKSubmodule {D : HarishChandraData} (M : HCGKModule D) (W : Submodule ℂ M.carrier) : Prop

def HCGKModule.IsIrreducible {D : HarishChandraData} (M : HCGKModule D) : Prop

structure HCClassifyingDatum (D : HarishChandraData) : Type (max (max (max (u_1 + 1) u_3) u_4) u_5)

• basepoint : D.𝓕
• orbit : Set D.𝓕
• orbit_eq : self.orbit = MulAction.orbit D.K self.basepoint
• K_x : Subgroup D.K
• K_x_eq : self.K_x = MulAction.stabilizer D.K self.basepoint
• V : Type u_1
• addCommGroupV : AddCommGroup self.V
• moduleV : Module ℂ self.V
• stabRep : Representation ℂ (↥self.K_x) self.V
• V_irreducible : self.stabRep.IsIrreducible
• lieKx : LieSubalgebra ℂ D.𝔤
• char_lieKx : D.𝔤 →ₗ[ℂ] ℂ
• lieKx_action : ↥self.lieKx →ₗ[ℂ] self.V →ₗ[ℂ] self.V
• char_lieKx_acts (X : ↥self.lieKx) (v : self.V) : (self.lieKx_action X) v = self.char_lieKx ↑X • v

theorem twistedDModuleClassification (D : HarishChandraData) (S : SmoothVarietyWithGroupAction) (hFlagVar : S.X = D.𝓕) (hGroupActs : S.K = D.K) : ∃ (M_assign : HCClassifyingDatum D → IrredKEquivDModule S), (∀ (d₁ d₂ : HCClassifyingDatum D), IrredKEquivDModule.IsIsomorphic S (M_assign d₁) (M_assign d₂) → d₁ = d₂) ∧ ∀ (M : IrredKEquivDModule S), ∃ (d : HCClassifyingDatum D), IrredKEquivDModule.IsIsomorphic S M (M_assign d)

theorem bbGlobalSectionsEquiv (D : HarishChandraData) (χ : D.Z_Ug →ₐ[ℂ] ℂ) (hχ : D.IsAntidominantChar χ) (S : SmoothVarietyWithGroupAction) (hFlagVar : S.X = D.𝓕) (hGroupActs : S.K = D.K) : ∃ (Γ_fun : IrredKEquivDModule S → HCGKModule D) (Loc_fun : HCGKModule D → IrredKEquivDModule S), (∀ (M : IrredKEquivDModule S), (Γ_fun M).χ = χ) ∧ (∀ (M : IrredKEquivDModule S), (Γ_fun M).IsIrreducible) ∧ (∀ (V : HCGKModule D), V.χ = χ → Nonempty (V.carrier ≃ₗ[ℂ] (Γ_fun (Loc_fun V)).carrier)) ∧ (∀ (M : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S (Loc_fun (Γ_fun M)) M) ∧ (∀ (M₁ M₂ : IrredKEquivDModule S), Γ_fun M₁ = Γ_fun M₂ → IrredKEquivDModule.IsIsomorphic S M₁ M₂) ∧ (∀ (V : HCGKModule D), V.IsIrreducible → V.χ = χ → ∃ (M : IrredKEquivDModule S), Nonempty (V.carrier ≃ₗ[ℂ] (Γ_fun M).carrier)) ∧ (∀ (M₁ M₂ : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S M₁ M₂ → Nonempty ((Γ_fun M₁).carrier ≃ₗ[ℂ] (Γ_fun M₂).carrier)) ∧ ∀ (M : IrredKEquivDModule S), Nonempty (M.carrier ≃ₗ[ℂ] (Γ_fun M).carrier)

theorem bbEquivWithDModuleRealization (D : HarishChandraData) (χ : D.Z_Ug →ₐ[ℂ] ℂ) (_hχ_reg : D.IsRegularChar χ) [hχ_ad : D.IsAntidominantChar χ] (S : SmoothVarietyWithGroupAction) (hFlagVar : S.X = D.𝓕) (hGroupActs : S.K = D.K) : ∃ (M_assign : HCClassifyingDatum D → IrredKEquivDModule S) (Γ_fun : IrredKEquivDModule S → HCGKModule D), (∀ (d₁ d₂ : HCClassifyingDatum D), IrredKEquivDModule.IsIsomorphic S (M_assign d₁) (M_assign d₂) → d₁ = d₂) ∧ (∀ (M : IrredKEquivDModule S), ∃ (d : HCClassifyingDatum D), IrredKEquivDModule.IsIsomorphic S M (M_assign d)) ∧ (∀ (M : IrredKEquivDModule S), (Γ_fun M).IsIrreducible ∧ (Γ_fun M).χ = χ) ∧ (∀ (M₁ M₂ : IrredKEquivDModule S), Γ_fun M₁ = Γ_fun M₂ → IrredKEquivDModule.IsIsomorphic S M₁ M₂) ∧ (∀ (V : HCGKModule D), V.IsIrreducible → V.χ = χ → ∃ (M : IrredKEquivDModule S), Nonempty (V.carrier ≃ₗ[ℂ] (Γ_fun M).carrier)) ∧ (∀ (M₁ M₂ : IrredKEquivDModule S), IrredKEquivDModule.IsIsomorphic S M₁ M₂ → Nonempty ((Γ_fun M₁).carrier ≃ₗ[ℂ] (Γ_fun M₂).carrier)) ∧ ∀ (M : IrredKEquivDModule S), Nonempty (M.carrier ≃ₗ[ℂ] (Γ_fun M).carrier)

theorem thm_31_4 (D : HarishChandraData) (χ : D.Z_Ug →ₐ[ℂ] ℂ) (hχ_reg : D.IsRegularChar χ) [hχ_ad : D.IsAntidominantChar χ] (S : SmoothVarietyWithGroupAction) (hFlagVar : S.X = D.𝓕) (hGroupActs : S.K = D.K) : ∃ (M_DModule : HCClassifyingDatum D → IrredKEquivDModule S) (π : HCClassifyingDatum D → HCGKModule D), (∀ (d : HCClassifyingDatum D), (π d).IsIrreducible ∧ (π d).χ = χ) ∧ Function.Injective π ∧ (∀ (M : HCGKModule D), M.IsIrreducible → M.χ = χ → ∃ (d : HCClassifyingDatum D), Nonempty (M.carrier ≃ₗ[ℂ] (π d).carrier)) ∧ (∀ (d₁ d₂ : HCClassifyingDatum D), IrredKEquivDModule.IsIsomorphic S (M_DModule d₁) (M_DModule d₂) → d₁ = d₂) ∧ ∀ (d : HCClassifyingDatum D), Nonempty ((M_DModule d).carrier ≃ₗ[ℂ] (π d).carrier)