The tangent Lie algebra of the special linear group

The tangent Lie algebra of SLₙ is the special linear Lie algebra of trace-zero matrices. The closed immersion SLₙ → GLₙ identifies a tangent derivation of the determinant-one quotient with an ambient derivation which vanishes on the ideal generated by det - 1. Under the existing tangent-matrix equivalence for GLₙ, this condition is exactly vanishing of the matrix trace.

The key calculation is valid over any commutative coefficient algebra. A tangent point of GLₙ over the dual numbers has matrix 1 + εX; the first-order part of its determinant is trace X. Consequently, the resulting equivalence is linear over the coefficient algebra and preserves the convolution and matrix-commutator Lie brackets.

This gives the standard SLₙ worked example in the ReductiveGroups roadmap's Layer 2 target on the tangent space at the identity / Lie(G) and the Lie algebra of a closed subgroup.

Main declarations

• TauCeti.SpecialLinear.mem_lieSubalgebra_definingHopfIdeal_iff: an ambient tangent derivation lies in the determinant-one Lie subalgebra exactly when its tangent matrix has trace zero.
• TauCeti.SpecialLinear.tangentMatrix: a tangent vector to SLₙ, as a trace-zero matrix.
• TauCeti.SpecialLinear.tangentLieEquivSl: the tangent Lie algebra of SLₙ is its classical special linear Lie algebra.

References

• J. S. Milne, Algebraic Groups (2017), §10.
• The target Lie algebra is Mathlib's LieAlgebra.SpecialLinear.sl.

Trace-zero matrices from the determinant-one quotient

theorem TauCeti.SpecialLinear.mem_lieSubalgebra_definingHopfIdeal_iff {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(GeneralLinear.coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(GeneralLinear.coordinateHopfAlgebra R n)) B)) : d ∈ (definingHopfIdeal R n).lieSubalgebra ↔ ((GeneralLinear.tangentMatrix n) d).trace = 0

An ambient tangent derivation lies in the Lie algebra cut out by the determinant-one ideal exactly when its tangent matrix has trace zero.

noncomputable def TauCeti.SpecialLinear.tangentMatrix {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) →ₗ[B] ↥(LieAlgebra.SpecialLinear.sl (Fin n) B)

The trace-zero matrix of a tangent vector to SLₙ. It is obtained by including the derivation into the tangent Lie algebra of GLₙ and evaluating on the generic matrix entries.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_apply_coe {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : ↑((tangentMatrix n) d) = (GeneralLinear.tangentMatrix n) ((definingHopfIdeal R n).quotientLieHom d)

The underlying matrix of SpecialLinear.tangentMatrix is the ambient GLₙ tangent matrix after precomposition with the determinant-one quotient.

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_mapValue_coe {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) {C : Type u_1} [CommRing C] [Algebra R C] (φ : B →ₐ[R] C) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : ↑((tangentMatrix n) ((Derivation.mapValue φ) d)) = (↑((tangentMatrix n) d)).map ⇑φ

Changing the coefficient algebra of a tangent vector applies the coefficient map to each entry of its trace-zero matrix.

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_apply {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) (i j : Fin n) : ↑((tangentMatrix n) d) i j = (Bialgebra.CounitAlgebra.algEquivSelf R (↑(coordinateHopfAlgebra R n)) B) (d ((CommHopfAlgCat.Hom.hom (coordinateMap R n)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.coordinateRingMap R n) (MvPolynomial.X (i, j))))))

An entry of the special-linear tangent matrix is the derivation evaluated on the image of the corresponding generic matrix coordinate in the determinant-one quotient.

@[simp]

theorem TauCeti.SpecialLinear.tangentMatrix_lie {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d e : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentMatrix n) ⁅d, e⁆ = ⁅(tangentMatrix n) d, (tangentMatrix n) e⁆

The tangent-matrix map for SLₙ preserves the Lie bracket, carrying convolution commutators to matrix commutators.

noncomputable def TauCeti.SpecialLinear.tangentLieEquivSl {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) ≃ₗ⁅B⁆ ↥(LieAlgebra.SpecialLinear.sl (Fin n) B)

The tangent Lie algebra of SLₙ is the special linear Lie algebra. The equivalence is valid after extension to every commutative R-algebra B.

Equations

• TauCeti.SpecialLinear.tangentLieEquivSl n = LieEquiv.ofBijective (let __src := TauCeti.SpecialLinear.tangentMatrix n; { toLinearMap := __src, map_lie' := ⋯ }) ⋯

@[simp]

theorem TauCeti.SpecialLinear.tangentLieEquivSl_apply {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentLieEquivSl n) d = (tangentMatrix n) d

The tangent Lie equivalence is implemented by SpecialLinear.tangentMatrix.