The infinitesimal adjoint action #
The differential of the adjoint representation is the adjoint representation of the Lie
algebra. Concretely, the dual-number point associated to a tangent vector d acts on a
constant tangent vector e by e + ε[d,e]. This identifies the convolution commutator
with the infinitesimal change of the group adjoint action, over any commutative base ring.
References #
- J. S. Milne, Algebraic Groups (2017), §10.d, 10.18–10.23.
@[simp]
theorem
Derivation.adDerivation_dualNumber_apply
{R : Type u_1}
{H : Type u_2}
{B : Type u_3}
[CommRing R]
[CommRing H]
[HopfAlgebra R H]
[CommRing B]
[Algebra R B]
(d e : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H B))
(a : H)
:
(TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H (DualNumber (TauCeti.Bialgebra.CounitAlgebra R H B)))
((adDerivation (DualNumber (TauCeti.Bialgebra.CounitAlgebra R H B))
((TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv R H (DualNumber (TauCeti.Bialgebra.CounitAlgebra R H B))).symm
↑((TauCeti.derivationMulEquivTangentKer R H B) (Multiplicative.ofAdd d)))
((mapValue
((TrivSqZeroExt.inlAlgHom R (TauCeti.Bialgebra.CounitAlgebra R H B)
(TauCeti.Bialgebra.CounitAlgebra R H B)).comp
↑(TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H B).symm))
e))
a) = TrivSqZeroExt.inl (e a) + TrivSqZeroExt.inr (⁅d, e⁆ a)
The adjoint action of the dual-number point of d on the constant lift of e
is e + ε[d,e]. Thus the differential of the group adjoint action is the Lie bracket.