structure BeilinsonBernstein.EquivariantBBDataextends BeilinsonBernstein.BBDataTwisted : Type (max (u + 1) (u_1 + 1))

• gLie : Type u_1
• instLieRing : LieRing self.gLie
• instLieAlgebra : LieAlgebra ℂ self.gLie
• instSemisimple : LieAlgebra.IsSemisimple ℂ self.gLie
• WeightSpace : Type u_1
• 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_1
• CotangentBundle : Type u_1
• 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⟩
• AlgGroupK : Type u
• instGroupK : Group self.AlgGroupK
• KEquivDModOfWeight (mu : self.WeightSpace) : AbCat
• GKModOfWeight (mu : self.WeightSpace) : AbCat
• inclKEquivDMod (mu : self.WeightSpace) : CategoryTheory.Functor (self.KEquivDModOfWeight mu).Obj (self.DModOfWeight mu).Obj
• inclGKMod (mu : self.WeightSpace) : CategoryTheory.Functor (self.GKModOfWeight mu).Obj (self.UModOfWeight mu).Obj
• inclKEquivDMod_faithful (mu : self.WeightSpace) : (self.inclKEquivDMod mu).Faithful
• inclGKMod_faithful (mu : self.WeightSpace) : (self.inclGKMod mu).Faithful
• GammaKEquivOfWeight (mu : self.WeightSpace) : CategoryTheory.Functor (self.KEquivDModOfWeight mu).Obj (self.GKModOfWeight mu).Obj
• LocKEquivOfWeight (mu : self.WeightSpace) : CategoryTheory.Functor (self.GKModOfWeight mu).Obj (self.KEquivDModOfWeight mu).Obj
• gammaKEquiv_compat (mu : self.WeightSpace) : (self.GammaKEquivOfWeight mu).comp (self.inclGKMod mu) = (self.inclKEquivDMod mu).comp (self.GammaOfWeight mu)
• locKEquiv_compat (mu : self.WeightSpace) : (self.LocKEquivOfWeight mu).comp (self.inclKEquivDMod mu) = (self.inclGKMod mu).comp (self.LocOfWeight mu)

noncomputable def BeilinsonBernstein.corollary_30_20 (D : EquivariantBBData) (mu : D.WeightSpace) (hmu : D.IsAntidominant mu) : (D.KEquivDModOfWeight mu).Obj ≌ (D.GKModOfWeight mu).Obj

theorem BeilinsonBernstein.corollary_30_20_functor_eq (D : EquivariantBBData) (mu : D.WeightSpace) (hmu : D.IsAntidominant mu) : (corollary_30_20 D mu hmu).functor = D.GammaKEquivOfWeight mu

theorem BeilinsonBernstein.corollary_30_20_inverse_eq (D : EquivariantBBData) (mu : D.WeightSpace) (hmu : D.IsAntidominant mu) : (corollary_30_20 D mu hmu).inverse = D.LocKEquivOfWeight mu