structure BeilinsonBernstein.SmoothAlgVariety : Type (u + 1)

• carrier : Type u

structure BeilinsonBernstein.CAlgebra : Type (u + 1)

• carrier : Type u
• instRing : Ring self.carrier
• instAlgebra : Algebra ℂ self.carrier

structure BeilinsonBernstein.AbCat : Type (u + 1)

• Obj : Type u
• instCat : CategoryTheory.Category.{u, u} self.Obj

structure BeilinsonBernstein.GradedAlgebra : Type (u + 1)

• carrier : Type u
• instRing : Ring self.carrier
• instAlgebra : Algebra ℂ self.carrier

def BeilinsonBernstein.filtPred {α : Type u_1} [AddCommMonoid α] [Module ℂ α] (F : ℕ → Submodule ℂ α) : ℕ → Submodule ℂ α

class BeilinsonBernstein.IsDaffine (X : SmoothAlgVariety) (DMod DXMod : AbCat) (Gamma : CategoryTheory.Functor DMod.Obj DXMod.Obj) (Loc : CategoryTheory.Functor DXMod.Obj DMod.Obj) : Prop

• equiv : ∃ (e : DMod.Obj ≌ DXMod.Obj), e.functor = Gamma ∧ e.inverse = Loc

noncomputable def BeilinsonBernstein.AlgHom.liftOfSurjectiveNC {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (π : A →ₐ[R] B) (hπ : Function.Surjective ⇑π) (f : A →ₐ[R] C) (hker : ∀ (x : A), π x = 0 → f x = 0) : B →ₐ[R] C

theorem BeilinsonBernstein.AlgHom.liftOfSurjectiveNC_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (π : A →ₐ[R] B) (hπ : Function.Surjective ⇑π) (f : A →ₐ[R] C) (hker : ∀ (x : A), π x = 0 → f x = 0) (x : A) : (liftOfSurjectiveNC π hπ f hker) (π x) = f x

structure BeilinsonBernstein.BBDataZero : Type (u + 1)

• gLie : Type u
• instLieRing : LieRing self.gLie
• instLieAlgebra : LieAlgebra ℂ self.gLie
• instSemisimple : LieAlgebra.IsSemisimple ℂ self.gLie
• FlagVar : SmoothAlgVariety
• DF : CAlgebra
• U₀ : CAlgebra
• proj₀ : UniversalEnvelopingAlgebra ℂ self.gLie →ₐ[ℂ] self.U₀.carrier
• actionMap : UniversalEnvelopingAlgebra ℂ self.gLie →ₐ[ℂ] self.DF.carrier
• proj₀_surjective : Function.Surjective ⇑self.proj₀
• ker_inclusion (x : UniversalEnvelopingAlgebra ℂ self.gLie) : self.proj₀ x = 0 → self.actionMap x = 0
• NilpCone : Type u
• CotangentBundle : Type u
• grU₀ : GradedAlgebra
• grDF : GradedAlgebra
• O_TstarF : GradedAlgebra
• gr_a₀ : self.grU₀.carrier →ₐ[ℂ] self.grDF.carrier
• p_star : self.grU₀.carrier →ₐ[ℂ] self.O_TstarF.carrier
• incl_TstarF : self.O_TstarF.carrier →ₐ[ℂ] self.grDF.carrier
• p_star_bijective : Function.Bijective ⇑self.p_star
• symbol_proj : self.grDF.carrier →ₐ[ℂ] self.O_TstarF.carrier
• symbol_proj_left_inv : Function.LeftInverse ⇑self.symbol_proj ⇑self.incl_TstarF
• generators_grU₀ : Set self.grU₀.carrier
• grU₀_generated : Algebra.adjoin ℂ self.generators_grU₀ = ⊤
• generators_grU₀_deg1 : Set self.grU₀.carrier
• generators_grU₀_decomp : self.generators_grU₀ ⊆ Set.range ⇑(algebraMap ℂ self.grU₀.carrier) ∪ self.generators_grU₀_deg1
• symbolOfAction : self.grU₀.carrier → self.grDF.carrier
• gr_a₀_eq_symbolOfAction_field (x : self.grU₀.carrier) : x ∈ self.generators_grU₀_deg1 → self.gr_a₀ x = self.symbolOfAction x
• incl_p_star_eq_symbolOfAction_field (x : self.grU₀.carrier) : x ∈ self.generators_grU₀_deg1 → (self.incl_TstarF.comp self.p_star) x = self.symbolOfAction x
• DModF : AbCat
• U₀Mod : AbCat
• Gamma : CategoryTheory.Functor self.DModF.Obj self.U₀Mod.Obj
• Loc : CategoryTheory.Functor self.U₀Mod.Obj self.DModF.Obj
• filtration_U₀ : ℕ → Submodule ℂ self.U₀.carrier
• filtration_DF : ℕ → Submodule ℂ self.DF.carrier
• filtration_U₀_exhaustive (x : self.U₀.carrier) : ∃ (n : ℕ), x ∈ self.filtration_U₀ n
• filtration_U₀_mono ⦃m n : ℕ⦄ : m ≤ n → self.filtration_U₀ m ≤ self.filtration_U₀ n
• filtration_DF_exhaustive (y : self.DF.carrier) : ∃ (n : ℕ), y ∈ self.filtration_DF n
• quotient_U₀ (n : ℕ) : ↥(self.filtration_U₀ n) → self.grU₀.carrier
• quotient_DF (n : ℕ) : ↥(self.filtration_DF n) → self.grDF.carrier
• quotient_U₀_ker (n : ℕ) (x : self.U₀.carrier) (hx : x ∈ self.filtration_U₀ n) : self.quotient_U₀ n ⟨x, hx⟩ = 0 ↔ x ∈ filtPred self.filtration_U₀ n
• quotient_DF_ker (n : ℕ) (y : self.DF.carrier) (hy : y ∈ self.filtration_DF n) : self.quotient_DF n ⟨y, hy⟩ = 0 ↔ y ∈ filtPred self.filtration_DF n
• quotient_DF_sub (n : ℕ) (y₁ y₂ : self.DF.carrier) (hy₁ : y₁ ∈ self.filtration_DF n) (hy₂ : y₂ ∈ self.filtration_DF n) (hy_sub : y₁ - y₂ ∈ self.filtration_DF n) : self.quotient_DF n ⟨y₁ - y₂, hy_sub⟩ = self.quotient_DF n ⟨y₁, hy₁⟩ - self.quotient_DF n ⟨y₂, hy₂⟩
• filtration_DF_mono ⦃m n : ℕ⦄ : m ≤ n → self.filtration_DF m ≤ self.filtration_DF n
• quotient_U₀_add (n : ℕ) (x₁ x₂ : self.U₀.carrier) (hx₁ : x₁ ∈ self.filtration_U₀ n) (hx₂ : x₂ ∈ self.filtration_U₀ n) (hx_add : x₁ + x₂ ∈ self.filtration_U₀ n) : self.quotient_U₀ n ⟨x₁ + x₂, hx_add⟩ = self.quotient_U₀ n ⟨x₁, hx₁⟩ + self.quotient_U₀ n ⟨x₂, hx₂⟩
• quotient_U₀_sub (n : ℕ) (x₁ x₂ : self.U₀.carrier) (hx₁ : x₁ ∈ self.filtration_U₀ n) (hx₂ : x₂ ∈ self.filtration_U₀ n) (hx_sub : x₁ - x₂ ∈ self.filtration_U₀ n) : self.quotient_U₀ n ⟨x₁ - x₂, hx_sub⟩ = self.quotient_U₀ n ⟨x₁, hx₁⟩ - self.quotient_U₀ n ⟨x₂, hx₂⟩
• quotient_DF_add (n : ℕ) (y₁ y₂ : self.DF.carrier) (hy₁ : y₁ ∈ self.filtration_DF n) (hy₂ : y₂ ∈ self.filtration_DF n) (hy_add : y₁ + y₂ ∈ self.filtration_DF n) : self.quotient_DF n ⟨y₁ + y₂, hy_add⟩ = self.quotient_DF n ⟨y₁, hy₁⟩ + self.quotient_DF n ⟨y₂, hy₂⟩
• quotient_DF_surj (z : self.grDF.carrier) : ∃ (n : ℕ) (y : self.DF.carrier) (hy : y ∈ self.filtration_DF n), self.quotient_DF n ⟨y, hy⟩ = z
• quotient_U₀_surj (z : self.grU₀.carrier) : ∃ (n : ℕ) (x : self.U₀.carrier) (hx : x ∈ self.filtration_U₀ n), self.quotient_U₀ n ⟨x, hx⟩ = z
• filtration_UEA : ℕ → Submodule ℂ (UniversalEnvelopingAlgebra ℂ self.gLie)
• actionMap_filtration_preserving (n : ℕ) (u : UniversalEnvelopingAlgebra ℂ self.gLie) : u ∈ self.filtration_UEA n → self.actionMap u ∈ self.filtration_DF n
• proj₀_filtration_surj (n : ℕ) (x : self.U₀.carrier) : x ∈ self.filtration_U₀ n → ∃ u ∈ self.filtration_UEA n, self.proj₀ u = x
• gr_a₀_compat_UEA (n : ℕ) (u : UniversalEnvelopingAlgebra ℂ self.gLie) (hu : u ∈ self.filtration_UEA n) (hpu : self.proj₀ u ∈ self.filtration_U₀ n) : self.gr_a₀ (self.quotient_U₀ n ⟨self.proj₀ u, hpu⟩) = self.quotient_DF n ⟨self.actionMap u, ⋯⟩
• symbol_proj_right_inv : Function.RightInverse ⇑self.symbol_proj ⇑self.incl_TstarF
• gr_a₀_approx_surj (n : ℕ) (y : self.DF.carrier) (hy : y ∈ self.filtration_DF n) : ∃ (u : UniversalEnvelopingAlgebra ℂ self.gLie) (hu : u ∈ self.filtration_UEA n) (_ : self.proj₀ u ∈ self.filtration_U₀ n), self.quotient_DF n ⟨self.actionMap u, ⋯⟩ = self.quotient_DF n ⟨y, hy⟩

noncomputable def BeilinsonBernstein.BBDataZero.a₀ (D : BBDataZero) : D.U₀.carrier →ₐ[ℂ] D.DF.carrier

theorem BeilinsonBernstein.BBDataZero.a₀_factors (D : BBDataZero) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : D.a₀ (D.proj₀ x) = D.actionMap x

theorem BeilinsonBernstein.BBDataZero.a₀_filtration_preserving (D : BBDataZero) (n : ℕ) (x : D.U₀.carrier) : x ∈ D.filtration_U₀ n → D.a₀ x ∈ D.filtration_DF n

theorem BeilinsonBernstein.BBDataZero.gr_a₀_compat (D : BBDataZero) (n : ℕ) (x : D.U₀.carrier) (hx : x ∈ D.filtration_U₀ n) : D.gr_a₀ (D.quotient_U₀ n ⟨x, hx⟩) = D.quotient_DF n ⟨D.a₀ x, ⋯⟩

theorem BeilinsonBernstein.BBDataZero.a₀_surj_of_structure (D : BBDataZero) : Function.Surjective ⇑D.a₀

theorem BeilinsonBernstein.BBDataZero.actionMap_surjective (D : BBDataZero) : Function.Surjective ⇑D.actionMap

theorem BeilinsonBernstein.BBDataZero.gr_a₀_eq_symbolOfAction (D : BBDataZero) (x : D.grU₀.carrier) : x ∈ D.generators_grU₀_deg1 → D.gr_a₀ x = D.symbolOfAction x

theorem BeilinsonBernstein.BBDataZero.incl_p_star_eq_symbolOfAction (D : BBDataZero) (x : D.grU₀.carrier) : x ∈ D.generators_grU₀_deg1 → (D.incl_TstarF.comp D.p_star) x = D.symbolOfAction x

theorem BeilinsonBernstein.BBDataZero.gr_a₀_step_down (D : BBDataZero) : Function.Injective ⇑D.gr_a₀ → ∀ (n : ℕ), ∀ x ∈ D.filtration_U₀ n, D.a₀ x ∈ filtPred D.filtration_DF n → x ∈ filtPred D.filtration_U₀ n

theorem BeilinsonBernstein.BBDataZero.quotient_surj_from_a₀ (D : BBDataZero) : Function.Surjective ⇑D.a₀ → ∀ (n : ℕ) (y : D.DF.carrier) (hy : y ∈ D.filtration_DF n), ∃ (x : D.U₀.carrier) (hx : x ∈ D.filtration_U₀ n), D.quotient_DF n ⟨D.a₀ x, ⋯⟩ = D.quotient_DF n ⟨y, hy⟩

theorem BeilinsonBernstein.BBDataZero.gr_a₀_step_up (D : BBDataZero) : Function.Surjective ⇑D.a₀ → ∀ (n : ℕ), ∀ y ∈ D.filtration_DF n, ∃ x ∈ D.filtration_U₀ n, y - D.a₀ x ∈ filtPred D.filtration_DF n

theorem BeilinsonBernstein.BBDataZero.gr_a₀_surj_of_levelwise_surj (D : BBDataZero) : (∀ (n : ℕ), ∀ y ∈ D.filtration_DF n, ∃ x ∈ D.filtration_U₀ n, D.a₀ x = y) → Function.Surjective ⇑D.gr_a₀

theorem BeilinsonBernstein.incl_TstarF_inj (D : BBDataZero) : Function.Injective ⇑D.incl_TstarF

theorem BeilinsonBernstein.a₀_factorization (D : BBDataZero) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : D.a₀ (D.proj₀ x) = D.actionMap x

theorem BeilinsonBernstein.a₀_surj (D : BBDataZero) : Function.Surjective ⇑D.a₀

theorem BeilinsonBernstein.gr_a₀_eq_on_deg1 (D : BBDataZero) (x : D.grU₀.carrier) : x ∈ D.generators_grU₀_deg1 → D.gr_a₀ x = (D.incl_TstarF.comp D.p_star) x

theorem BeilinsonBernstein.a₀_comp_proj₀ (D : BBDataZero) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : D.a₀ (D.proj₀ x) = D.actionMap x

theorem BeilinsonBernstein.gr_a₀_eq_on_generators (D : BBDataZero) (x : D.grU₀.carrier) : x ∈ D.generators_grU₀ → D.gr_a₀ x = (D.incl_TstarF.comp D.p_star) x

theorem BeilinsonBernstein.incl_TstarF_injective (D : BBDataZero) : Function.Injective ⇑D.incl_TstarF

theorem BeilinsonBernstein.filtered_surj (D : BBDataZero) : Function.Surjective ⇑D.a₀ → Function.Surjective ⇑D.gr_a₀

theorem BeilinsonBernstein.gr_a₀_surjective (D : BBDataZero) : Function.Surjective ⇑D.gr_a₀

theorem BeilinsonBernstein.thm_29_1_factorization (D : BBDataZero) : D.actionMap = D.a₀.comp D.proj₀

theorem BeilinsonBernstein.thm_29_1_gr_eq_pullback (D : BBDataZero) : D.gr_a₀ = D.incl_TstarF.comp D.p_star

theorem BeilinsonBernstein.thm_29_1_grDF_eq_O_TstarF (D : BBDataZero) : Function.Bijective ⇑D.incl_TstarF

theorem BeilinsonBernstein.filtered_bij (D : BBDataZero) : Function.Bijective ⇑D.gr_a₀ → Function.Bijective ⇑D.a₀

theorem BeilinsonBernstein.thm_29_1_iso (D : BBDataZero) : Function.Bijective ⇑D.a₀

theorem BeilinsonBernstein.thm_29_2_localization (D : BBDataZero) : ∃ (e : D.DModF.Obj ≌ D.U₀Mod.Obj), e.functor = D.Gamma ∧ e.inverse = D.Loc

theorem BeilinsonBernstein.cor_29_4_flag_Daffine (D : BBDataZero) : IsDaffine D.FlagVar D.DModF D.U₀Mod D.Gamma D.Loc

structure BeilinsonBernstein.PartialFlagData : Type (u + 1)

• gLie : Type u
• instLieRing : LieRing self.gLie
• instLieAlgebra : LieAlgebra ℂ self.gLie
• instSemisimple : LieAlgebra.IsSemisimple ℂ self.gLie
• X : SmoothAlgVariety
• DX : CAlgebra
• DMod : AbCat
• DXMod : AbCat
• Gamma : CategoryTheory.Functor self.DMod.Obj self.DXMod.Obj
• Loc : CategoryTheory.Functor self.DXMod.Obj self.DMod.Obj

theorem BeilinsonBernstein.cor_29_4_partial_flag_Daffine (D : PartialFlagData) : IsDaffine D.X D.DMod D.DXMod D.Gamma D.Loc

structure BeilinsonBernstein.TwistedDiffOps (X : SmoothAlgVariety) (WeightSpace : Type u) : Type (u + 1)

• weight : WeightSpace
• algebra : CAlgebra

structure BeilinsonBernstein.TwistedDModuleCat (X : SmoothAlgVariety) (WeightSpace : Type u) : Type (u + 1)

• weight : WeightSpace
• cat : AbCat

structure BeilinsonBernstein.BBDataTwisted : Type (u + 1)

• gLie : Type u
• instLieRing : LieRing self.gLie
• instLieAlgebra : LieAlgebra ℂ self.gLie
• instSemisimple : LieAlgebra.IsSemisimple ℂ self.gLie
• WeightSpace : Type u
• IsAntidominant : self.WeightSpace → Prop
• FlagVar : SmoothAlgVariety
• DOfWeight : self.WeightSpace → CAlgebra
• UOfWeight : self.WeightSpace → CAlgebra
• projOfWeight (mu : self.WeightSpace) : UniversalEnvelopingAlgebra ℂ self.gLie →ₐ[ℂ] (self.UOfWeight mu).carrier
• actionMapOfWeight (mu : self.WeightSpace) : UniversalEnvelopingAlgebra ℂ self.gLie →ₐ[ℂ] (self.DOfWeight mu).carrier
• aOfWeight (mu : self.WeightSpace) : (self.UOfWeight mu).carrier →ₐ[ℂ] (self.DOfWeight mu).carrier
• NilpCone : Type u
• CotangentBundle : Type u
• grUOfWeight : self.WeightSpace → GradedAlgebra
• grDOfWeight : self.WeightSpace → GradedAlgebra
• O_TstarF : GradedAlgebra
• gr_aOfWeight (mu : self.WeightSpace) : (self.grUOfWeight mu).carrier →ₐ[ℂ] (self.grDOfWeight mu).carrier
• p_starOfWeight (mu : self.WeightSpace) : (self.grUOfWeight mu).carrier →ₐ[ℂ] self.O_TstarF.carrier
• incl_TstarFOfWeight (mu : self.WeightSpace) : self.O_TstarF.carrier →ₐ[ℂ] (self.grDOfWeight mu).carrier
• p_starOfWeight_bijective (mu : self.WeightSpace) : Function.Bijective ⇑(self.p_starOfWeight mu)
• symbol_projOfWeight (mu : self.WeightSpace) : (self.grDOfWeight mu).carrier →ₐ[ℂ] self.O_TstarF.carrier
• symbol_projOfWeight_left_inv (mu : self.WeightSpace) : Function.LeftInverse ⇑(self.symbol_projOfWeight mu) ⇑(self.incl_TstarFOfWeight mu)
• generators_grUOfWeight (mu : self.WeightSpace) : Set (self.grUOfWeight mu).carrier
• grUOfWeight_generated (mu : self.WeightSpace) : Algebra.adjoin ℂ (self.generators_grUOfWeight mu) = ⊤
• generators_grUOfWeight_deg1 (mu : self.WeightSpace) : Set (self.grUOfWeight mu).carrier
• generators_grUOfWeight_decomp (mu : self.WeightSpace) : self.generators_grUOfWeight mu ⊆ Set.range ⇑(algebraMap ℂ (self.grUOfWeight mu).carrier) ∪ self.generators_grUOfWeight_deg1 mu
• symbolOfActionOfWeight (mu : self.WeightSpace) : (self.grUOfWeight mu).carrier → (self.grDOfWeight mu).carrier
• gr_aOfWeight_eq_symbolOfAction_field (mu : self.WeightSpace) (x : (self.grUOfWeight mu).carrier) : x ∈ self.generators_grUOfWeight_deg1 mu → (self.gr_aOfWeight mu) x = self.symbolOfActionOfWeight mu x
• incl_p_star_eq_symbolOfActionOfWeight_field (mu : self.WeightSpace) (x : (self.grUOfWeight mu).carrier) : x ∈ self.generators_grUOfWeight_deg1 mu → ((self.incl_TstarFOfWeight mu).comp (self.p_starOfWeight mu)) x = self.symbolOfActionOfWeight mu x
• filtration_UOfWeight (mu : self.WeightSpace) : ℕ → Submodule ℂ (self.UOfWeight mu).carrier
• filtration_DOfWeight (mu : self.WeightSpace) : ℕ → Submodule ℂ (self.DOfWeight mu).carrier
• filtration_UOfWeight_exhaustive (mu : self.WeightSpace) (x : (self.UOfWeight mu).carrier) : ∃ (n : ℕ), x ∈ self.filtration_UOfWeight mu n
• filtration_UOfWeight_mono (mu : self.WeightSpace) ⦃m n : ℕ⦄ : m ≤ n → self.filtration_UOfWeight mu m ≤ self.filtration_UOfWeight mu n
• filtration_DOfWeight_exhaustive (mu : self.WeightSpace) (y : (self.DOfWeight mu).carrier) : ∃ (n : ℕ), y ∈ self.filtration_DOfWeight mu n
• DModOfWeight : self.WeightSpace → AbCat
• UModOfWeight : self.WeightSpace → AbCat
• GammaOfWeight (mu : self.WeightSpace) : CategoryTheory.Functor (self.DModOfWeight mu).Obj (self.UModOfWeight mu).Obj
• LocOfWeight (mu : self.WeightSpace) : CategoryTheory.Functor (self.UModOfWeight mu).Obj (self.DModOfWeight mu).Obj
• aOfWeight_filtration_preserving (mu : self.WeightSpace) (n : ℕ) (x : (self.UOfWeight mu).carrier) : x ∈ self.filtration_UOfWeight mu n → (self.aOfWeight mu) x ∈ self.filtration_DOfWeight mu n
• quotient_UOfWeight (mu : self.WeightSpace) (n : ℕ) : ↥(self.filtration_UOfWeight mu n) → (self.grUOfWeight mu).carrier
• quotient_DOfWeight (mu : self.WeightSpace) (n : ℕ) : ↥(self.filtration_DOfWeight mu n) → (self.grDOfWeight mu).carrier
• quotient_UOfWeight_ker (mu : self.WeightSpace) (n : ℕ) (x : (self.UOfWeight mu).carrier) (hx : x ∈ self.filtration_UOfWeight mu n) : self.quotient_UOfWeight mu n ⟨x, hx⟩ = 0 ↔ x ∈ filtPred (self.filtration_UOfWeight mu) n
• quotient_DOfWeight_ker (mu : self.WeightSpace) (n : ℕ) (y : (self.DOfWeight mu).carrier) (hy : y ∈ self.filtration_DOfWeight mu n) : self.quotient_DOfWeight mu n ⟨y, hy⟩ = 0 ↔ y ∈ filtPred (self.filtration_DOfWeight mu) n
• gr_aOfWeight_compat (mu : self.WeightSpace) (n : ℕ) (x : (self.UOfWeight mu).carrier) (hx : x ∈ self.filtration_UOfWeight mu n) : (self.gr_aOfWeight mu) (self.quotient_UOfWeight mu n ⟨x, hx⟩) = self.quotient_DOfWeight mu n ⟨(self.aOfWeight mu) x, ⋯⟩
• quotient_DOfWeight_sub (mu : self.WeightSpace) (n : ℕ) (y₁ y₂ : (self.DOfWeight mu).carrier) (hy₁ : y₁ ∈ self.filtration_DOfWeight mu n) (hy₂ : y₂ ∈ self.filtration_DOfWeight mu n) (hy_sub : y₁ - y₂ ∈ self.filtration_DOfWeight mu n) : self.quotient_DOfWeight mu n ⟨y₁ - y₂, hy_sub⟩ = self.quotient_DOfWeight mu n ⟨y₁, hy₁⟩ - self.quotient_DOfWeight mu n ⟨y₂, hy₂⟩
• filtration_DOfWeight_mono (mu : self.WeightSpace) ⦃m n : ℕ⦄ : m ≤ n → self.filtration_DOfWeight mu m ≤ self.filtration_DOfWeight mu n
• quotient_DOfWeight_surj (mu : self.WeightSpace) (z : (self.grDOfWeight mu).carrier) : ∃ (n : ℕ) (y : (self.DOfWeight mu).carrier) (hy : y ∈ self.filtration_DOfWeight mu n), self.quotient_DOfWeight mu n ⟨y, hy⟩ = z
• quotient_UOfWeight_surj (mu : self.WeightSpace) (z : (self.grUOfWeight mu).carrier) : ∃ (n : ℕ) (x : (self.UOfWeight mu).carrier) (hx : x ∈ self.filtration_UOfWeight mu n), self.quotient_UOfWeight mu n ⟨x, hx⟩ = z
• aOfWeight_factors_field (mu : self.WeightSpace) (x : UniversalEnvelopingAlgebra ℂ self.gLie) : (self.aOfWeight mu) ((self.projOfWeight mu) x) = (self.actionMapOfWeight mu) x
• actionMapOfWeight_surjective_field (mu : self.WeightSpace) : Function.Surjective ⇑(self.actionMapOfWeight mu)
• gr_aOfWeight_approx_surj (mu : self.WeightSpace) (n : ℕ) (y : (self.DOfWeight mu).carrier) (hy : y ∈ self.filtration_DOfWeight mu n) : ∃ (x : (self.UOfWeight mu).carrier) (hx : x ∈ self.filtration_UOfWeight mu n), self.quotient_DOfWeight mu n ⟨(self.aOfWeight mu) x, ⋯⟩ = self.quotient_DOfWeight mu n ⟨y, hy⟩

theorem BeilinsonBernstein.BBDataTwisted.aOfWeight_factors (D : BBDataTwisted) (mu : D.WeightSpace) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : (D.aOfWeight mu) ((D.projOfWeight mu) x) = (D.actionMapOfWeight mu) x

theorem BeilinsonBernstein.BBDataTwisted.actionMapOfWeight_surjective (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.actionMapOfWeight mu)

theorem BeilinsonBernstein.BBDataTwisted.gr_aOfWeight_eq_symbolOfAction (D : BBDataTwisted) (mu : D.WeightSpace) (x : (D.grUOfWeight mu).carrier) : x ∈ D.generators_grUOfWeight_deg1 mu → (D.gr_aOfWeight mu) x = D.symbolOfActionOfWeight mu x

theorem BeilinsonBernstein.BBDataTwisted.incl_p_star_eq_symbolOfActionOfWeight (D : BBDataTwisted) (mu : D.WeightSpace) (x : (D.grUOfWeight mu).carrier) : x ∈ D.generators_grUOfWeight_deg1 mu → ((D.incl_TstarFOfWeight mu).comp (D.p_starOfWeight mu)) x = D.symbolOfActionOfWeight mu x

theorem BeilinsonBernstein.BBDataTwisted.gr_aOfWeight_step_down (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Injective ⇑(D.gr_aOfWeight mu) → ∀ (n : ℕ), ∀ x ∈ D.filtration_UOfWeight mu n, (D.aOfWeight mu) x ∈ filtPred (D.filtration_DOfWeight mu) n → x ∈ filtPred (D.filtration_UOfWeight mu) n

theorem BeilinsonBernstein.BBDataTwisted.quotient_surj_from_aOfWeight (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.aOfWeight mu) → ∀ (n : ℕ) (y : (D.DOfWeight mu).carrier) (hy : y ∈ D.filtration_DOfWeight mu n), ∃ (x : (D.UOfWeight mu).carrier) (hx : x ∈ D.filtration_UOfWeight mu n), D.quotient_DOfWeight mu n ⟨(D.aOfWeight mu) x, ⋯⟩ = D.quotient_DOfWeight mu n ⟨y, hy⟩

theorem BeilinsonBernstein.BBDataTwisted.gr_aOfWeight_step_up (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.aOfWeight mu) → ∀ (n : ℕ), ∀ y ∈ D.filtration_DOfWeight mu n, ∃ x ∈ D.filtration_UOfWeight mu n, y - (D.aOfWeight mu) x ∈ filtPred (D.filtration_DOfWeight mu) n

theorem BeilinsonBernstein.BBDataTwisted.gr_aOfWeight_surj_of_levelwise_surj (D : BBDataTwisted) (mu : D.WeightSpace) : (∀ (n : ℕ), ∀ y ∈ D.filtration_DOfWeight mu n, ∃ x ∈ D.filtration_UOfWeight mu n, (D.aOfWeight mu) x = y) → Function.Surjective ⇑(D.gr_aOfWeight mu)

theorem BeilinsonBernstein.aOfWeight_factorization (D : BBDataTwisted) (mu : D.WeightSpace) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : (D.aOfWeight mu) ((D.projOfWeight mu) x) = (D.actionMapOfWeight mu) x

theorem BeilinsonBernstein.incl_TstarFOfWeight_inj (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Injective ⇑(D.incl_TstarFOfWeight mu)

theorem BeilinsonBernstein.aOfWeight_surj (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.aOfWeight mu)

theorem BeilinsonBernstein.gr_aOfWeight_eq_on_deg1 (D : BBDataTwisted) (mu : D.WeightSpace) (x : (D.grUOfWeight mu).carrier) : x ∈ D.generators_grUOfWeight_deg1 mu → (D.gr_aOfWeight mu) x = ((D.incl_TstarFOfWeight mu).comp (D.p_starOfWeight mu)) x

theorem BeilinsonBernstein.aOfWeight_comp_proj (D : BBDataTwisted) (mu : D.WeightSpace) (x : UniversalEnvelopingAlgebra ℂ D.gLie) : (D.aOfWeight mu) ((D.projOfWeight mu) x) = (D.actionMapOfWeight mu) x

theorem BeilinsonBernstein.gr_aOfWeight_eq_on_generators (D : BBDataTwisted) (mu : D.WeightSpace) (x : (D.grUOfWeight mu).carrier) : x ∈ D.generators_grUOfWeight mu → (D.gr_aOfWeight mu) x = ((D.incl_TstarFOfWeight mu).comp (D.p_starOfWeight mu)) x

theorem BeilinsonBernstein.incl_TstarFOfWeight_injective (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Injective ⇑(D.incl_TstarFOfWeight mu)

theorem BeilinsonBernstein.thm_29_6_factorization (D : BBDataTwisted) (mu : D.WeightSpace) : D.actionMapOfWeight mu = (D.aOfWeight mu).comp (D.projOfWeight mu)

theorem BeilinsonBernstein.thm_29_6_gr_eq_pullback (D : BBDataTwisted) (mu : D.WeightSpace) : D.gr_aOfWeight mu = (D.incl_TstarFOfWeight mu).comp (D.p_starOfWeight mu)

theorem BeilinsonBernstein.filtered_surj_twisted (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.aOfWeight mu) → Function.Surjective ⇑(D.gr_aOfWeight mu)

theorem BeilinsonBernstein.gr_aOfWeight_surjective (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Surjective ⇑(D.gr_aOfWeight mu)

theorem BeilinsonBernstein.thm_29_6_grDF_eq_O_TstarF (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Bijective ⇑(D.incl_TstarFOfWeight mu)

theorem BeilinsonBernstein.filtered_bijOfWeight (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Bijective ⇑(D.gr_aOfWeight mu) → Function.Bijective ⇑(D.aOfWeight mu)

theorem BeilinsonBernstein.thm_29_6_iso (D : BBDataTwisted) (mu : D.WeightSpace) : Function.Bijective ⇑(D.aOfWeight mu)

theorem BeilinsonBernstein.thm_29_7_BB_localization (D : BBDataTwisted) (mu : D.WeightSpace) (hmu : D.IsAntidominant mu) : ∃ (e : (D.DModOfWeight mu).Obj ≌ (D.UModOfWeight mu).Obj), e.functor = D.GammaOfWeight mu ∧ e.inverse = D.LocOfWeight mu

theorem BeilinsonBernstein.cor_29_7_twisted_flag_Daffine (D : BBDataTwisted) (mu : D.WeightSpace) (hmu : D.IsAntidominant mu) : IsDaffine D.FlagVar (D.DModOfWeight mu) (D.UModOfWeight mu) (D.GammaOfWeight mu) (D.LocOfWeight mu)