Recognising a semidirect sum from an ideal and a complementary subalgebra

Mathlib's LieAlgebra.SemiDirectSum K L ψ, written K ⋊⁅ψ⁆ L, is the external semidirect sum of two Lie algebras twisted by a Lie homomorphism ψ : L →ₗ⁅R⁆ LieDerivation R K K. A Lie algebra L is presented internally as a semidirect sum by an ideal S, a Lie subalgebra H, and the requirement that the two underlying submodules be complementary. This file connects the two descriptions.

The twisting homomorphism is the adjoint action. An ideal S of L is stable under ⁅x, -⁆ for every x : L, and the Jacobi identity says exactly that the resulting endomorphism of S is a Lie derivation; the assignment is itself a homomorphism of Lie algebras, so it gives LieIdeal.ad S : L →ₗ⁅R⁆ LieDerivation R S S. Restricting it along the inclusion of a Lie subalgebra H produces the ψ that a semidirect sum needs, and when S and H are complementary as submodules, (s, h) ↦ s + h is an isomorphism ↥S ⋊⁅ψ⁆ ↥H ≃ₗ⁅R⁆ L.

In the converse direction, an external semidirect sum K ⋊⁅ψ⁆ L carries such internal data tautologically: the kernel of the projection to L is an ideal, the range of the inclusion of L is a Lie subalgebra, and the two are complementary. So neither presentation is more general than the other, and a theorem may be stated against the external form without loss.

The file also records two closure properties of the external semidirect sum. It is module-finite when both factors are, by transport along the linear equivalence toProdl with the product, and solvable when both factors are, because it is an extension of L by K: the range of inl is the kernel of the surjection projr.

Main definitions

• LieIdeal.ad: the adjoint action of L on an ideal S, as a Lie homomorphism L →ₗ⁅R⁆ LieDerivation R S S. The ψ attached to a Lie subalgebra H is the composite (LieIdeal.ad S).comp H.incl.
• LieIdeal.semiDirectSumHom: the Lie homomorphism ↥S ⋊⁅ψ⁆ ↥H →ₗ⁅R⁆ L given by (s, h) ↦ s + h.
• LieIdeal.semiDirectSumEquiv: that homomorphism as an isomorphism, when the underlying submodules of S and H are complementary.

Main statements

• LieIdeal.nonempty_lieEquiv_semiDirectSum and LieIdeal.exists_lieEquiv_semiDirectSum: the recognition theorem, in the Nonempty (L ≃ₗ⁅R⁆ ↥S ⋊⁅ψ⁆ ↥H) form that consumers of a splitting hypothesis take as input.
• LieIdeal.semiDirectSumEquiv_symm_apply_right_eq_zero_iff and LieIdeal.semiDirectSumEquiv_symm_apply_left_eq_zero_iff: the recognition isomorphism carries S and H onto the two factors, which is what lets a statement about the left factor be read back as a statement about the ideal.
• LieAlgebra.SemiDirectSum.isCompl_ker_projr_range_inr: the converse, that an external semidirect sum is internally presented by the kernel of projr and the range of inr, with LieAlgebra.SemiDirectSum.exists_lieEquiv_semiDirectSum_ker_projr the resulting reconstruction.
• Instances Module.Finite R (K ⋊⁅ψ⁆ L) and IsSolvable (K ⋊⁅ψ⁆ L): an external semidirect sum of module-finite, resp. solvable, Lie algebras is module-finite, resp. solvable.

References

• [W. Fulton and J. Harris, Representation Theory: A First Course][fulton-harris1991], Appendix E, §E.2, where Ado's theorem extends a representation of a solvable ideal across a complementary subalgebra.

def LieIdeal.ad {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) : L →ₗ⁅R⁆ LieDerivation R ↥S ↥S

The adjoint action of a Lie algebra on one of its ideals, as a homomorphism into the Lie algebra of Lie derivations of that ideal. The ideal is stable under ⁅x, -⁆, and the Jacobi identity is both the Leibniz rule for each ⁅x, -⁆ and the statement that x ↦ ⁅x, -⁆ preserves brackets.

Equations

• S.ad = { toFun := fun (x : L) => let __LinearMap := (LieModule.toEnd R L ↥S) x; { toLinearMap := __LinearMap, leibniz' := ⋯ }, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieIdeal.ad_apply_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (x : L) (a : ↥S) : (S.ad x) a = ⁅x, a⁆

def LieIdeal.semiDirectSumHom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) : ↥S ⋊⁅S.ad.comp H.incl⁆ ↥H →ₗ⁅R⁆ L

The canonical map from the semidirect sum of an ideal S and a Lie subalgebra H of L, twisted by the adjoint action of H on S, back to L: it adds the two components. It is a homomorphism of Lie algebras because the twist is the adjoint action.

Equations

• S.semiDirectSumHom H = { toFun := fun (z : ↥S ⋊⁅S.ad.comp H.incl⁆ ↥H) => ↑z.left + ↑z.right, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieIdeal.semiDirectSumHom_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (z : ↥S ⋊⁅S.ad.comp H.incl⁆ ↥H) : (S.semiDirectSumHom H) z = ↑z.left + ↑z.right

theorem LieIdeal.semiDirectSumHom_injective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {S : LieIdeal R L} {H : LieSubalgebra R L} (h : Disjoint (↑S) H.toSubmodule) : Function.Injective ⇑(S.semiDirectSumHom H)

theorem LieIdeal.semiDirectSumHom_surjective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {S : LieIdeal R L} {H : LieSubalgebra R L} (h : Codisjoint (↑S) H.toSubmodule) : Function.Surjective ⇑(S.semiDirectSumHom H)

theorem LieIdeal.semiDirectSumHom_bijective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {S : LieIdeal R L} {H : LieSubalgebra R L} (h : IsCompl (↑S) H.toSubmodule) : Function.Bijective ⇑(S.semiDirectSumHom H)

noncomputable def LieIdeal.semiDirectSumEquiv {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) : (↥S ⋊⁅S.ad.comp H.incl⁆ ↥H) ≃ₗ⁅R⁆ L

Internal recognition of a semidirect sum. An ideal S and a Lie subalgebra H of L whose underlying submodules are complementary exhibit L as the semidirect sum of S and H, twisted by the adjoint action of H on S.

Equations

• S.semiDirectSumEquiv H h = LieEquiv.ofBijective (S.semiDirectSumHom H) ⋯

@[simp]

theorem LieIdeal.semiDirectSumEquiv_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (z : ↥S ⋊⁅S.ad.comp H.incl⁆ ↥H) : (S.semiDirectSumEquiv H h) z = ↑z.left + ↑z.right

theorem LieIdeal.semiDirectSumEquiv_inl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (s : ↥S) : (S.semiDirectSumEquiv H h) ((LieAlgebra.SemiDirectSum.inl (S.ad.comp H.incl)) s) = ↑s

theorem LieIdeal.semiDirectSumEquiv_inr {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (t : ↥H) : (S.semiDirectSumEquiv H h) ((LieAlgebra.SemiDirectSum.inr (S.ad.comp H.incl)) t) = ↑t

@[simp]

theorem LieIdeal.semiDirectSumEquiv_symm_coe_left {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (s : ↥S) : (S.semiDirectSumEquiv H h).symm ↑s = (LieAlgebra.SemiDirectSum.inl (S.ad.comp H.incl)) s

@[simp]

theorem LieIdeal.semiDirectSumEquiv_symm_coe_right {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (t : ↥H) : (S.semiDirectSumEquiv H h).symm ↑t = (LieAlgebra.SemiDirectSum.inr (S.ad.comp H.incl)) t

theorem LieIdeal.semiDirectSumEquiv_symm_of_mem_left {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) {x : L} (hx : x ∈ S) : (S.semiDirectSumEquiv H h).symm x = (LieAlgebra.SemiDirectSum.inl (S.ad.comp H.incl)) ⟨x, hx⟩

theorem LieIdeal.semiDirectSumEquiv_symm_of_mem_right {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) {x : L} (hx : x ∈ H) : (S.semiDirectSumEquiv H h).symm x = (LieAlgebra.SemiDirectSum.inr (S.ad.comp H.incl)) ⟨x, hx⟩

theorem LieIdeal.semiDirectSumEquiv_symm_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) (x : L) : (S.semiDirectSumEquiv H h).symm x = { left := (((↑S).prodEquivOfIsCompl H.toSubmodule h).symm x).1, right := (((↑S).prodEquivOfIsCompl H.toSubmodule h).symm x).2 }

The inverse of the recognition isomorphism is Mathlib's decomposition of an element of L along the complementary pair S.toSubmodule, H.toSubmodule, read as an element of the semidirect sum.

@[simp]

theorem LieIdeal.semiDirectSumEquiv_symm_apply_right_eq_zero_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) {x : L} : ((S.semiDirectSumEquiv H h).symm x).right = 0 ↔ x ∈ S

The recognition isomorphism identifies the ideal S with the left factor: an element of L lies in S exactly when its preimage has vanishing right component.

@[simp]

theorem LieIdeal.semiDirectSumEquiv_symm_apply_left_eq_zero_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) {x : L} : ((S.semiDirectSumEquiv H h).symm x).left = 0 ↔ x ∈ H

The recognition isomorphism identifies the Lie subalgebra H with the right factor: an element of L lies in H exactly when its preimage has vanishing left component.

theorem LieIdeal.nonempty_lieEquiv_semiDirectSum {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) : Nonempty (L ≃ₗ⁅R⁆ ↥S ⋊⁅S.ad.comp H.incl⁆ ↥H)

The recognition theorem in the external form a splitting hypothesis is stated in: an ideal and a complementary Lie subalgebra make L isomorphic to a semidirect sum.

theorem LieIdeal.exists_lieEquiv_semiDirectSum {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (S : LieIdeal R L) (H : LieSubalgebra R L) (h : IsCompl (↑S) H.toSubmodule) : ∃ (ψ : ↥H →ₗ⁅R⁆ LieDerivation R ↥S ↥S), Nonempty (L ≃ₗ⁅R⁆ ↥S ⋊⁅ψ⁆ ↥H)

The recognition theorem with the twisting homomorphism existentially quantified, the form in which a Levi-style decomposition theorem delivers its conclusion.

instance LieAlgebra.SemiDirectSum.instFinite_leanPool {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [LieRing K] [LieAlgebra R K] [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) [Module.Finite R K] [Module.Finite R L] : Module.Finite R (K ⋊⁅ψ⁆ L)

A semidirect sum of module-finite Lie algebras is module-finite.

instance LieAlgebra.SemiDirectSum.instIsSolvable_leanPool {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [LieRing K] [LieAlgebra R K] [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) [IsSolvable K] [IsSolvable L] : IsSolvable (K ⋊⁅ψ⁆ L)

A semidirect sum of solvable Lie algebras is solvable.

theorem LieAlgebra.SemiDirectSum.mem_range_inr {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [LieRing K] [LieAlgebra R K] [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {z : K ⋊⁅ψ⁆ L} : z ∈ (inr ψ).range ↔ z.left = 0

The range of the inclusion of the right factor consists of the elements whose left component vanishes. This is not a simp lemma: Mathlib's LieHom.mem_range is already @[simp] and rewrites the left-hand side to ∃ y, inr ψ y = z.

theorem LieAlgebra.SemiDirectSum.isCompl_ker_projr_range_inr {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [LieRing K] [LieAlgebra R K] [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : IsCompl (↑(projr ψ).ker) (inr ψ).range.toSubmodule

An external semidirect sum carries the internal data that recognises it: the kernel of the projection onto the right factor is an ideal, the range of the inclusion of the right factor is a Lie subalgebra, and their underlying submodules are complementary.

theorem LieAlgebra.SemiDirectSum.exists_lieEquiv_semiDirectSum_ker_projr {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [LieRing K] [LieAlgebra R K] [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : ∃ (ψ' : ↥(inr ψ).range →ₗ⁅R⁆ LieDerivation R ↥(projr ψ).ker ↥(projr ψ).ker), Nonempty ((K ⋊⁅ψ⁆ L) ≃ₗ⁅R⁆ ↥(projr ψ).ker ⋊⁅ψ'⁆ ↥(inr ψ).range)

Every external semidirect sum is reconstructed by the internal recognition theorem applied to the kernel of projr and the range of inr. Nothing is lost by stating a splitting hypothesis in the external form.