The Lie algebra of the kernel of an affine group morphism

For a morphism f : H ⟶ K of commutative Hopf algebras, the induced morphism of affine group schemes runs from Spec K to Spec H. Its scheme-theoretic kernel has coordinate ring K ⧸ kernelHopfIdeal f, where kernelHopfIdeal f is generated by the image in K of the augmentation ideal of H.

This file proves that the Lie algebra of this kernel is canonically the kernel of the differential of f. The key algebraic step says that a counit-valued derivation of K vanishes on the ideal generated by the image of the augmentation ideal exactly when its precomposition with f is zero. Combining this with the closed-subgroup tangent equivalence gives the expected Lie equivalence and the corresponding dimension identity.

This is the coordinate-Hopf-algebra form of the kernel part of the ReductiveGroups roadmap's Layer 2 target on dimension tools through Lie(G).

Main declarations

• TauCeti.CommHopfAlgCat.derivationComp_eq_zero_iff_vanishes_kernelHopfIdeal: the differential vanishes exactly on derivations annihilating the kernel Hopf ideal.
• TauCeti.CommHopfAlgCat.lieSubalgebra_kernelHopfIdeal: the closed-subgroup Lie algebra cut out by the kernel Hopf ideal is the kernel of the differential.
• TauCeti.CommHopfAlgCat.kernelLieEquiv: the Lie algebra of the scheme-theoretic kernel is canonically Lie-equivalent to the kernel of the differential.
• TauCeti.CommHopfAlgCat.finrank_kernelLie: the resulting equality of Lie algebra dimensions over a field.

References

J. S. Milne, Algebraic Groups (2017), §10.a, identifies tangent spaces with counit-valued derivations; the kernel calculation is the coordinate form of this functoriality. The coordinate ring of the kernel used here is Milne's Proposition 4.1.

theorem TauCeti.CommHopfAlgCat.derivationComp_eq_zero_iff_vanishes_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {B : Type w} [CommRing B] [Algebra R B] (f : H ⟶ K) (d : Derivation R (↑K) (Bialgebra.CounitAlgebra R (↑K) B)) : (derivationComp (CommHopfAlgCat.Hom.hom f)) d = 0 ↔ ∀ x ∈ (kernelHopfIdeal f).toIdeal, d x = 0

A counit-valued derivation lies in the kernel of the differential exactly when it vanishes on the kernel Hopf ideal.

The forward implication is the nontrivial one: zero precomposition says that the derivation vanishes on the image of the augmentation ideal, hence on the ideal it generates by Derivation.apply_eq_zero_of_mem_span. The reverse implication tests on x - ε(x), whose image belongs to the kernel Hopf ideal and differs from the image of x by a scalar, on which every derivation vanishes.

theorem TauCeti.CommHopfAlgCat.lieSubalgebra_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {B : Type w} [CommRing B] [Algebra R B] (f : H ⟶ K) : (kernelHopfIdeal f).lieSubalgebra = LieIdeal.toLieSubalgebra B (Derivation R (↑K) (Bialgebra.CounitAlgebra R (↑K) B)) (derivationCompLieHom (CommHopfAlgCat.Hom.hom f)).ker

The Lie subalgebra of Lie(Spec K) cut out by the kernel Hopf ideal is exactly the kernel of the differential Lie(Spec K) → Lie(Spec H).

noncomputable def TauCeti.CommHopfAlgCat.kernelLieEquiv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {B : Type w} [CommRing B] [Algebra R B] (f : H ⟶ K) : Derivation R (↑K ⧸ (kernelHopfIdeal f).toIdeal) (Bialgebra.CounitAlgebra R (↑K ⧸ (kernelHopfIdeal f).toIdeal) B) ≃ₗ⁅B⁆ ↥(derivationCompLieHom (CommHopfAlgCat.Hom.hom f)).ker

The Lie algebra of the scheme-theoretic kernel of Spec K ⟶ Spec H is canonically Lie-equivalent to the kernel of its differential.

The source is the derivation presentation of the Lie algebra of Spec (K ⧸ kernelHopfIdeal f). The map is induced by precomposition with the quotient map, and its range is identified with the differential kernel by lieSubalgebra_kernelHopfIdeal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelLieEquiv_apply_coe {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {B : Type w} [CommRing B] [Algebra R B] (f : H ⟶ K) (d : Derivation R (↑K ⧸ (kernelHopfIdeal f).toIdeal) (Bialgebra.CounitAlgebra R (↑K ⧸ (kernelHopfIdeal f).toIdeal) B)) : ↑((kernelLieEquiv f) d) = (kernelHopfIdeal f).quotientLieHom d

Under kernelLieEquiv, a derivation of the kernel coordinate ring is included into the ambient Lie algebra by precomposition with the quotient map.

@[simp]

theorem TauCeti.CommHopfAlgCat.derivationCompLieHom_comp_quotientLieHom_kernelHopfIdeal_eq_zero {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {B : Type w} [CommRing B] [Algebra R B] (f : H ⟶ K) : (derivationCompLieHom (CommHopfAlgCat.Hom.hom f)).comp (kernelHopfIdeal f).quotientLieHom = 0

The differential of a group morphism vanishes after the inclusion of its scheme-theoretic kernel.

theorem TauCeti.CommHopfAlgCat.finrank_kernelLie {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : Module.finrank k (Derivation k (↑K ⧸ (kernelHopfIdeal f).toIdeal) (Bialgebra.CounitAlgebra k (↑K ⧸ (kernelHopfIdeal f).toIdeal) k)) = Module.finrank k ↥(derivationCompLieHom (CommHopfAlgCat.Hom.hom f)).ker

The Lie algebra dimension of a scheme-theoretic kernel is the dimension of the kernel of the differential.