The Lie algebra of a closed affine subgroup

A Hopf ideal I in a commutative Hopf algebra H presents the closed affine subgroup Spec (H ⧸ I) ↪ Spec H. The differential of this inclusion is contravariantly induced by the quotient bialgebra morphism H → H ⧸ I. This file identifies that differential as an injective Lie algebra morphism and characterizes its image: it consists exactly of the counit-valued derivations of H which vanish on I.

Thus the Lie algebra of the closed subgroup is canonically a Lie subalgebra of the Lie algebra of the ambient group. This is the coordinate-Hopf-algebra form of the ReductiveGroups roadmap's Layer 2 target "the Lie algebra of a closed subgroup".

Main declarations

• TauCeti.HopfIdeal.quotientLieHom: the coefficient-linear differential of the closed-subgroup inclusion.
• TauCeti.HopfIdeal.lieSubalgebra: its image in the ambient Lie algebra.
• TauCeti.HopfIdeal.mem_lieSubalgebra_iff, TauCeti.HopfIdeal.mem_lieSubalgebra_iff_of_toIdeal_eq_span: membership means vanishing on the Hopf ideal, or just on a chosen set of ideal generators.
• TauCeti.HopfIdeal.quotientLieEquiv: the closed subgroup's Lie algebra is Lie-equivalent to that image.
• TauCeti.HopfIdeal.lieSubalgebra_map: tangent Lie algebras commute with inverse images of closed subgroups under arbitrary group homomorphisms.

References

This is the affine coordinate-ring description in J. S. Milne, Algebraic Groups (2017), §10.a: the tangent space of a closed subgroup is the subspace of tangent derivations annihilating its defining ideal. The Lie bracket and differential use Tau Ceti's convolution-derivation API; the quotient Hopf algebra itself is Mathlib's Bialgebra.Quotient construction.

noncomputable def TauCeti.HopfIdeal.quotientLieHom {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B) →ₗ⁅B⁆ Derivation R H (Bialgebra.CounitAlgebra R H B)

The differential of the closed-subgroup inclusion presented by a Hopf ideal I.

On coordinate rings the inclusion is represented by the quotient bialgebra morphism H → H ⧸ I; the differential therefore sends a derivation of the quotient to its precomposition with the quotient map.

Equations

• I.quotientLieHom = TauCeti.derivationCompLieHom (Bialgebra.Quotient.mkBialgHom I.toIdeal)

theorem TauCeti.HopfIdeal.quotientLieHom_apply {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (d : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) : I.quotientLieHom d = (derivationComp (Bialgebra.Quotient.mkBialgHom I.toIdeal)) d

The differential of a closed-subgroup inclusion is precomposition with the quotient map.

@[simp]

theorem TauCeti.HopfIdeal.quotientLieHom_adDerivation {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (g : WithConv (H ⧸ I.toIdeal →ₐ[R] Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) (d : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) : I.quotientLieHom (Derivation.adDerivation B g d) = Derivation.adDerivation B ((AlgHom.mapDomain (Bialgebra.Quotient.mkBialgHom I.toIdeal)) g) (I.quotientLieHom d)

The differential of a closed-subgroup inclusion intertwines the adjoint actions.

@[simp]

theorem TauCeti.HopfIdeal.quotientLieHom_apply_apply {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (d : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) (x : H) : (I.quotientLieHom d) x = (Bialgebra.CounitAlgebra.algEquivSelf R (H ⧸ I.toIdeal) B) (d ((Ideal.Quotient.mkₐ R I.toIdeal) x))

The closed-subgroup differential acts by precomposition with the quotient map.

@[simp]

theorem TauCeti.HopfIdeal.quotientLieHom_mapValue {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) {C : Type u_1} [CommRing C] [Algebra R C] (φ : B →ₐ[R] C) (d : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) : I.quotientLieHom ((Derivation.mapValue φ) d) = (Derivation.mapValue φ) (I.quotientLieHom d)

The closed-subgroup differential commutes with extension of the coefficient algebra.

theorem TauCeti.HopfIdeal.quotientLieHom_injective {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) : Function.Injective ⇑I.quotientLieHom

The differential of a closed-subgroup inclusion is injective.

noncomputable def TauCeti.HopfIdeal.lieSubalgebra {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) : LieSubalgebra B (Derivation R H (Bialgebra.CounitAlgebra R H B))

The Lie subalgebra of the ambient tangent Lie algebra cut out by a Hopf ideal.

It is defined intrinsically as the range of the closed-subgroup differential; membership is characterized without reference to this range by mem_lieSubalgebra_iff.

Equations

• I.lieSubalgebra = I.quotientLieHom.range

@[simp]

theorem TauCeti.HopfIdeal.mem_lieSubalgebra_iff {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (d : Derivation R H (Bialgebra.CounitAlgebra R H B)) : d ∈ I.lieSubalgebra ↔ ∀ x ∈ I.toIdeal, d x = 0

A tangent derivation belongs to the Lie algebra of the closed subgroup defined by I exactly when it vanishes on the defining Hopf ideal.

theorem TauCeti.HopfIdeal.mem_lieSubalgebra_iff_of_toIdeal_eq_span {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) {S : Set H} (hI : I.toIdeal = Ideal.span S) (d : Derivation R H (Bialgebra.CounitAlgebra R H B)) : d ∈ I.lieSubalgebra ↔ ∀ x ∈ S, d x = 0

When a Hopf ideal is generated by S, membership in its tangent Lie subalgebra is equivalent to vanishing of the derivation on the generators in S.

theorem TauCeti.HopfIdeal.lieSubalgebra_map {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] {K : Type u_1} [CommRing K] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) : (I.map f).lieSubalgebra = LieSubalgebra.comap (derivationCompLieHom f) I.lieSubalgebra

Taking the inverse image of a closed subgroup commutes with taking its tangent Lie algebra. On coordinate rings the inverse image is presented by the image Hopf ideal. No surjectivity assumption on the coordinate morphism is needed.

noncomputable def TauCeti.HopfIdeal.quotientLieEquiv {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B) ≃ₗ⁅B⁆ ↥I.lieSubalgebra

The Lie algebra of the quotient Hopf algebra is canonically Lie-equivalent to its image in the ambient tangent Lie algebra.

Equations

• I.quotientLieEquiv = I.quotientLieHom.equivRangeOfInjective ⋯

@[simp]

theorem TauCeti.HopfIdeal.quotientLieEquiv_apply_coe {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (d : Derivation R (H ⧸ I.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ I.toIdeal) B)) : ↑(I.quotientLieEquiv d) = I.quotientLieHom d

The canonical Lie equivalence sends a quotient derivation to its precomposition with the quotient map.

@[simp]

theorem TauCeti.HopfIdeal.quotientLieEquiv_symm_apply_mk {R : Type u} {H : Type v} {B : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommRing B] [Algebra R B] (I : HopfIdeal R H) (d : ↥I.lieSubalgebra) (x : H) : (I.quotientLieEquiv.symm d) ((Ideal.Quotient.mk I.toIdeal) x) = ↑d x

The inverse of the canonical Lie equivalence descends an ambient derivation by evaluating on representatives of the quotient.