Differential of a special-linear root subgroup

The differential at the identity of the represented morphism xᵢⱼ : 𝔾ₐ → SLₙ is the map c ↦ c Eᵢⱼ into the trace-zero matrices. In particular, the unit tangent vector gives the normalized root vector used in the standard type-A pinning.

The calculation uses the coordinate factorization through SLₙ → GLₙ and GeneralLinear.tangentMatrix_derivationComp_rootSubgroup. It holds over every commutative base ring and every commutative coefficient algebra, without smoothness or characteristic assumptions.

References

• J. S. Milne, Algebraic Groups (2017), §21.

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_derivationComp_rootSubgroup {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} (hij : i ≠ j) (d : Derivation R (↑(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (↑(AdditiveGroup.coordinateHopfAlgebra R)) B)) : (tangentMatrix n) ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) d) = (LieAlgebra.SpecialLinear.single i j hij) (AdditiveGroup.gaTangentLinearEquiv d)

In the special linear Lie algebra, the differential of xᵢⱼ : 𝔾ₐ → SLₙ is Mathlib's linear map c ↦ c Eᵢⱼ of off-diagonal single-entry matrices.

theorem TauCeti.SpecialLinear.derivationComp_rootSubgroup_injective {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Function.Injective ⇑(derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij)))

The root-subgroup differential is injective, even over nonreduced coefficient rings.

theorem TauCeti.SpecialLinear.mem_range_derivationCompLieHom_rootSubgroup_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} (hij : i ≠ j) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : d ∈ (derivationCompLieHom (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))).range ↔ ∃ (c : B), (tangentMatrix n) d = (LieAlgebra.SpecialLinear.single i j hij) c

A tangent vector belongs to the image of the root-subgroup differential exactly when its trace-zero matrix is a scalar multiple of the corresponding matrix unit.

theorem TauCeti.SpecialLinear.range_derivationCompLieHom_rootSubgroup_eq_span {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (derivationCompLieHom (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))).range.toSubmodule = B ∙ (derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) (AdditiveGroup.gaTangentLinearEquiv.symm 1)

The image of the root-subgroup differential is the line spanned by the image of the unit tangent vector. This characterizes the normalized root vector inside Lie(SLₙ).

theorem TauCeti.SpecialLinear.derivationComp_rootSubgroup_unit_ne_zero {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} [Nontrivial B] (hij : i ≠ j) : (derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) (AdditiveGroup.gaTangentLinearEquiv.symm 1) ≠ 0

The normalized root vector is nonzero over any nontrivial coefficient algebra.