The Lie ideal of a normal closed subgroup

The Lie algebra of a normal closed subgroup of an affine group scheme is an ideal in the ambient Lie algebra. First, scheme-theoretic normality makes its tangent space stable under conjugation by every algebra-valued point. Applying this to a dual-number point gives stability under the Lie bracket. This works over commutative rings, without smoothness, reducedness, or finite-type assumptions, and retains infinitesimal normal subgroups in positive characteristic.

The resulting HopfIdeal.IsNormal.lieIdeal has the same underlying submodule as the existing closed-subgroup Lie subalgebra: its elements are exactly the counit-valued derivations vanishing on the defining Hopf ideal. It allows normal subgroup constructions to be used in the ideal and quotient APIs for Lie algebras.

References

• J. S. Milne, Algebraic Groups (2017), §10, the Lie algebra and adjoint representation.
• J. C. Jantzen, Representations of Algebraic Groups, I.7.

theorem TauCeti.HopfIdeal.IsNormal.adDerivation_mem_lieSubalgebra {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {I : HopfIdeal R H} (hI : I.IsNormal) (g : WithConv (H →ₐ[R] Bialgebra.CounitAlgebra R H B)) {d : Derivation R H (Bialgebra.CounitAlgebra R H B)} (hd : d ∈ I.lieSubalgebra) : Derivation.adDerivation B g d ∈ I.lieSubalgebra

The Lie algebra of a normal closed subgroup is stable under the adjoint action of every algebra-valued point of the ambient group.

theorem TauCeti.HopfIdeal.IsNormal.lie_mem_lieSubalgebra {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {I : HopfIdeal R H} (hI : I.IsNormal) (d : Derivation R H (Bialgebra.CounitAlgebra R H B)) {e : Derivation R H (Bialgebra.CounitAlgebra R H B)} (he : e ∈ I.lieSubalgebra) : ⁅d, e⁆ ∈ I.lieSubalgebra

Bracketing an ambient tangent vector with a tangent vector of a normal closed subgroup again gives a tangent vector of that subgroup.

noncomputable def TauCeti.HopfIdeal.IsNormal.lieIdeal {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {I : HopfIdeal R H} (hI : I.IsNormal) : LieIdeal B (Derivation R H (Bialgebra.CounitAlgebra R H B))

The Lie ideal of the normal closed subgroup defined by I, inside the ambient tangent Lie algebra with coefficients in B.

Equations

• hI.lieIdeal = { toSubmodule := I.lieSubalgebra.toSubmodule, lie_mem := ⋯ }

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.lieIdeal_toLieSubalgebra {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {I : HopfIdeal R H} (hI : I.IsNormal) : LieIdeal.toLieSubalgebra B (Derivation R H (Bialgebra.CounitAlgebra R H B)) hI.lieIdeal = I.lieSubalgebra

The underlying Lie subalgebra of the normal-subgroup Lie ideal is the closed-subgroup Lie subalgebra. To identify their underlying submodules, use rw [← LieIdeal.toLieSubalgebra_toSubmodule, hI.lieIdeal_toLieSubalgebra].

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.mem_lieIdeal_iff {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {I : HopfIdeal R H} (hI : I.IsNormal) (d : Derivation R H (Bialgebra.CounitAlgebra R H B)) : d ∈ hI.lieIdeal ↔ ∀ x ∈ I.toIdeal, d x = 0

Membership in the normal-subgroup Lie ideal is vanishing on its defining Hopf ideal.