The Lie algebra of a representation kernel

For a finite free representation of an affine group, the differential of its coordinate morphism is the differentiated comodule action. Consequently the Lie algebra of its scheme-theoretic kernel consists exactly of the tangent vectors acting by zero.

The statements work over an arbitrary commutative base ring. A basis describes the coordinate morphism to the general linear group; the vanishing criterion is intrinsic to the comodule.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 4 and 10.

The proof combines Derivation.apply_matrixCoefficient, the tangent-matrix equivalence for the general linear group, and TauCeti.CommHopfAlgCat.lieSubalgebra_kernelHopfIdeal.

theorem Derivation.tangentMatrix_comp_coordinateBialgHom {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [TauCeti.Comodule R H M] {n : ℕ} (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) (b : Module.Basis (Fin n) R M) : (TauCeti.GeneralLinear.tangentMatrix n) ((TauCeti.derivationComp (TauCeti.Comodule.coordinateBialgHom b)) d) = (LinearMap.toMatrix b b) (TauCeti.Comodule.differential d)

In a finite basis, differentiating the coordinate morphism of a representation gives the matrix of the differentiated comodule action.

@[simp]

theorem Derivation.mem_lieSubalgebra_kernel_coordinateBialgHom_iff {R H : Type u} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [TauCeti.Comodule R H M] {n : ℕ} (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) (b : Module.Basis (Fin n) R M) : d ∈ (TauCeti.CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.ofHom (TauCeti.Comodule.coordinateBialgHom b))).lieSubalgebra ↔ TauCeti.Comodule.differential d = 0

A tangent vector lies in the Lie algebra of a representation's scheme-theoretic kernel exactly when its differentiated action is zero.