The adjoint action respects the Lie bracket #
Derivation.adDerivation conjugates a tangent vector by a point of the Hopf algebra.
Tangent.Adjoint shows that this is an action by linear automorphisms; this file adds the
one statement that needs the Lie structure of Tangent.Lie.Basic, namely that each Ad g is
an automorphism of the Lie bracket rather than merely of the module.
It is kept out of Tangent.Adjoint so that the non-Lie tangent aggregator does not re-export
the Lie-algebra structure.
Main results #
Derivation.adDerivation_lie:Ad g ⁅d₁, d₂⁆ = ⁅Ad g d₁, Ad g d₂⁆.
@[simp]
theorem
Derivation.adDerivation_lie
{R : Type u_1}
{A : Type u_2}
(B : Type u_3)
[CommSemiring R]
[CommSemiring A]
[HopfAlgebra R A]
[CommRing B]
[Algebra R B]
(g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B))
(d₁ d₂ : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))
:
The adjoint action is by Lie automorphisms. Ad g is conjugation g ⋆ · ⋆ g⁻¹ in the
convolution ring, and conjugation by a unit preserves the commutator, so it respects the
bracket of tangent vectors.