Documentation

Mathlib.Algebra.Lie.Quotient

Quotients of Lie algebras and Lie modules #

Given a Lie submodule of a Lie module, the quotient carries a natural Lie module structure. In the special case that the Lie module is the Lie algebra itself via the adjoint action, the submodule is a Lie ideal and the quotient carries a natural Lie algebra structure.

We define these quotient structures here. A notable omission at the time of writing (February 2021) is a statement and proof of the universal property of these quotients.

Main definitions #

Tags #

lie algebra, quotient

source
๐Ÿ”ธ coverage
@[implicit_reducible]
instance LieSubmodule.instHasQuotient {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :
HasQuotient M (LieSubmodule R L M)

The quotient of a Lie module by a Lie submodule. It is a Lie module.

source
๐Ÿ”ธ coverage
@[implicit_reducible]
instance LieSubmodule.Quotient.addCommGroup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :
AddCommGroup (M โงธ N)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
instance LieSubmodule.Quotient.module' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {S : Type u_1} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
Module S (M โงธ N)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
instance LieSubmodule.Quotient.module {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :
Module R (M โงธ N)
source
๐Ÿ“ coverage
instance LieSubmodule.Quotient.isCentralScalar {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {S : Type u_1} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] [SMul Sแตแต’แต– R] [Module Sแตแต’แต– M] [IsScalarTower Sแตแต’แต– R M] [IsCentralScalar S M] :
IsCentralScalar S (M โงธ N)
source
๐Ÿ”ธ coverage
@[implicit_reducible]
instance LieSubmodule.Quotient.inhabited {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :
Inhabited (M โงธ N)
source
๐Ÿ”ธ coverage
@[reducible, inline]
abbrev LieSubmodule.Quotient.mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :
M โ†’ M โงธ N

Map sending an element of M to the corresponding element of M โงธ N, when N is a Lie submodule of the Lie module M.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem LieSubmodule.Quotient.mk_eq_zero' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {m : M} :
    mk m = 0 โ†” m โˆˆ N
    source
    ๐Ÿ“ coverage
    theorem LieSubmodule.Quotient.is_quotient_mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} (m : M) :
    Quotient.mk'' m = mk m
    source
    ๐Ÿ”ธ coverage
    def LieSubmodule.Quotient.lieSubmoduleInvariant {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} [LieAlgebra R L] [LieModule R L M] :
    L โ†’โ‚—[R] โ†ฅ((โ†‘N).compatibleMaps โ†‘N)

    Given a Lie module M over a Lie algebra L, together with a Lie submodule N โŠ† M, there is a natural linear map from L to the endomorphisms of M leaving N invariant.

    Instances For
      source
      ๐Ÿ”ธ coverage
      def LieSubmodule.Quotient.actionAsEndoMap {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
      L โ†’โ‚—โ…Rโ† Module.End R (M โงธ N)

      Given a Lie module M over a Lie algebra L, together with a Lie submodule N โŠ† M, there is a natural Lie algebra morphism from L to the linear endomorphism of the quotient M/N.

      Instances For
        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance LieSubmodule.Quotient.actionAsEndoMapBracket {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
        Bracket L (M โงธ N)

        Given a Lie module M over a Lie algebra L, together with a Lie submodule N โŠ† M, there is a natural bracket action of L on the quotient M/N.

        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance LieSubmodule.Quotient.lieQuotientLieRingModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
        LieRingModule L (M โงธ N)
        source
        ๐Ÿ“ coverage
        instance LieSubmodule.Quotient.lieQuotientLieModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
        LieModule R L (M โงธ N)

        The quotient of a Lie module by a Lie submodule, is a Lie module.

        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance LieSubmodule.Quotient.lieQuotientHasBracket {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
        Bracket (L โงธ I) (L โงธ I)
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem LieSubmodule.Quotient.mk_bracket {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) :
        mk โ…x, yโ† = โ…mk x, mk yโ†
        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance LieSubmodule.Quotient.lieQuotientLieRing {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
        LieRing (L โงธ I)
        source
        ๐Ÿ”ธ coverage
        @[implicit_reducible]
        instance LieSubmodule.Quotient.lieQuotientLieAlgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
        LieAlgebra R (L โงธ I)
        source
        ๐Ÿ”ธ coverage
        def LieSubmodule.Quotient.mk' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
        M โ†’โ‚—โ…R,Lโ† M โงธ N

        LieSubmodule.Quotient.mk as a LieModuleHom.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem LieSubmodule.Quotient.mk'_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] (aโœ : M) :
          (mk' N) aโœ = mk aโœ
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem LieSubmodule.Quotient.surjective_mk' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
          Function.Surjective โ‡‘(mk' N)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem LieSubmodule.Quotient.range_mk' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
          (mk' N).range = โŠค
          source
          ๐Ÿ“ coverage
          instance LieSubmodule.Quotient.isNoetherian {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [IsNoetherian R M] :
          IsNoetherian R (M โงธ N)
          source
          ๐Ÿ“ coverage
          theorem LieSubmodule.Quotient.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] {m : M} :
          (mk' N) m = 0 โ†” m โˆˆ N
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem LieSubmodule.Quotient.mk'_ker {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
          (mk' N).ker = N
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem LieSubmodule.Quotient.map_mk'_eq_bot_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] :
          map (mk' N) N' = โŠฅ โ†” N' โ‰ค N
          source
          theorem LieSubmodule.Quotient.lieModuleHom_ext {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] โฆƒf g : M โงธ N โ†’โ‚—โ…R,Lโ† Mโฆ„ (h : f.comp (mk' N) = g.comp (mk' N)) :
          f = g

          Two LieModuleHoms from a quotient lie module are equal if their compositions with LieSubmodule.Quotient.mk' are equal.

          See note [partially-applied ext lemmas].

          source
          ๐Ÿ“ coverage
          theorem LieSubmodule.Quotient.lieModuleHom_ext_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} [LieAlgebra R L] [LieModule R L M] {f g : M โงธ N โ†’โ‚—โ…R,Lโ† M} :
          f = g โ†” f.comp (mk' N) = g.comp (mk' N)
          source
          ๐Ÿ“ coverage
          theorem LieSubmodule.Quotient.toEnd_comp_mk' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] [LieModule R L M] (x : L) :
          (LieModule.toEnd R L (M โงธ N)) x โˆ˜โ‚— โ†‘(mk' N) = โ†‘(mk' N) โˆ˜โ‚— (LieModule.toEnd R L M) x
          source
          ๐Ÿ”ธ coverage
          noncomputable def LieHom.quotKerEquivRange {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L โ†’โ‚—โ…Rโ† L') :
          (L โงธ f.ker) โ‰ƒโ‚—โ…Rโ† โ†ฅf.range

          The first isomorphism theorem for morphisms of Lie algebras.

          Instances For
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem LieHom.quotKerEquivRange_invFun {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L โ†’โ‚—โ…Rโ† L') (aโœ : โ†ฅ(โ†‘f).range) :
            f.quotKerEquivRange.invFun aโœ = (โ†‘f).quotKerEquivRange.invFun aโœ
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem LieHom.quotKerEquivRange_toFun {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L โ†’โ‚—โ…Rโ† L') (a : L โงธ (โ†‘f).ker) :
            f.quotKerEquivRange a = (โ†‘f).quotKerEquivRange a