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

• LieSubmodule.Quotient.lieQuotientLieModule
• LieSubmodule.Quotient.lieQuotientLieAlgebra

Tags

lie algebra, quotient

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.

Equations

• LieSubmodule.instHasQuotient = { quotient' := fun (N : LieSubmodule R L M) => M ⧸ ↑N }

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)

Equations

• LieSubmodule.Quotient.addCommGroup = Submodule.Quotient.addCommGroup ↑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} {S : Type u_1} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S (M ⧸ N)

Equations

• LieSubmodule.Quotient.module' = Submodule.Quotient.module' ↑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)

Equations

• LieSubmodule.Quotient.module = Submodule.Quotient.module ↑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] : IsCentralScalar S (M ⧸ N)

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)

Equations

• LieSubmodule.Quotient.inhabited = { default := 0 }

@[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 N.

Equations

• LieSubmodule.Quotient.mk = Submodule.Quotient.mk

@[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

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

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.

Equations

• LieSubmodule.Quotient.lieSubmoduleInvariant = LinearMap.codRestrict ((↑N).compatibleMaps ↑N) ↑(LieModule.toEnd R L M) ⋯

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.

Equations

• LieSubmodule.Quotient.actionAsEndoMap N = { toLinearMap := (↑N).mapQLinear ↑N ∘ₗ LieSubmodule.Quotient.lieSubmoduleInvariant, map_lie' := ⋯ }

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.

Equations

• LieSubmodule.Quotient.actionAsEndoMapBracket N = { bracket := fun (x : L) (n : M ⧸ N) => ((LieSubmodule.Quotient.actionAsEndoMap N) x) n }

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)

Equations

• LieSubmodule.Quotient.lieQuotientLieRingModule N = { toBracket := LieSubmodule.Quotient.actionAsEndoMapBracket N, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

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.

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)

Equations

• LieSubmodule.Quotient.lieQuotientHasBracket I = { bracket := fun (x y : L ⧸ I) => Quotient.liftOn₂' x y (fun (x' y' : L) => LieSubmodule.Quotient.mk ⁅x', y'⁆) ⋯ }

@[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⁆

instance LieSubmodule.Quotient.lieQuotientLieRing {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing (L ⧸ I)

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• LieSubmodule.Quotient.lieQuotientLieAlgebra I = { toModule := LieSubmodule.Quotient.module, lie_smul := ⋯ }

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.

Equations

• LieSubmodule.Quotient.mk' N = { toFun := LieSubmodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[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✝

@[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)

@[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 = ⊤

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)

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

@[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

@[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

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].

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)

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

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.

Equations

• f.quotKerEquivRange = { toFun := ⇑(↑f).quotKerEquivRange, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := (↑f).quotKerEquivRange.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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✝ : ↥(LinearMap.range ↑f)) : f.quotKerEquivRange.invFun a✝ = (↑f).quotKerEquivRange.invFun a✝

@[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) : f.quotKerEquivRange a = (↑f).quotKerEquivRange a