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

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

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} :
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)
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)
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] :
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} :
@[inline, reducible]
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} :
MM N

Map sending an element of M to the corresponding element of M/N, when N is a lie_submodule of the lie_module N.

Instances For
    def LieSubmodule.Quotient.lieSubmoduleInvariant {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} :
    L →ₗ[R] { x // x Submodule.compatibleMaps N 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
      def LieSubmodule.Quotient.actionAsEndoMap {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :

      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
        instance LieSubmodule.Quotient.actionAsEndoMapBracket {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule 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.

        instance LieSubmodule.Quotient.lieQuotientLieRingModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
        instance LieSubmodule.Quotient.lieQuotientLieModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
        LieModule R L (M N)

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

        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)
        @[simp]
        theorem LieSubmodule.Quotient.mk'_toFun {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
        def LieSubmodule.Quotient.mk' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :

        LieSubmodule.Quotient.mk as a LieModuleHom.

        Instances For
          theorem LieSubmodule.Quotient.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) {m : M} :
          @[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} :
          @[simp]
          @[simp]

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

          See note [partially-applied ext lemmas].

          @[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') :
          @[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 LinearMap.ker f) :
          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') :

          The first isomorphism theorem for morphisms of Lie algebras.

          Instances For