The adjoint action on the tangent space

The points of a Hopf algebra act on the counit-valued derivations — the tangent vectors at the identity — by convolution conjugation: Ad g d = g ⋆ d ⋆ g⁻¹ in the convolution semiring of linear maps, the differential of the conjugation c_g x = g ⋆ x ⋆ g⁻¹ of the group of points. Conjugation is a semiring automorphism of the whole convolution semiring; this file shows it restricts to the derivations, and packages the restriction, one coefficient algebra B at a time, as a representation of the B-points on the B-valued tangent vectors (adRepresentation). For commutative A these are the coefficientwise layers of the adjoint action of the corresponding affine group scheme on its Lie functor; their compatibility as B varies (postcomposition naturality) is later infrastructure, not packaged here.

Closure is composition-level, by the exterior-product calculus of Tangent.Basic: an algebra-map point satisfies g ∘ mul = g ⊠ g, a derivation satisfies d ∘ mul = e ⊠ d + d ⊠ e for the convolution unit e, and the conjugates collapse by g ⋆ e ⋆ g⁻¹ = e, leaving the Leibniz form for g ⋆ d ⋆ g⁻¹. No antipode computation appears; inverses come from the group of points.

Main declarations

• Derivation.adDerivation: the conjugate of a tangent vector by a point.
• Derivation.toConv_coe_adDerivation: that conjugate as the convolution product g ⋆ d ⋆ g⁻¹, the form the algebraic manipulations use.
• Derivation.snd_conjugate_tangentPoint: conjugation on dual-number tangent points induces the adjoint action on their infinitesimal coefficients.
• Derivation.adRepresentation: the adjoint action, as a representation of the convolution group of points on the tangent space.

Compatibility of the action with the Lie bracket needs the Lie structure and so lives in Tangent.Lie.Adjoint.Basic, keeping this module free of it.

The action stays on the Lie functor B ↦ Derivation R A (CounitAlgebra R A B); at each B it is a genuine representation. Identifying the functor's value at B with B ⊗ Lie(G)(R) — the classical fixed-module G → GL(Lie G) — needs a finite-projectivity hypothesis on the conormal module and is not attempted here.

References

• J. S. Milne, Algebraic Groups (2017), §14 (the adjoint representation).
• J. C. Jantzen, Representations of Algebraic Groups, I.7.18.

noncomputable def Derivation.adDerivation {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)

The conjugate of a tangent vector by a point: the adjoint action Ad g d = g ⋆ d ⋆ g⁻¹, the differential of conjugation on the group of points.

Equations

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

@[simp]

theorem Derivation.coe_adDerivation_linearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : ↑(adDerivation B g d) = (WithConv.toConv g.ofConv.toLinearMap * WithConv.toConv ↑d * WithConv.toConv g⁻¹.ofConv.toLinearMap).ofConv

The adjoint action is the convolution conjugate, on underlying linear maps.

@[simp]

theorem Derivation.adDerivation_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (a : A) : (adDerivation B g d) a = (WithConv.toConv g.ofConv.toLinearMap * WithConv.toConv ↑d * WithConv.toConv g⁻¹.ofConv.toLinearMap).ofConv a

The adjoint action, valuewise: the conjugate evaluated at an element of the bialgebra.

theorem Derivation.toConv_coe_adDerivation {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : WithConv.toConv ↑(adDerivation B g d) = WithConv.toConv g.ofConv.toLinearMap * WithConv.toConv ↑d * WithConv.toConv g⁻¹.ofConv.toLinearMap

The conjugate of a tangent vector, in convolution form: Ad g d is the product g ⋆ d ⋆ g⁻¹ in the convolution algebra of linear maps. This is the form in which the adjoint action is manipulated algebraically, and the bracket compatibility in Tangent.Lie.Adjoint.Basic is proved from it.

noncomputable def Derivation.adRepresentation {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : Representation B (WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))

The adjoint action of the group of points on the tangent space, as a B-linear representation: conjugation is a semiring automorphism of the convolution semiring, it restricts to the derivations, and scalars of the coefficient algebra pass through the conjugation because B is commutative.

Equations

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

@[simp]

theorem Derivation.adRepresentation_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : ((adRepresentation B) g) d = adDerivation B g d

@[simp]

theorem Derivation.snd_conjugate_tangentPoint {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (a : A) : (((TauCeti.AlgHom.mapValue (TrivSqZeroExt.inlAlgHom R (TauCeti.Bialgebra.CounitAlgebra R A B) (TauCeti.Bialgebra.CounitAlgebra R A B))) g * ↑((TauCeti.derivationMulEquivTangentKer R A B) (Multiplicative.ofAdd d)) * ((TauCeti.AlgHom.mapValue (TrivSqZeroExt.inlAlgHom R (TauCeti.Bialgebra.CounitAlgebra R A B) (TauCeti.Bialgebra.CounitAlgebra R A B))) g)⁻¹).ofConv a).snd = (adDerivation B g d) a

Conjugating a tangent point by a constant dual-number point induces the adjoint action on its infinitesimal coefficient.