Equivariance of the differential for the adjoint action

A morphism of affine group schemes intertwines conjugation. Differentiating at the identity says that its differential intertwines the corresponding adjoint actions. In coordinate rings, a bialgebra morphism φ : A' →ₐc[R] A acts on both points and tangent derivations by precomposition, and the compatibility is

dφ (Ad(g)(d)) = Ad(g ∘ φ)(dφ(d)).

This file proves that identity directly from functoriality of convolution and packages it as an intertwining identity for the adjoint representations. It synchronizes the differential and adjoint-action parts of Layer 2 of the ReductiveGroups roadmap; in particular, it is the functoriality needed when tangent Lie algebras of closed subgroups are used inside an ambient group.

Main declarations

• TauCeti.derivationComp_adDerivation: the differential intertwines the adjoint action.

References

• J. S. Milne, Algebraic Groups (2017), §14.

@[simp]

theorem TauCeti.derivationComp_adDerivation {R : Type u} {A : Type v} {A' : Type w} {B : Type x} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] (φ : A' →ₐc[R] A) (g : WithConv (A →ₐ[R] Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) : (derivationComp φ) (Derivation.adDerivation B g d) = Derivation.adDerivation B ((AlgHom.mapDomain φ) g) ((derivationComp φ) d)

The differential of a Hopf-algebra morphism intertwines the adjoint actions.

Contravariantly, φ : A' →ₐc[R] A represents a morphism Spec A → Spec A'. Precomposing both a point and a tangent derivation with φ commutes with convolution conjugation.