Differentiating the adjoint comodule

The differentiated action of the adjoint comodule is the Lie bracket on the dual of the augmentation cotangent space. This connects the dual-number description of the infinitesimal adjoint action with the differentiated representation used to study invariant subspaces. Restricting the adjoint comodule to a closed subgroup, the differentiated action of a tangent vector of the subgroup is the bracket with its image under the differential of the inclusion (TauCeti.differential_corestrict_adjointComodule).

References

• J. S. Milne, Algebraic Groups (2017), §10.d, 10.18–10.23.

@[simp]

theorem Derivation.differential_adjointComodule {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) (x : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) : (TauCeti.Comodule.differential d) x = ⁅cotangentDualLieEquiv.symm d, x⁆

The differential of the adjoint comodule is the adjoint action of the tangent Lie algebra, expressed in the cotangent-dual model.

theorem TauCeti.differential_corestrict_adjointComodule {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (Bialgebra.CotangentSpace R H)] [Module.Projective R (Bialgebra.CotangentSpace R H)] (J : HopfIdeal R H) (d : Derivation R (H ⧸ J.toIdeal) (Bialgebra.CounitAlgebra R (H ⧸ J.toIdeal) R)) (y : Module.Dual R (Bialgebra.CotangentSpace R H)) : (Comodule.differential d) y = ⁅Derivation.cotangentDualLieEquiv.symm (J.quotientLieHom d), y⁆

The restricted adjoint representation differentiates to the bracket. A tangent vector d of the closed subgroup cut out by J acts on 𝔤 by the bracket with its image in 𝔤 under the differential of the inclusion.