Documentation

Atlas.LieGroups.code.ExtO

source
def ExtOVanishes {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 projective_in_O_is_nminus_retract_of_free {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {wg : WeylGroupData Ξ”} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] (_hPO : IsCategoryO Ξ” rd P) (_hPproj : IsProjectiveInO rd P _hPO) :
    βˆƒ (Q : Type uCatO) (x : AddCommGroup Q) (x_1 : Module R Q) (x_2 : LieRingModule 𝔀 Q) (x_3 : LieModule R 𝔀 Q), Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) Q ∧ βˆƒ (ΞΉ : P β†’β‚—[UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg] Q) (s : Q β†’β‚—[UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg] P), s βˆ˜β‚— ΞΉ = LinearMap.id
    source
    theorem quillen_suslin_UEA_nminus {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] [Module (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) P] :
    Module.Projective (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) P β†’ Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) P
    source
    theorem nminus_projective_is_free {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] :
    Module.Projective (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) P β†’ Module.Free (UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) P
    source
    theorem projective_in_O_is_free_nminus {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {wg : WeylGroupData Ξ”} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] (hPO : IsCategoryO Ξ” rd P) (_hPproj : IsProjectiveInO rd P hPO) :
    IsFreeOverNMinus P
    source
    theorem UEA_induction_on {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] {C : UniversalEnvelopingAlgebra R L β†’ Prop} (u : UniversalEnvelopingAlgebra R L) (h_alg : βˆ€ (r : R), C ((algebraMap R (UniversalEnvelopingAlgebra R L)) r)) (h_ΞΉ : βˆ€ (x : L), C ((UniversalEnvelopingAlgebra.ΞΉ R) x)) (h_mul : βˆ€ (a b : UniversalEnvelopingAlgebra R L), C a β†’ C b β†’ C (a * b)) (h_add : βˆ€ (a b : UniversalEnvelopingAlgebra R L), C a β†’ C b β†’ C (a + b)) :
    C u
    source
    theorem lieModuleHom_ueaSubalg_compat {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔀 N] [LieModule R 𝔀 N] (f : M →ₗ⁅R,𝔀⁆ N) (u : UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg) (m : M) :
    f (((ueaSubalgAction Ξ”.𝔫_neg M) u) m) = ((ueaSubalgAction Ξ”.𝔫_neg N) u) (f m)
    source
    noncomputable def lieModuleHomToUEALinearMap {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {M N : Type uCatO} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] [AddCommGroup N] [Module R N] [LieRingModule 𝔀 N] [LieModule R 𝔀 N] (f : M →ₗ⁅R,𝔀⁆ N) :
    M β†’β‚—[UniversalEnvelopingAlgebra R β†₯Ξ”.𝔫_neg] N
    Instances For
      source
      theorem direct_summand_of_free_nminus_is_free {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] (_hPfree : IsFreeOverNMinus P) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (_hXfree : IsFreeOverNMinus X) {K : Type uCatO} [AddCommGroup K] [Module R K] [LieRingModule 𝔀 K] [LieModule R 𝔀 K] (_ΞΉ : K →ₗ⁅R,𝔀⁆ P) (_hΞΉ : Function.Injective ⇑_ΞΉ) (_p : P →ₗ⁅R,𝔀⁆ X) (_hp : Function.Surjective ⇑_p) (_hexact : βˆ€ (q : P), _p q = 0 ↔ βˆƒ (k : K), _ΞΉ k = q) :
      IsFreeOverNMinus K
      source
      theorem kernel_of_projective_over_free_nminus_is_free {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {wg : WeylGroupData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (_hXO : IsCategoryO Ξ” rd X) (hXfree : IsFreeOverNMinus X) {K : Type uCatO} [AddCommGroup K] [Module R K] [LieRingModule 𝔀 K] [LieModule R 𝔀 K] (_hKO : IsCategoryO Ξ” rd K) {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔀 P] [LieModule R 𝔀 P] (_hPO : IsCategoryO Ξ” rd P) (_hPproj : IsProjectiveInO rd P _hPO) (ΞΉ : K →ₗ⁅R,𝔀⁆ P) (_hΞΉ : Function.Injective ⇑ι) (p : P →ₗ⁅R,𝔀⁆ X) (_hp : Function.Surjective ⇑p) (hexact : βˆ€ (q : P), p q = 0 ↔ βˆƒ (k : K), ΞΉ k = q) :
      IsFreeOverNMinus K
      source
      theorem ext_vanishing_free_nminus {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {wg : WeylGroupData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hXfree : IsFreeOverNMinus 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) (i : β„•) (hi : i > 0) :
      ExtOVanishes i X hXO MmuDual hMmuDualO
      source
      theorem standardly_filtered_higher_ext_vanishing {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {wg : WeylGroupData Ξ”} {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXO : IsCategoryO Ξ” rd X) (hSF : 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) (i : β„•) (hi : i > 0) :
      ExtOVanishes i X hXO MmuDual hMmuDualO
      source
      theorem nonsplit_verma_ext_implies_comp_mult {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) {Mlam : Type uCatO} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔀 Mlam] [LieModule R 𝔀 Mlam] (hMlam : IsVermaModule Ξ” Mlam lam) (hMlamO : IsCategoryO Ξ” rd Mlam) {Mmu : Type uCatO} [AddCommGroup Mmu] [Module R Mmu] [LieRingModule 𝔀 Mmu] [LieModule R 𝔀 Mmu] (hMmu : IsVermaModule Ξ” Mmu mu) (hMmuO : IsCategoryO Ξ” rd Mmu) (E : Type uCatO) [AddCommGroup E] [Module R E] [LieRingModule 𝔀 E] [LieModule R 𝔀 E] (hEO : IsCategoryO Ξ” rd E) (i : Mlam →ₗ⁅R,𝔀⁆ E) (hi : Function.Injective ⇑i) (p : E →ₗ⁅R,𝔀⁆ Mmu) (hp : Function.Surjective ⇑p) (hns : Β¬βˆƒ (s : Mmu →ₗ⁅R,𝔀⁆ E), βˆ€ (x : Mmu), p (s x) = x) :
      compositionMultiplicity rd wg mu lam β‰  0 ∧ lam β‰  mu