The adjoint action of the special linear group #
The tangent Lie algebra of SLₙ is the Lie algebra of trace-zero matrices. Its adjoint
action is conjugation by the corresponding determinant-one matrix over every commutative
coefficient algebra, including nonreduced ones. This comparison supports the calculation
of adjoint weights for SLₙ.
Main declarations #
TauCeti.SpecialLinear.tangentMatrix_adDerivation_coe: identifies the adjoint action onLie(SLₙ)with conjugation by its image inGLₙ.
References #
- J. S. Milne, Algebraic Groups (2017), §10.d (the adjoint representation), cf. 10.24.
@[simp]
theorem
TauCeti.SpecialLinear.tangentMatrix_adDerivation_coe
{R : Type u_1}
[CommRing R]
{B : Type u_2}
[CommRing B]
[Algebra R B]
(n : ℕ)
(g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B))
(d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B))
:
↑((tangentMatrix n) (Derivation.adDerivation B g d)) = ↑((counitPointsMulEquiv n) g) * ↑((tangentMatrix n) d) * ↑((counitPointsMulEquiv n) g)⁻¹
The adjoint action of SLₙ on its tangent Lie algebra is conjugation on trace-zero
matrices by the ambient GLₙ point. This holds for every commutative coefficient algebra.