Invariant derivations and nilpotent functions

Let H be a commutative bialgebra over R, the coordinate ring of an affine monoid. A tangent vector at the identity is a counit-valued derivation d. It extends to the derivation

D h = ∑ h₍₁₎ d(h₍₂₎)

of the whole coordinate ring: the left-invariant vector field with value d at the identity. As a linear map it is the action of d in the differentiated regular representation (TauCeti.Comodule.differential); the point here is that this action satisfies the Leibniz rule. It satisfies ε ∘ D = d and the invariance identity Δ ∘ D = (id ⊗ D) ∘ Δ.

Over a domain of characteristic zero, every derivation of H sends nilpotent functions into the prime ideal ker ε. Applied to the invariant extension of d, this shows that every tangent vector at the identity vanishes on the nilradical. Over a field of characteristic zero it follows that the nilradical lies in the square of the augmentation ideal: nilpotent functions vanish to second order at the identity, so the closed subscheme they cut out has the same tangent space as the ambient group. This is the infinitesimal input to Cartier's theorem.

Main declarations

• TauCeti.Bialgebra.leftInvariantDerivation: the left-invariant derivation extending a tangent vector at the identity.
• TauCeti.Bialgebra.counit_leftInvariantDerivation: its value at the identity is the tangent vector.
• TauCeti.Bialgebra.comul_leftInvariantDerivation: its invariance under left translations.
• TauCeti.Bialgebra.eq_leftInvariantDerivation: a left-invariant derivation is determined by its value at the identity.
• Derivation.apply_eq_zero_of_isNilpotent: in characteristic zero, tangent vectors at the identity vanish on nilpotent functions.
• TauCeti.Bialgebra.nilradical_le_augmentationIdeal_sq: over a field of characteristic zero, the nilradical lies in the square of the augmentation ideal.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 3 (Cartier's theorem) and Chapter 10.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapters 11 and 12.

noncomputable def TauCeti.Bialgebra.leftInvariantDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] : Derivation R H (CounitAlgebra R H R) →ₗ⁅R⁆ Derivation R H H

The left-invariant derivation extending a tangent vector at the identity: h ↦ ∑ h₍₁₎ d(h₍₂₎). This Lie algebra homomorphism is the differentiated regular representation with its values regarded as derivations.

Equations

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

theorem TauCeti.Bialgebra.toLinearMap_leftInvariantDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] (d : Derivation R H (CounitAlgebra R H R)) : ↑(leftInvariantDerivation d) = Comodule.differential d

The left-invariant derivation is the differentiated regular representation.

theorem TauCeti.Bialgebra.leftInvariantDerivation_apply {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] (d : Derivation R H (CounitAlgebra R H R)) (h : H) : (leftInvariantDerivation d) h = ((CounitAlgebra.algEquivSelf R H R).toLinearMap ∘ₗ ↑d).tensorComponent (CoalgebraStruct.comul h)

The left-invariant derivation contracts the comultiplication against the tangent vector.

@[simp]

theorem TauCeti.Bialgebra.counit_leftInvariantDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] (d : Derivation R H (CounitAlgebra R H R)) (h : H) : CoalgebraStruct.counit ((leftInvariantDerivation d) h) = (CounitAlgebra.algEquivSelf R H R) (d h)

The left-invariant derivation has value d at the identity: ε ∘ D = d.

@[simp]

theorem TauCeti.Bialgebra.comul_leftInvariantDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] (d : Derivation R H (CounitAlgebra R H R)) (h : H) : CoalgebraStruct.comul ((leftInvariantDerivation d) h) = (LinearMap.lTensor H ↑(leftInvariantDerivation d)) (CoalgebraStruct.comul h)

The left-invariant derivation commutes with left translations: Δ ∘ D = (id ⊗ D) ∘ Δ.

theorem TauCeti.Bialgebra.eq_leftInvariantDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [Bialgebra R H] (D : Derivation R H H) (d : Derivation R H (CounitAlgebra R H R)) (hε : ∀ (h : H), CoalgebraStruct.counit (D h) = (CounitAlgebra.algEquivSelf R H R) (d h)) (hΔ : ∀ (h : H), CoalgebraStruct.comul (D h) = (LinearMap.lTensor H ↑D) (CoalgebraStruct.comul h)) : D = leftInvariantDerivation d

A left-invariant derivation with value d at the identity is the left-invariant extension of d.

theorem Derivation.apply_eq_zero_of_isNilpotent {R : Type u_1} {H : Type u_2} [CommRing R] [IsDomain R] [CharZero R] [CommRing H] [Bialgebra R H] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) {x : H} (hx : IsNilpotent x) : d x = 0

In characteristic zero, a tangent vector at the identity vanishes on nilpotent functions. The base ring may be any domain of characteristic zero.

theorem TauCeti.Bialgebra.nilradical_le_augmentationIdeal_sq {k : Type u_1} {H : Type u_2} [Field k] [CharZero k] [CommRing H] [Bialgebra k H] : nilradical H ≤ AugmentationIdeal k H ^ 2

Over a field of characteristic zero, nilpotent functions vanish to second order at the identity: the nilradical lies in the square of the augmentation ideal. Equivalently, the reduced closed subscheme has the same tangent space at the identity.