Documentation

Atlas.LieGroups.code.BGGResolution

source
def ExtVanishes_CategoryO {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} (rd : PositiveRootData Ξ”) :
β„• β†’ (X : Type uCatO) β†’ [inst : AddCommGroup X] β†’ [inst✝ : Module R X] β†’ [inst✝¹ : LieRingModule 𝔀 X] β†’ [inst✝² : LieModule R 𝔀 X] β†’ IsCategoryO Ξ” rd X β†’ (Y : Type uCatO) β†’ [inst✝³ : AddCommGroup Y] β†’ [inst✝⁴ : Module R Y] β†’ [inst✝⁡ : LieRingModule 𝔀 Y] β†’ [inst✝⁢ : LieModule R 𝔀 Y] β†’ IsCategoryO Ξ” rd Y β†’ Prop
Instances For
    source
    theorem free_over_nminus_is_projective_in_O {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXfree : Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) X) :
    IsProjectiveInO rd X hXO
    source
    theorem projective_implies_ext1_vanishes {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXproj : IsProjectiveInO rd X hXO) {Y : Type uCatO} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔀 Y] [LieModule R 𝔀 Y] (hYO : IsCategoryO Ξ” rd Y) :
    ExtVanishes_CategoryO rd 1 X hXO Y hYO
    source
    theorem ext1_vanishing_free_nminus_all_Y {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXfree : Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) X) {Y : Type uCatO} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔀 Y] [LieModule R 𝔀 Y] (hYO : IsCategoryO Ξ” rd Y) :
    ExtVanishes_CategoryO rd 1 X hXO Y hYO
    source
    theorem ext_higher_vanishing_of_free_nminus_general {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXfree : Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) X) (m : β„•) {Y : Type uCatO} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔀 Y] [LieModule R 𝔀 Y] (hYO : IsCategoryO Ξ” rd Y) :
    ExtVanishes_CategoryO rd (m + 1 + 1) X hXO Y hYO
    source
    theorem ext_higher_vanishing_of_free_nminus {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXfree : Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) X) (mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) {MmuDual : Type uCatO} [AddCommGroup MmuDual] [Module R MmuDual] [LieRingModule 𝔀 MmuDual] [LieModule R 𝔀 MmuDual] (hMmuDualO : IsCategoryO Ξ” rd MmuDual) (_hMmuDual : IsContragredientVerma rd MmuDual mu hMmuDualO) (m : β„•) :
    ExtVanishes_CategoryO rd (m + 1 + 1) X hXO MmuDual hMmuDualO
    source
    theorem ext_vanishing_higher_of_standard_filtration {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXsf : HasStandardFiltration rd X hXO) (mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) {MmuDual : Type uCatO} [AddCommGroup MmuDual] [Module R MmuDual] [LieRingModule 𝔀 MmuDual] [LieModule R 𝔀 MmuDual] (hMmuDualO : IsCategoryO Ξ” rd MmuDual) (hMmuDual : IsContragredientVerma rd MmuDual mu hMmuDualO) (m : β„•) :
    ExtVanishes_CategoryO rd (m + 1 + 1) X hXO MmuDual hMmuDualO