structure
BeilinsonBernstein.EquivariantBBDataextends BeilinsonBernstein.BBDataTwisted :
Type (max (u + 1) (u_1 + 1))
- instLieRing : LieRing self.gLie
- instLieAlgebra : LieAlgebra ℂ self.gLie
- WeightSpace : Type u_1
- IsAntidominant : self.WeightSpace → Prop
- 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
- CotangentBundle : Type u_1
- grUOfWeight : self.WeightSpace → GradedAlgebra
- grDOfWeight : self.WeightSpace → GradedAlgebra
- gr_aOfWeight (mu : self.WeightSpace) : (self.grUOfWeight mu).carrier →ₐ[ℂ] (self.grDOfWeight mu).carrier
- incl_TstarFOfWeight (mu : self.WeightSpace) : self.O_TstarF.carrier →ₐ[ℂ] (self.grDOfWeight mu).carrier
- 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)
- grUOfWeight_generated (mu : self.WeightSpace) : Algebra.adjoin ℂ (self.generators_grUOfWeight mu) = ⊤
- 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_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
- 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)
Instances For
noncomputable def
BeilinsonBernstein.corollary_30_20
(D : EquivariantBBData)
(mu : D.WeightSpace)
(hmu : D.IsAntidominant mu)
:
Instances For
theorem
BeilinsonBernstein.corollary_30_20_functor_eq
(D : EquivariantBBData)
(mu : D.WeightSpace)
(hmu : D.IsAntidominant mu)
:
theorem
BeilinsonBernstein.corollary_30_20_inverse_eq
(D : EquivariantBBData)
(mu : D.WeightSpace)
(hmu : D.IsAntidominant mu)
: