def DModulesII.IsSupportedOn {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (I : Ideal R) : Prop

def DModulesII.sheafSupport (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : Set (PrimeSpectrum R)

@[reducible]

def DModulesII.rModuleOf {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] : Module R M

def DModulesII.DModIsSupportedOn {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] (I : Ideal R) : Prop

@[reducible, inline]

abbrev DModulesII.DModSupportedPred {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (I : Ideal R) : CategoryTheory.ObjectProperty (ModuleCat D)

@[reducible, inline]

abbrev DModulesII.DModSupportedCat {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (I : Ideal R) : Type (max u_2 (u_3 + 1))

def DModulesII.annihilatedByIdeal {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (I : Ideal R) (M : Type u_3) [AddCommGroup M] [Module D M] : Set M

def DModulesII.annihilatedByIdealAddSubgroup {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (I : Ideal R) (M : Type u_3) [AddCommGroup M] [Module D M] : AddSubgroup M

def DModulesII.DModSheafSupport {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] : Set (PrimeSpectrum R)

class DModulesII.IsLeibnizCompatible {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] : Prop

• smul_torsion (d : D) (f : R) (m : M) (n : ℕ) : ι f ^ n • m = 0 → ∃ (N : ℕ), ι f ^ N • d • m = 0

theorem DModulesII.torsion_is_DSubmodule {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] [IsLeibnizCompatible ι M] (f : R) : ∃ (N : Submodule D M), ∀ (v : M), v ∈ N ↔ ∃ (n : ℕ), ι f ^ n • v = 0

theorem DModulesII.sheafSupport_subset_implies_supported {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] [IsSimpleModule D M] (I : Ideal R) (h : DModSheafSupport ι M ⊆ PrimeSpectrum.zeroLocus ↑I) : IsSupportedOn M I

theorem DModulesII.simple_DModule_support_preirreducible {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] [IsSimpleModule D M] [IsLeibnizCompatible ι M] (z₁ z₂ : Set (PrimeSpectrum R)) (hz₁ : IsClosed z₁) (hz₂ : IsClosed z₂) (hsub : DModSheafSupport ι M ⊆ z₁ ∪ z₂) : DModSheafSupport ι M ⊆ z₁ ∨ DModSheafSupport ι M ⊆ z₂

theorem DModulesII.irreducible_DModule_support_irreducible {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (M : Type u_3) [AddCommGroup M] [Module D M] [IsSimpleModule D M] [IsLeibnizCompatible ι M] : IsIrreducible (DModSheafSupport ι M)

class DModulesII.IsKashiwaraSetup {R : Type u_3} [CommRing R] {D : Type u_4} [Ring D] : (R →+* D) → (I : Ideal R) → (D' : Type u_5) → [inst : Ring D'] → (ι' : R ⧸ I →+* D') → Prop

• isSmooth_X : IsNoetherian R R
• isSmooth_Z : IsNoetherian (R ⧸ I) (R ⧸ I)
• ι'_injective : Function.Injective ⇑ι'

noncomputable def DModulesII.kashiwara_equiv {R : Type u_1} [CommRing R] {D : Type u_2} [Ring D] (ι : R →+* D) (D' : Type u_3) [Ring D'] (I : Ideal R) (ι' : R ⧸ I →+* D') [IsKashiwaraSetup ι I D' ι'] : DModSupportedCat ι I ≌ ModuleCat D'

structure DModulesII.QCohSheafData (k : Type u_sheaf) [Field k] : Type (u_sheaf + 1)

• affineIndex : Type u_sheaf
• coordRing : self.affineIndex → Type u_sheaf
• instCommRing (i : self.affineIndex) : CommRing (self.coordRing i)
• instAlgebra (i : self.affineIndex) : Algebra k (self.coordRing i)
• diffOpsRing : self.affineIndex → Type u_sheaf
• instDiffRing (i : self.affineIndex) : Ring (self.diffOpsRing i)
• sections : self.affineIndex → Type u_sheaf
• instAddCommGroup (i : self.affineIndex) : AddCommGroup (self.sections i)
• instModule (i : self.affineIndex) : Module (self.diffOpsRing i) (self.sections i)
• instModuleK (i : self.affineIndex) : Module k (self.sections i)

structure DModulesII.GEquivariantSheaf (k : Type u_sheaf) [Field k] (G : Type u_sheaf) [Group G] : Type (u_sheaf + 1)

• sheafData : QCohSheafData k
• mulAction : MulAction G self.sheafData.affineIndex
• phi (g : G) (i : self.sheafData.affineIndex) : self.sheafData.sections i ≃ₗ[k] self.sheafData.sections (g • i)
• cocycle (g h : G) (i : self.sheafData.affineIndex) (v : self.sheafData.sections i) : ⋯ ▸ (self.phi (g * h) i) v = (self.phi g (h • i)) ((self.phi h i) v)
• phi_one (i : self.sheafData.affineIndex) (v : self.sheafData.sections i) : ⋯ ▸ (self.phi 1 i) v = v

structure DModulesII.GEquivQCohSheaf (k : Type u_1) [Field k] (G : Type u_2) [Group G] (M : Type u_5) [AddCommGroup M] [Module k M] : Type (max u_2 u_5)

• groupAction : G →* M ≃ₗ[k] M

structure DModulesII.WeaklyEquivDModule (k : Type u_1) [Field k] (G : Type u_2) [Group G] (D : Type u_4) [Ring D] (M : Type u_5) [AddCommGroup M] [Module k M] [Module D M] extends DModulesII.GEquivQCohSheaf k G M : Type (max u_2 u_5)

• groupAction : G →* M ≃ₗ[k] M
• groupAction_DLinear (g : G) (d : D) (m : M) : (self.groupAction g) (d • m) = d • (self.groupAction g) m

structure DModulesII.EquivDModule (k : Type u_1) [Field k] (G : Type u_2) [Group G] (𝔤 : Type u_3) [LieRing 𝔤] [LieAlgebra k 𝔤] (D : Type u_4) [Ring D] [Algebra k D] (M : Type u_5) [AddCommGroup M] [Module k M] [Module D M] extends DModulesII.WeaklyEquivDModule k G D M : Type (max (max (max u_2 u_3) u_4) u_5)

• groupAction : G →* M ≃ₗ[k] M
• groupAction_DLinear (g : G) (d : D) (m : M) : (self.groupAction g) (d • m) = d • (self.groupAction g) m
• lieToD : 𝔤 →ₗ⁅k⁆ D
• lieAction_phi : 𝔤 →ₗ[k] Module.End k M
• actions_agree (x : 𝔤) (v : M) : (self.lieAction_phi x) v = self.lieToD x • v

def DModulesII.rho_phi (k : Type u_1) [Field k] (G : Type u_2) [Group G] (𝔤 : Type u_3) [LieRing 𝔤] [LieAlgebra k 𝔤] (D : Type u_4) [Ring D] [Algebra k D] {M : Type u_5} [AddCommGroup M] [Module k M] [Module D M] (_W : WeaklyEquivDModule k G D M) (lieAction_phi : 𝔤 →ₗ[k] Module.End k M) (lieToD : 𝔤 →ₗ⁅k⁆ D) (x : 𝔤) (v : M) : M

@[reducible, inline]

abbrev DModulesII.MonodromicDModule (k : Type u_1) [Field k] (T : Type u_5) [CommGroup T] (D' : Type u_6) [Ring D'] [Algebra k D'] (M : Type u_7) [AddCommGroup M] [Module k M] [Module D' M] : Type (max u_5 u_7)

def DModulesII.monodromic_rho_phi (k : Type u_1) [Field k] (G : Type u_2) [Group G] (𝔤 : Type u_3) [LieRing 𝔤] [LieAlgebra k 𝔤] (D : Type u_4) [Ring D] [Algebra k D] {M : Type u_5} [AddCommGroup M] [Module k M] [Module D M] (W : WeaklyEquivDModule k G D M) (lieAction_phi : 𝔤 →ₗ[k] Module.End k M) (lieToD : 𝔤 →ₗ⁅k⁆ D) (x : 𝔤) (v : M) : M

class DModulesII.IsDaffine (D : Type u_aag) [Ring D] (DXMod : Type u_1) [CategoryTheory.Category.{u_dxmod, u_1} DXMod] (X : Type u_2) : Prop

• isNoetherian_DX : IsNoetherian D D
• globalSections_equiv : Nonempty (DXMod ≌ ModuleCat D)

structure DModulesII.IsAffineAlgebraicGroup (G : Type u_aag) [Group G] : Prop

• fg : Group.FG G

class DModulesII.IsAntidominant {k' : Type u_1} [Field k'] (𝔥star : Type u_2) (posRoots : Set 𝔥star) (pairing : 𝔥star → 𝔥star → k') (lam : 𝔥star) : Prop

• not_pos_int_pairing (α : 𝔥star) : α ∈ posRoots → ¬∃ n > 0, pairing lam α = ↑n

def DModulesII.StrongKEquivDModPred (k : Type u_aag) [Field k] (K : Type u_aag) [Group K] (𝔨 : Type u_aag) [LieRing 𝔨] [LieAlgebra k 𝔨] (D : Type u_aag) [Ring D] [Algebra k D] (lieToD : 𝔨 →ₗ⁅k⁆ D) : CategoryTheory.ObjectProperty (ModuleCat D)

def DModulesII.CompatibleKActionPred (k : Type u_aag) [Field k] (K : Type u_aag) [Group K] (𝔨 : Type u_aag) [LieRing 𝔨] [LieAlgebra k 𝔨] (D : Type u_aag) [Ring D] [Algebra k D] (lieToD : 𝔨 →ₗ⁅k⁆ D) (Ad : K →* 𝔨 ≃ₗ[k] 𝔨) : CategoryTheory.ObjectProperty (ModuleCat D)

noncomputable def DModulesII.daffine_equivariant_equiv (k : Type u_aag) [Field k] (K : Type u_aag) [Group K] (𝔨 : Type u_aag) [LieRing 𝔨] [LieAlgebra k 𝔨] (D : Type u_aag) [Ring D] [Algebra k D] (DXMod : Type u_1) [CategoryTheory.Category.{u_dxmod, u_1} DXMod] (X : Type u_2) [IsDaffine D DXMod X] (hK : IsAffineAlgebraicGroup K) (lieToD : 𝔨 →ₗ⁅k⁆ D) (Ad : K →* 𝔨 ≃ₗ[k] 𝔨) : (StrongKEquivDModPred k K 𝔨 D lieToD).FullSubcategory ≌ (CompatibleKActionPred k K 𝔨 D lieToD Ad).FullSubcategory

structure DModulesII.BBLocalizationData (k' : Type u_aag) [Field k'] : Type (u_aag + 1)

• G : Type u_aag
• grpG : Group self.G
• K : Type u_aag
• grpK : Group self.K
• iK : self.K →* self.G
• 𝔤 : Type u_aag
• lieRing_𝔤 : LieRing self.𝔤
• lieAlg_𝔤 : LieAlgebra k' self.𝔤
• 𝔨 : Type u_aag
• lieRing_𝔨 : LieRing self.𝔨
• lieAlg_𝔨 : LieAlgebra k' self.𝔨
• ι𝔨 : self.𝔨 →ₗ⁅k'⁆ self.𝔤
• 𝔥 : Type u_aag
• lieRing_𝔥 : LieRing self.𝔥
• lieAlg_𝔥 : LieAlgebra k' self.𝔥
• ι𝔥 : self.𝔥 →ₗ⁅k'⁆ self.𝔤
• D : Type u_aag
• ring_D : Ring self.D
• alg_D : Algebra k' self.D
• lieToD : self.𝔤 →ₗ⁅k'⁆ self.D
• 𝔥star : Type u_aag
• add_𝔥star : AddCommGroup self.𝔥star
• mod_𝔥star : Module k' self.𝔥star
• duality : self.𝔥 →ₗ[k'] self.𝔥star →ₗ[k'] k'
• roots : Set self.𝔥star
• posRoots : Set self.𝔥star
• lam : self.𝔥star
• FlagVariety : Type u_aag
• isNoetherian_D : IsNoetherian self.D self.D
• aag_K : IsAffineAlgebraicGroup self.K
• Ad_K : self.K →* self.𝔨 ≃ₗ[k'] self.𝔨

noncomputable def DModulesII.BBLocalizationData.DlambdaMod {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : Type u_aag

@[implicit_reducible]

noncomputable instance DModulesII.BBLocalizationData.instCatDlambdaMod {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : CategoryTheory.Category.{u_aag, u_aag} bd.DlambdaMod

@[implicit_reducible]

noncomputable instance DModulesII.instCategoryDlambdaMod {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : CategoryTheory.Category.{u_aag, u_aag} bd.DlambdaMod

def DModulesII.BBLocalizationData.IsAntidominant {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : Prop

def DModulesII.IsKEquivDModBB {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : CategoryTheory.ObjectProperty (ModuleCat bd.D)

def DModulesII.IsGKModBB {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : CategoryTheory.ObjectProperty (ModuleCat bd.D)

theorem DModulesII.isKEquivDModBB_eq_strongKEquivDModPred {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : IsKEquivDModBB bd = StrongKEquivDModPred k' bd.K bd.𝔨 bd.D (bd.lieToD.comp bd.ι𝔨)

theorem DModulesII.isGKModBB_eq_compatibleKActionPred {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') : IsGKModBB bd = CompatibleKActionPred k' bd.K bd.𝔨 bd.D (bd.lieToD.comp bd.ι𝔨) bd.Ad_K

noncomputable def DModulesII.antidominant_globalSections_equiv {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') (h : bd.IsAntidominant) : bd.DlambdaMod ≌ ModuleCat bd.D

theorem DModulesII.antidominant_implies_daffine {k' : Type u_aag} [Field k'] (bd : BBLocalizationData k') (h : bd.IsAntidominant) : IsDaffine bd.D bd.DlambdaMod bd.FlagVariety

noncomputable def DModulesII.beilinsonBernstein_equivariant_equiv (k : Type u_aag) [Field k] (bd : BBLocalizationData k) (h : bd.IsAntidominant) : (IsKEquivDModBB bd).FullSubcategory ≌ (IsGKModBB bd).FullSubcategory