Homomorphisms from quotients by Lie ideals

Mathlib equips the quotient of a Lie algebra by a Lie ideal with its Lie algebra structure and provides the quotient map as a morphism of Lie modules. This file records that map as a homomorphism of Lie algebras and gives its universal property: a homomorphism killing the ideal factors uniquely through the quotient. A Lie subalgebra complementary to the ideal is isomorphic to the quotient. For a surjective homomorphism, the induced map from the quotient by its kernel is an isomorphism, which is the first isomorphism theorem.

These declarations live in the root LieIdeal and LieHom namespaces, extending Mathlib's API and supporting receiver notation on the ideal and the homomorphism.

Main definitions

• LieIdeal.mkQ: the quotient map L →ₗ⁅R⁆ L ⧸ I.
• LieIdeal.liftQ: the homomorphism L ⧸ I →ₗ⁅R⁆ L' induced by a homomorphism L →ₗ⁅R⁆ L' whose kernel contains I.
• LieIdeal.quotientEquivOfIsCompl: the isomorphism L ⧸ I ≃ₗ⁅R⁆ S for a Lie subalgebra S complementary to I.
• LieHom.quotKerEquivOfSurjective: the first isomorphism theorem, identifying the quotient of L by the kernel of a surjective homomorphism with its target.

Main results

• LieIdeal.mkQ_surjective: every quotient class has a representative in the original Lie algebra.
• LieIdeal.liftQ_mkQ: the lifted homomorphism restricts to the original one along the quotient map.
• LieIdeal.coe_liftQ: the lifted homomorphism is Submodule.liftQ of the underlying linear map.
• LieIdeal.liftQ_injective and LieIdeal.liftQ_surjective: the lifted homomorphism is injective when the ideal exhausts the kernel, and surjective when the original homomorphism is.
• LieIdeal.lieHom_qext: two homomorphisms from the quotient are equal when they agree after the quotient map.
• LieIdeal.eq_liftQ: the lifted homomorphism is the unique such factorization.
• LieIdeal.ker_liftQ_mkQ: for ideals J ≤ I, the kernel of L ⧸ J → L ⧸ I is the image of I.
• LieIdeal.mkQ_comp_incl_surjective: a Lie subalgebra P with I + P = L maps onto L ⧸ I.
• LieIdeal.ker_mkQ_comp_incl: the kernel of P → L ⧸ I is the ideal I ∩ P of P.
• LieIdeal.isCompl_map_incl: a complement of I ∩ P inside a supplement P of I is a complement of I in L.

def LieIdeal.mkQ {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : L →ₗ⁅R⁆ L ⧸ I

The quotient map L → L ⧸ I as a homomorphism of Lie algebras.

Its underlying function is Mathlib's LieSubmodule.Quotient.mk, sending each element to its quotient class.

Equations

• I.mkQ = { toLinearMap := (↑I).mkQ, map_lie' := ⋯ }

@[simp]

theorem LieIdeal.mkQ_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) : I.mkQ x = LieSubmodule.Quotient.mk x

The quotient homomorphism sends an element to its class.

theorem LieIdeal.mkQ_surjective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Function.Surjective ⇑I.mkQ

Every element of the quotient has a representative in the original Lie algebra.

@[simp]

theorem LieIdeal.ker_mkQ {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.mkQ.ker = I

The kernel of the quotient homomorphism is the ideal quotiented by.

def LieIdeal.liftQ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) : L ⧸ I →ₗ⁅R⁆ L'

The homomorphism L ⧸ I →ₗ⁅R⁆ L' induced by a homomorphism f : L →ₗ⁅R⁆ L' whose kernel contains the ideal I.

Equations

• I.liftQ f h = { toLinearMap := (↑I).liftQ (↑f) h, map_lie' := ⋯ }

@[simp]

theorem LieIdeal.liftQ_apply {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) (x : L) : (I.liftQ f h) (LieSubmodule.Quotient.mk x) = f x

The induced homomorphism on the quotient sends the class of x to f x.

theorem LieIdeal.coe_liftQ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) : ↑(I.liftQ f h) = (↑I).liftQ ↑f ⋯

The linear map underlying the induced homomorphism on the quotient is Submodule.liftQ of the linear map underlying f.

theorem LieIdeal.liftQ_injective {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) (h' : f.ker ≤ I) : Function.Injective ⇑(I.liftQ f h)

The homomorphism induced on the quotient is injective as soon as the ideal quotiented by exhausts the kernel.

theorem LieIdeal.liftQ_surjective {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) (h' : Function.Surjective ⇑f) : Function.Surjective ⇑(I.liftQ f h)

The homomorphism induced on the quotient by a surjective homomorphism is surjective.

@[simp]

theorem LieIdeal.liftQ_mkQ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L') (h : I ≤ f.ker) : (I.liftQ f h).comp I.mkQ = f

The induced homomorphism on the quotient composed with the quotient map is the original homomorphism.

theorem LieIdeal.lieHom_qext {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) {g₁ g₂ : L ⧸ I →ₗ⁅R⁆ L'} (h : ∀ (x : L), g₁ (I.mkQ x) = g₂ (I.mkQ x)) : g₁ = g₂

Two homomorphisms out of L ⧸ I that agree after composition with the quotient map are equal.

theorem LieIdeal.lieHom_qext_iff {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {I : LieIdeal R L} {g₁ g₂ : L ⧸ I →ₗ⁅R⁆ L'} : g₁ = g₂ ↔ ∀ (x : L), g₁ (I.mkQ x) = g₂ (I.mkQ x)

theorem LieIdeal.eq_liftQ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) {f : L →ₗ⁅R⁆ L'} {h : I ≤ f.ker} {g : L ⧸ I →ₗ⁅R⁆ L'} (hg : ∀ (x : L), g (I.mkQ x) = f x) : g = I.liftQ f h

The factorization of LieIdeal.liftQ is the only one: a homomorphism out of L ⧸ I restricting to f along the quotient map is I.liftQ f h.

theorem LieIdeal.ker_liftQ_mkQ {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {J : LieIdeal R L} (h : J ≤ I.mkQ.ker) : (J.liftQ I.mkQ h).ker = map J.mkQ I

For ideals J ≤ I, the kernel of the induced map L ⧸ J → L ⧸ I is the image of I in L ⧸ J.

theorem LieIdeal.mkQ_comp_incl_surjective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {P : LieSubalgebra R L} (hIP : Codisjoint (↑I) P.toSubmodule) : Function.Surjective ⇑(I.mkQ.comp P.incl)

A Lie subalgebra P supplementing an ideal I, in the sense that I + P = L, maps onto the quotient L ⧸ I.

@[simp]

theorem LieIdeal.ker_mkQ_comp_incl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {P : LieSubalgebra R L} : (I.mkQ.comp P.incl).ker = comap P.incl I

The kernel of the map P → L ⧸ I induced by a Lie subalgebra P is the ideal I ∩ P of P.

noncomputable def LieIdeal.quotientEquivOfIsCompl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (S : LieSubalgebra R L) (h : IsCompl (↑I) S.toSubmodule) : (L ⧸ I) ≃ₗ⁅R⁆ ↥S

A Lie subalgebra S complementary to a Lie ideal I is isomorphic to the quotient L ⧸ I, the class of x : S corresponding to x. This is the Lie algebra version of Submodule.quotientEquivOfIsCompl, which is its underlying linear equivalence (LieIdeal.toLinearEquiv_quotientEquivOfIsCompl).

Equations

• I.quotientEquivOfIsCompl S h = (LieEquiv.ofBijective (I.mkQ.comp S.incl) ⋯).symm

@[simp]

theorem LieIdeal.quotientEquivOfIsCompl_symm_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (S : LieSubalgebra R L) (h : IsCompl (↑I) S.toSubmodule) (x : ↥S) : (I.quotientEquivOfIsCompl S h).symm x = LieSubmodule.Quotient.mk ↑x

The inverse of LieIdeal.quotientEquivOfIsCompl sends x : S to its class.

@[simp]

theorem LieIdeal.quotientEquivOfIsCompl_apply_mk_coe {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (S : LieSubalgebra R L) (h : IsCompl (↑I) S.toSubmodule) (x : ↥S) : (I.quotientEquivOfIsCompl S h) (LieSubmodule.Quotient.mk ↑x) = x

LieIdeal.quotientEquivOfIsCompl sends the class of x : S to x.

theorem LieIdeal.toLinearEquiv_quotientEquivOfIsCompl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (S : LieSubalgebra R L) (h : IsCompl (↑I) S.toSubmodule) : (I.quotientEquivOfIsCompl S h).toLinearEquiv = (↑I).quotientEquivOfIsCompl S.toSubmodule h

The linear equivalence underlying LieIdeal.quotientEquivOfIsCompl is Submodule.quotientEquivOfIsCompl.

noncomputable def LieHom.quotKerEquivOfSurjective {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') (hf : Function.Surjective ⇑f) : (L ⧸ f.ker) ≃ₗ⁅R⁆ L'

The first isomorphism theorem for a surjective homomorphism of Lie algebras: the quotient by its kernel is isomorphic to the target.

Equations

• f.quotKerEquivOfSurjective hf = LieEquiv.ofBijective (f.ker.liftQ f ⋯) ⋯

@[simp]

theorem LieHom.quotKerEquivOfSurjective_apply_mk {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') (hf : Function.Surjective ⇑f) (x : L) : (f.quotKerEquivOfSurjective hf) (LieSubmodule.Quotient.mk x) = f x

The first isomorphism theorem sends the class of x to f x.

@[simp]

theorem LieHom.quotKerEquivOfSurjective_symm_apply {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') (hf : Function.Surjective ⇑f) (x : L) : (f.quotKerEquivOfSurjective hf).symm (f x) = LieSubmodule.Quotient.mk x

The inverse of the first isomorphism theorem sends f x to the class of x.

theorem LieIdeal.isCompl_map_incl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {P : LieSubalgebra R L} (hIP : Codisjoint (↑I) P.toSubmodule) {J : LieSubalgebra R ↥P} (hJ : IsCompl (↑(comap P.incl I)) J.toSubmodule) : IsCompl (↑I) (LieSubalgebra.map P.incl J).toSubmodule

A complement inside a supplement. If a Lie subalgebra P supplements an ideal I, then a complement in P of the ideal I ∩ P of P is a complement of I in L.