Tangent vectors and the antipode #
A counit-valued derivation d of a commutative Hopf algebra is a tangent vector at the identity
of the corresponding affine group. Inversion on the group is represented by the antipode S, and
its differential at the identity is negation: d ∘ S = -d.
Consequently a tangent vector that annihilates a set of coordinate functions also annihilates their antipodes. This is what lets the Lie algebra of a closed subgroup be computed from an antipode-stable generating set of its ideal, such as the matrix coefficients and their antipodes cutting out the stabilizer of a subspace of a representation.
Main declaration #
Derivation.apply_antipode: a counit-valued derivation negates under the antipode.
References #
- J. S. Milne, Algebraic Groups (2017), §10.a.
@[simp]
theorem
Derivation.apply_antipode
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommRing R]
[CommRing A]
[HopfAlgebra R A]
[CommRing B]
[Algebra R B]
(d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))
(a : A)
:
A tangent vector at the identity negates under the antipode: the differential of inversion
at the identity is -1.