The adjoint representation modulo a Lie ideal

For a connected affine group over an algebraically closed field of characteristic zero, every Lie ideal is an adjoint subrepresentation. The quotient therefore carries a rational representation whose differential is the induced Lie bracket. If the quotient Lie algebra has zero center, the scheme-theoretic kernel of this representation has precisely the given Lie ideal as its Lie algebra. In particular this applies to the solvable radical.

This realizes the Lie radical by a closed normal subgroup before taking its identity component, allowing comparison with the solvable radical of the algebraic group.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 10 and 22.
• J. E. Humphreys, Linear Algebraic Groups, §13.

The construction uses LieIdeal.toAdjointSubcomodule and the quotient-comodule construction. The radical case uses LieAlgebra.hasTrivialRadical_quotient_radical.

@[instance_reducible]

noncomputable instance LieIdeal.quotientAdjointComodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) : TauCeti.Comodule k (↑H.obj) (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj) ⧸ I)

The rational adjoint action on the quotient of the tangent Lie algebra by a Lie ideal. Connectedness and characteristic zero ensure that the ideal is an adjoint subcomodule.

noncomputable def LieIdeal.quotientAdjointMkQ {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) : TauCeti.Comodule.Hom k (↑H.obj) (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj)) (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj) ⧸ I)

Projection to a Lie-ideal quotient is a morphism for the rational adjoint action.

@[simp]

theorem LieIdeal.quotientAdjointMkQ_apply {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) (x : Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj)) : I.quotientAdjointMkQ x = I.mkQ x

The adjoint-comodule projection is the usual Lie-algebra quotient map.

@[simp]

theorem LieIdeal.differential_quotientAdjointComodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) (d : Derivation k (↑H.obj) (TauCeti.Bialgebra.CounitAlgebra k (↑H.obj) k)) (x : Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj)) : (TauCeti.Comodule.differential d) (I.mkQ x) = I.mkQ ⁅Derivation.cotangentDualLieEquiv.symm d, x⁆

The differential of the quotient adjoint representation is the Lie bracket modulo the ideal.

theorem LieIdeal.differential_quotientAdjointComodule_eq_zero_iff {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) (d : Derivation k (↑H.obj) (TauCeti.Bialgebra.CounitAlgebra k (↑H.obj) k)) : TauCeti.Comodule.differential d = 0 ↔ I.mkQ (Derivation.cotangentDualLieEquiv.symm d) ∈ LieAlgebra.center k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj) ⧸ I)

The tangent vectors acting trivially on the quotient adjoint representation are exactly the inverse image of the center of the quotient Lie algebra.

theorem LieIdeal.mem_lieSubalgebra_kernel_quotientAdjoint_iff {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) (hI : LieAlgebra.center k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj) ⧸ I) = ⊥) {n : ℕ} (b : Module.Basis (Fin n) k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj) ⧸ I)) (d : Derivation k (↑H.obj) (TauCeti.Bialgebra.CounitAlgebra k (↑H.obj) k)) : d ∈ (TauCeti.CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.ofHom (TauCeti.Comodule.coordinateBialgHom b))).lieSubalgebra ↔ Derivation.cotangentDualLieEquiv.symm d ∈ I

If the quotient Lie algebra has zero center, the kernel of its rational adjoint quotient representation has Lie algebra exactly the original ideal. The basis only specifies the coordinate morphism to the general linear group.

theorem TauCeti.FiniteTypeCommHopfAlgCat.exists_isNormal_lieSubalgebra_eq_radical {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [ConnectedSpace (PrimeSpectrum ↑H.obj)] : ∃ (I : HopfIdeal k ↑H.obj), I.IsNormal ∧ I.lieSubalgebra = LieSubalgebra.comap Derivation.cotangentDualLieEquiv.symm.toLieHom (↑k (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj)) (LieAlgebra.radical k (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))))

The solvable radical of the tangent Lie algebra of a connected affine group in characteristic zero is the Lie algebra of a closed normal subgroup. The subgroup can be chosen as the kernel of the adjoint representation modulo the Lie radical.