Documentation

Atlas.LieGroups.code.TranslationFunctors

source
structure TranslationFunctorData {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) :
Type (max (max u_1 u_2) (u_3 + 1))
Instances For
    source
    structure TranslationFunctorData.ApplyResult {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] :
    Type (max (max u_1 u_2) (u_4 + 1))
    Instances For
      source
      def charEigenspace {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) :
      Submodule R M
      Instances For
        source
        theorem charEigenspace_closed_uea {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (u : UniversalEnvelopingAlgebra R 𝔀) {m : M} (hm : m ∈ charEigenspace act Ο‡) :
        (act u) m ∈ charEigenspace act Ο‡
        source
        def charEigenspaceLie {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hcompat : βˆ€ (x : 𝔀) (m : M), (act ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆) :
        LieSubmodule R 𝔀 M
        Instances For
          source
          noncomputable def restrictedUEAAction {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hcompat : βˆ€ (x : 𝔀) (m : M), (act ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆) :
          UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R β†₯(charEigenspaceLie act Ο‡ hcompat)
          Instances For
            source
            theorem restrictedUEAAction_compat {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hcompat : βˆ€ (x : 𝔀) (m : M), (act ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆) (x : 𝔀) (m : β†₯(charEigenspaceLie act Ο‡ hcompat)) :
            ((restrictedUEAAction act Ο‡ hcompat) ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆
            source
            theorem restrictedUEA_center_acts {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hcompat : βˆ€ (x : 𝔀) (m : M), (act ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆) (z : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀))) (m : β†₯(charEigenspaceLie act Ο‡ hcompat)) :
            ((restrictedUEAAction act Ο‡ hcompat) ↑z) m = Ο‡ z β€’ m
            source
            theorem translation_center_acts_by_scalar_ax {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (z : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀))) (m : TensorProduct R F.V M) :
            ((ueaActionFromLieModule (TensorProduct R F.V M)) ↑z) m = (evalHC Ξ” wg F.mu) z β€’ m
            source
            noncomputable def TranslationFunctorData.applyToModule {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] :
            ApplyResult Ξ” rd wg F M
            Instances For
              source
              theorem lemma_23_4_shifted_stabilizer {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (hmu : IsDominantWeightLE rd wg mu) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔀 V] [LieModule R 𝔀 V] [Module.Finite R V] [IsSimpleModule R V] (hext : mu - lam ∈ weights Ξ” V) (w : wg.W) (hw_weight : wg.shiftedAction w mu - lam ∈ weights Ξ” V) :
              wg.shiftedAction w mu = mu
              source
              theorem norm_inequality_forces_extremal_weight {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M_lam : Type u_5) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (_hM : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) (_hW : WeylStabilizerModQ rd wg F.lam βŠ† WeylStabilizerModQ rd wg F.mu) (Ξ² : β†₯Ξ”.π”₯ β†’β‚—[R] R) (_hΞ²_weight : Ξ² ∈ weights Ξ” F.V) (_hΞ²_survives : evalHC Ξ” wg (F.lam + Ξ²) = evalHC Ξ” wg F.mu) :
              Ξ² = F.mu - F.lam
              source
              theorem block_projection_single_verma_factor {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M_lam : Type u_5) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (_hM : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) (_hW : WeylStabilizerModQ rd wg F.lam βŠ† WeylStabilizerModQ rd wg F.mu) (_h_unique : βˆ€ Ξ² ∈ weights Ξ” F.V, evalHC Ξ” wg (F.lam + Ξ²) = evalHC Ξ” wg F.mu β†’ Ξ² = F.mu - F.lam) :
              Nonempty (IsVermaModule Ξ” (TranslationFunctorData.applyToModule Ξ” rd wg F M_lam).carrier (F.mu - wg.ρ))
              source
              theorem translation_functor_verma_output {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M_lam : Type u_5) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (hM : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) (hW : WeylStabilizerModQ rd wg F.lam βŠ† WeylStabilizerModQ rd wg F.mu) :
              Nonempty (IsVermaModule Ξ” (TranslationFunctorData.applyToModule Ξ” rd wg F M_lam).carrier (F.mu - wg.ρ))
              source
              theorem TranslationFunctor.verma_maps_to_verma {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M_lam : Type u_3) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (hM : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) (hW : WeylStabilizerModQ rd wg F.lam βŠ† WeylStabilizerModQ rd wg F.mu) :
              have result := TranslationFunctorData.applyToModule Ξ” rd wg F M_lam; Nonempty (IsVermaModule Ξ” result.carrier (F.mu - wg.ρ))
              source
              structure IsContragredientLieModule {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (V : Type u_3) [AddCommGroup V] [Module R V] [LieRingModule 𝔀 V] [LieModule R 𝔀 V] (W : Type u_4) [AddCommGroup W] [Module R W] [LieRingModule 𝔀 W] [LieModule R 𝔀 W] :
              Type (max (max u_1 u_3) u_4)
              Instances For
                source
                def IsContragredientLieModule.symm {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] {V : Type u_3} [AddCommGroup V] [Module R V] [LieRingModule 𝔀 V] [LieModule R 𝔀 V] {W : Type u_4} [AddCommGroup W] [Module R W] [LieRingModule 𝔀 W] [LieModule R 𝔀 W] (h : IsContragredientLieModule V W) :
                IsContragredientLieModule W V
                Instances For
                  source
                  theorem exists_verma_module {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) :
                  βˆƒ (M_lam : Type u_5) (x : AddCommGroup M_lam) (x_1 : Module R M_lam) (x_2 : LieRingModule 𝔀 M_lam) (x_3 : LieModule R 𝔀 M_lam), Nonempty (IsVermaModule Ξ” M_lam wt)
                  source
                  theorem verma_module_iso_of_same_weight {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (M₁ : Type u_5) [AddCommGroup M₁] [Module R M₁] [LieRingModule 𝔀 M₁] [LieModule R 𝔀 M₁] (Mβ‚‚ : Type u_6) [AddCommGroup Mβ‚‚] [Module R Mβ‚‚] [LieRingModule 𝔀 Mβ‚‚] [LieModule R 𝔀 Mβ‚‚] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (h₁ : IsVermaModule Ξ” M₁ wt) (hβ‚‚ : IsVermaModule Ξ” Mβ‚‚ wt) :
                  Nonempty (M₁ ≃ₗ⁅R,𝔀⁆ Mβ‚‚)
                  source
                  theorem projective_functor_determination_on_block {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (G : TranslationFunctorData Ξ” rd wg) (hG_lam : G.lam = F.mu) (hG_mu : G.mu = F.lam) (hG_V_dual : IsContragredientLieModule F.V G.V) (hW : WeylStabilizerModQ rd wg F.lam = WeylStabilizerModQ rd wg F.mu) (M_lam : Type u_5) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (hVerma : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) (hVerma_fixed : Nonempty ((TranslationFunctorData.applyToModule Ξ” rd wg G (TranslationFunctorData.applyToModule Ξ” rd wg F M_lam).carrier).carrier ≃ₗ⁅R,𝔀⁆ M_lam)) (M : Type u_6) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM_ic : HasInfinitesimalCharacter M (evalHC Ξ” wg F.lam)) :
                  have FM := TranslationFunctorData.applyToModule Ξ” rd wg F M; have GFM := TranslationFunctorData.applyToModule Ξ” rd wg G FM.carrier; Nonempty (GFM.carrier ≃ₗ⁅R,𝔀⁆ M)
                  source
                  theorem composition_fixes_verma {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (G : TranslationFunctorData Ξ” rd wg) (hG_lam : G.lam = F.mu) (hG_mu : G.mu = F.lam) (hW : WeylStabilizerModQ rd wg F.lam = WeylStabilizerModQ rd wg F.mu) (M_lam : Type u_5) [AddCommGroup M_lam] [Module R M_lam] [LieRingModule 𝔀 M_lam] [LieModule R 𝔀 M_lam] (hVerma : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)) :
                  Nonempty ((TranslationFunctorData.applyToModule Ξ” rd wg G (TranslationFunctorData.applyToModule Ξ” rd wg F M_lam).carrier).carrier ≃ₗ⁅R,𝔀⁆ M_lam)
                  source
                  theorem translation_functor_composition_iso_id {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (G : TranslationFunctorData Ξ” rd wg) (hG_lam : G.lam = F.mu) (hG_mu : G.mu = F.lam) (hG_V_dual : IsContragredientLieModule F.V G.V) (hW : WeylStabilizerModQ rd wg F.lam = WeylStabilizerModQ rd wg F.mu) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM_ic : HasInfinitesimalCharacter M (evalHC Ξ” wg F.lam)) :
                  have FM := TranslationFunctorData.applyToModule Ξ” rd wg F M; have GFM := TranslationFunctorData.applyToModule Ξ” rd wg G FM.carrier; Nonempty (GFM.carrier ≃ₗ⁅R,𝔀⁆ M)
                  source
                  theorem TranslationFunctor.equivalence {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (hW : WeylStabilizerModQ rd wg F.lam = WeylStabilizerModQ rd wg F.mu) (G : TranslationFunctorData Ξ” rd wg) (hG_lam : G.lam = F.mu) (hG_mu : G.mu = F.lam) (hG_V_dual : IsContragredientLieModule F.V G.V) :
                  (βˆ€ (M_lam : Type u_3) [inst : AddCommGroup M_lam] [inst_1 : Module R M_lam] [inst_2 : LieRingModule 𝔀 M_lam] [inst_3 : LieModule R 𝔀 M_lam] (a : IsVermaModule Ξ” M_lam (F.lam - wg.ρ)), Nonempty (IsVermaModule Ξ” (TranslationFunctorData.applyToModule Ξ” rd wg F M_lam).carrier (F.mu - wg.ρ))) ∧ (βˆ€ (M_mu : Type u_4) [inst : AddCommGroup M_mu] [inst_1 : Module R M_mu] [inst_2 : LieRingModule 𝔀 M_mu] [inst_3 : LieModule R 𝔀 M_mu] (a : IsVermaModule Ξ” M_mu (F.mu - wg.ρ)), Nonempty (IsVermaModule Ξ” (TranslationFunctorData.applyToModule Ξ” rd wg G M_mu).carrier (F.lam - wg.ρ))) ∧ (βˆ€ (M : Type u_5) [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : LieRingModule 𝔀 M] [inst_3 : LieModule R 𝔀 M] (a : HasInfinitesimalCharacter M (evalHC Ξ” wg F.lam)), have FM := TranslationFunctorData.applyToModule Ξ” rd wg F M; have GFM := TranslationFunctorData.applyToModule Ξ” rd wg G FM.carrier; Nonempty (GFM.carrier ≃ₗ⁅R,𝔀⁆ M)) ∧ βˆ€ (N : Type u_6) [inst : AddCommGroup N] [inst_1 : Module R N] [inst_2 : LieRingModule 𝔀 N] [inst_3 : LieModule R 𝔀 N] (a : HasInfinitesimalCharacter N (evalHC Ξ” wg F.mu)), have GN := TranslationFunctorData.applyToModule Ξ” rd wg G N; have FGN := TranslationFunctorData.applyToModule Ξ” rd wg F GN.carrier; Nonempty (FGN.carrier ≃ₗ⁅R,𝔀⁆ N)
                  source
                  theorem charEigenspace_isCategoryO_ax {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {rd : PositiveRootData Ξ”} {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsCategoryO Ξ” rd M) (act : UniversalEnvelopingAlgebra R 𝔀 →ₐ[R] Module.End R M) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hcompat : βˆ€ (x : 𝔀) (m : M), (act ((UniversalEnvelopingAlgebra.ΞΉ R) x)) m = ⁅x, m⁆) :
                  IsCategoryO Ξ” rd β†₯(charEigenspaceLie act Ο‡ hcompat)
                  source
                  theorem TranslationFunctor.preserves_categoryO {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsCategoryO Ξ” rd M) :
                  have result := TranslationFunctorData.applyToModule Ξ” rd wg F M; IsCategoryO Ξ” rd result.carrier
                  source
                  theorem tensor_finiteDim_free_nminus {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] {Ξ” : TriangularDecomposition R 𝔀} {V : Type u_5} [AddCommGroup V] [Module R V] [LieRingModule 𝔀 V] [LieModule R 𝔀 V] [Module.Finite R V] {X : Type u_6} [AddCommGroup X] [Module R X] [LieRingModule 𝔀 X] [LieModule R 𝔀 X] (hXfree : IsFreeOverNMinus X) :
                  IsFreeOverNMinus (TensorProduct R V X)
                  source
                  theorem translation_functor_standard_filtration {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (F : TranslationFunctorData Ξ” rd wg) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsCategoryO Ξ” rd M) (hFM : IsCategoryO Ξ” rd (TranslationFunctorData.applyToModule Ξ” rd wg F M).carrier) :
                  HasStandardFiltration rd (TranslationFunctorData.applyToModule Ξ” rd wg F M).carrier hFM
                  source
                  def TwoSidedIdeal.toSubmoduleR {R : Type u_3} {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] (J : TwoSidedIdeal A) :
                  Submodule R A
                  Instances For
                    source
                    noncomputable def idealToSubmoduleEvalAtV {R : Type u_3} {A : Type u_4} {M : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (act : A →ₐ[R] Module.End R M) (v : M) :
                    A β†’β‚—[R] M
                    Instances For
                      source
                      theorem idealToSubmoduleMap_order_reflecting {R : Type u_3} [CommRing R] {A : Type u_4} [Ring A] [Algebra R A] (M : Type u_5) [AddCommGroup M] [Module R M] (act : A →ₐ[R] Module.End R M) (v : M) (I J : TwoSidedIdeal A) (hinj : Function.Injective fun (u : A) => (act u) v) (hsurj : Function.Surjective fun (u : A) => (act u) v) (hle : Submodule.span R {m : M | βˆƒ j ∈ I, βˆƒ (x : M), m = (act j) x} ≀ Submodule.span R {m : M | βˆƒ j ∈ J, βˆƒ (x : M), m = (act j) x}) :
                      I ≀ J
                      source
                      theorem pbw_verma_hwv_annihilator_in_central_ideal_aux {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (wg : WeylGroupData Ξ”) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hM : IsVermaModule Ξ” M wt) (u : UniversalEnvelopingAlgebra R 𝔀) (hu : ((ueaActionFromLieModule M) u) hM.highestWeightVec = 0) :
                      (MaximalQuotient.proj (evalHC Ξ” wg (wt + wg.ρ))) u = 0
                      source
                      theorem smul_left_injective_of_pbw_verma {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hM : IsVermaModule Ξ” M wt) (r₁ rβ‚‚ : R) (h : r₁ β€’ hM.highestWeightVec = rβ‚‚ β€’ hM.highestWeightVec) :
                      r₁ = rβ‚‚
                      source
                      theorem verma_hwv_annihilator_in_central_ideal {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (wg : WeylGroupData Ξ”) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hM : IsVermaModule Ξ” M wt) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hic : HasInfinitesimalCharacter M Ο‡) (u : UniversalEnvelopingAlgebra R 𝔀) (hu : (hic.ueaAction u) hM.highestWeightVec = 0) :
                      (MaximalQuotient.proj Ο‡) u = 0
                      source
                      theorem verma_eval_injective {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (wg : WeylGroupData Ξ”) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hM : IsVermaModule Ξ” M wt) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hic : HasInfinitesimalCharacter M Ο‡) (act : MaximalQuotient Ο‡ →ₐ[R] Module.End R M) (hcompat : βˆ€ (u : UniversalEnvelopingAlgebra R 𝔀) (m : M), (hic.ueaAction u) m = (act ((MaximalQuotient.proj Ο‡) u)) m) :
                      Function.Injective fun (u : MaximalQuotient Ο‡) => (act u) hM.highestWeightVec
                      source
                      theorem verma_eval_surjective {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (wg : WeylGroupData Ξ”) {M : Type u_5} [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (wt : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hM : IsVermaModule Ξ” M wt) (Ο‡ : β†₯(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔀)) →ₐ[R] R) (hic : HasInfinitesimalCharacter M Ο‡) (act : MaximalQuotient Ο‡ →ₐ[R] Module.End R M) (hcompat : βˆ€ (u : UniversalEnvelopingAlgebra R 𝔀) (m : M), (hic.ueaAction u) m = (act ((MaximalQuotient.proj Ο‡) u)) m) :
                      Function.Surjective fun (u : MaximalQuotient Ο‡) => (act u) hM.highestWeightVec
                      source
                      theorem idealToSubmoduleMap_order_properties {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (hmu : evalHC Ξ” wg mu = evalHC Ξ” wg lam) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (mu - wg.ρ)) :
                      βˆƒ (Ξ½ : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) β†’o Submodule R M), Ξ½ βŠ₯ = βŠ₯ ∧ Ξ½ ⊀ = ⊀ ∧ βˆ€ (I J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ I ≀ Ξ½ J β†’ I ≀ J
                      source
                      theorem idealToSubmoduleMap_reflects_order_general {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (hmu : evalHC Ξ” wg mu = evalHC Ξ” wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (mu - wg.ρ)) :
                      βˆƒ (Ξ½ : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) β†’o Submodule R M), Ξ½ βŠ₯ = βŠ₯ ∧ Ξ½ ⊀ = ⊀ ∧ βˆ€ (I J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ I ≀ Ξ½ J β†’ I ≀ J
                      source
                      noncomputable def idealToSubmoduleMap {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) :
                      TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) β†’o Submodule R M
                      Instances For
                        source
                        theorem idealToSubmoduleMap_properties {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) :
                        have Ξ½ := idealToSubmoduleMap Ξ” rd wg lam hlam M hM; Ξ½ βŠ₯ = βŠ₯ ∧ Ξ½ ⊀ = ⊀ ∧ βˆ€ (I J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ I ≀ Ξ½ J β†’ I ≀ J
                        source
                        theorem ideals_submodules_image_characterization_forward {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type uM) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) :
                        have Ξ½ := idealToSubmoduleMap Ξ” rd wg lam hlam M hM; βˆ€ (J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), βˆƒ (I : Type uM) (mu : I β†’ β†₯Ξ”.π”₯ β†’β‚—[R] R), (βˆ€ (i : I), evalHC Ξ” wg (mu i) = evalHC Ξ” wg lam) ∧ (βˆ€ (i : I), BruhatLE rd (mu i) lam) ∧ (βˆ€ (i : I) (w : wg.W), wg.dualAction w lam = lam β†’ BruhatLE rd (mu i) (wg.dualAction w (mu i))) ∧ βˆƒ (P : Type uM) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔀 P) (x_3 : LieModule R 𝔀 P) (hPO : IsCategoryO Ξ” rd P), IsProjectiveInO rd P hPO ∧ Nonempty (P →ₗ⁅R,𝔀⁆ M)
                        source
                        theorem projective_image_in_nu_range {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type uM) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) (N : Submodule R M) (hN : βˆƒ (I : Type uM) (mu : I β†’ β†₯Ξ”.π”₯ β†’β‚—[R] R), (βˆ€ (i : I), evalHC Ξ” wg (mu i) = evalHC Ξ” wg lam) ∧ (βˆ€ (i : I), BruhatLE rd (mu i) lam) ∧ (βˆ€ (i : I) (w : wg.W), wg.dualAction w lam = lam β†’ BruhatLE rd (mu i) (wg.dualAction w (mu i))) ∧ βˆƒ (P : Type uM) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔀 P) (x_3 : LieModule R 𝔀 P) (hPO : IsCategoryO Ξ” rd P), IsProjectiveInO rd P hPO ∧ Nonempty (P →ₗ⁅R,𝔀⁆ M)) :
                        βˆƒ (J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), (idealToSubmoduleMap Ξ” rd wg lam hlam M hM) J = N
                        source
                        theorem ideals_submodules_image_backward_ax {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type uM) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) :
                        have Ξ½ := idealToSubmoduleMap Ξ” rd wg lam hlam M hM; βˆ€ (N : Submodule R M), (βˆƒ (I : Type uM) (mu : I β†’ β†₯Ξ”.π”₯ β†’β‚—[R] R), (βˆ€ (i : I), evalHC Ξ” wg (mu i) = evalHC Ξ” wg lam) ∧ (βˆ€ (i : I), BruhatLE rd (mu i) lam) ∧ (βˆ€ (i : I) (w : wg.W), wg.dualAction w lam = lam β†’ BruhatLE rd (mu i) (wg.dualAction w (mu i))) ∧ βˆƒ (P : Type uM) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔀 P) (x_3 : LieModule R 𝔀 P) (hPO : IsCategoryO Ξ” rd P), IsProjectiveInO rd P hPO ∧ Nonempty (P →ₗ⁅R,𝔀⁆ M)) β†’ βˆƒ (J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ J = N
                        source
                        theorem ideals_submodules_lattice_iso {R : Type u_3} [Field R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (hregular : βˆ€ (w : wg.W), wg.dualAction w lam = lam β†’ w = 1) (M : Type uM) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) :
                        Nonempty (TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) ≃o LieSubmodule R 𝔀 M)
                        source
                        theorem idealToSubmoduleMap_image_isLieSubmodule {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) (Ξ½ : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) β†’o Submodule R M) (hΞ½bot : Ξ½ βŠ₯ = βŠ₯) (hΞ½top : Ξ½ ⊀ = ⊀) (hΞ½refl : βˆ€ (I J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ I ≀ Ξ½ J β†’ I ≀ J) (hΞ½lie : βˆ€ (I : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))) (x : 𝔀), βˆ€ m ∈ Ξ½ I, ⁅x, m⁆ ∈ Ξ½ I) (I : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))) :
                        βˆƒ (N : LieSubmodule R 𝔀 M), ↑N = Ξ½ I
                        source
                        theorem lie_closure_of_ideal_action {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) (Ξ½ : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam)) β†’o Submodule R M) (hΞ½bot : Ξ½ βŠ₯ = βŠ₯) (hΞ½top : Ξ½ ⊀ = ⊀) (hΞ½refl : βˆ€ (I J : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))), Ξ½ I ≀ Ξ½ J β†’ I ≀ J) (I : TwoSidedIdeal (MaximalQuotient (evalHC Ξ” wg lam))) (x : 𝔀) (m : M) :
                        m ∈ Ξ½ I β†’ ⁅x, m⁆ ∈ Ξ½ I
                        source
                        theorem dufloJoseph_proper_ideal_contradicts_simple {R : Type u_3} [CommRing R] {𝔀 : Type u_4} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam mu : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (hmu : evalHC Ξ” wg mu = evalHC Ξ” wg lam) (hSimple : IsSimpleRing (MaximalQuotient (evalHC Ξ” wg lam))) (M : Type u_5) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hVM : IsVermaModule Ξ” M (mu - wg.ρ)) (h_not_irr : Β¬LieModule.IsIrreducible R 𝔀 M) :
                        False
                        source
                        theorem simple_algebra_if_irreducible_verma {R : Type u_1} [CommRing R] {𝔀 : Type u_2} [LieRing 𝔀] [LieAlgebra R 𝔀] (Ξ” : TriangularDecomposition R 𝔀) (rd : PositiveRootData Ξ”) (wg : WeylGroupData Ξ”) (lam : β†₯Ξ”.π”₯ β†’β‚—[R] R) (hlam : IsDominantWeightLE rd wg lam) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔀 M] [LieModule R 𝔀 M] (hM : IsVermaModule Ξ” M (lam - wg.ρ)) (hirr : LieModule.IsIrreducible R 𝔀 M) :
                        IsSimpleRing (MaximalQuotient (evalHC Ξ” wg lam))