The Lie algebra of the upper-triangular subgroup of SLₙ

The differential of the upper-triangular subgroup inclusion identifies its tangent Lie algebra with the upper-triangular trace-zero matrices. This holds over every commutative base ring and every coefficient algebra, including in characteristics dividing n.

Over a nontrivial coefficient ring, the normalized matrix unit at a root of the diagonal root datum of SL_{r+1} lies in this Lie algebra exactly when the root is positive for the consecutive-root base. Thus the chosen upper-triangular Borel selects the existing positive system, and contains the matrix units at its simple roots. This containment supplies the Lie-algebra condition on the normalized simple-root vectors in a standard pinning.

The matrix Lie algebra reuses TauCeti.upperTriangular; the tangent equivalence restricts SpecialLinear.tangentLieEquivSl along HopfIdeal.quotientLieEquiv.

References

• J. S. Milne, Algebraic Groups (2017), §10.a and §21, Example 21.2.
• B. Conrad, Reductive Group Schemes, §5.1.

def TauCeti.SpecialLinear.UpperTriangular.matrixLieSubalgebra (n : ℕ) (B : Type w) [CommRing B] : LieSubalgebra B ↥(LieAlgebra.SpecialLinear.sl (Fin n) B)

The upper-triangular trace-zero matrices, as a Lie subalgebra of slₙ.

Equations

• TauCeti.SpecialLinear.UpperTriangular.matrixLieSubalgebra n B = LieSubalgebra.comap (LieAlgebra.SpecialLinear.sl (Fin n) B).incl (TauCeti.upperTriangular B (Fin n))

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.mem_matrixLieSubalgebra_iff (n : ℕ) (B : Type w) [CommRing B] (X : ↥(LieAlgebra.SpecialLinear.sl (Fin n) B)) : X ∈ matrixLieSubalgebra n B ↔ ∀ (i j : Fin n), j < i → ↑X i j = 0

Membership in the matrix Lie algebra of the upper-triangular subgroup is vanishing below the diagonal. Trace zero is already part of the ambient special linear Lie algebra.

theorem TauCeti.SpecialLinear.UpperTriangular.mem_lieSubalgebra_definingHopfIdeal_iff (n : ℕ) {B : Type w} [CommRing B] {R : Type u} [CommRing R] [Algebra R B] (d : Derivation R (↑(SpecialLinear.coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(SpecialLinear.coordinateHopfAlgebra R n)) B)) : d ∈ (definingHopfIdeal R n).lieSubalgebra ↔ ∀ (i j : Fin n), j < i → ↑((tangentMatrix n) d) i j = 0

A tangent vector to SLₙ belongs to the Lie algebra of the upper-triangular closed subgroup exactly when its tangent matrix vanishes below the diagonal.

Use this for explicit rewriting: HopfIdeal.mem_lieSubalgebra_iff already determines the simp normal form of membership.

theorem TauCeti.SpecialLinear.UpperTriangular.map_lieSubalgebra_definingHopfIdeal (n : ℕ) {B : Type w} [CommRing B] {R : Type u} [CommRing R] [Algebra R B] : LieSubalgebra.map (tangentLieEquivSl n).toLieHom (definingHopfIdeal R n).lieSubalgebra = matrixLieSubalgebra n B

The special-linear tangent equivalence carries the Lie algebra of the upper-triangular subgroup onto the upper-triangular trace-zero matrices.

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

The tangent Lie algebra of the upper-triangular subgroup of SLₙ is the Lie algebra of upper-triangular trace-zero matrices over the coefficient algebra.

Equations

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

@[simp]

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

The tangent equivalence is compatible with the differential of the inclusion into SLₙ.

@[simp]

theorem TauCeti.SpecialLinear.UpperTriangular.tangentMatrix_quotientLieHom_tangentLieEquiv_symm (n : ℕ) {B : Type w} [CommRing B] {R : Type u} [CommRing R] [Algebra R B] (X : ↥(matrixLieSubalgebra n B)) : (tangentMatrix n) ((definingHopfIdeal R n).quotientLieHom ((tangentLieEquiv n).symm X)) = ↑X

Descending an upper-triangular trace-zero matrix and then differentiating its inclusion recovers that matrix.

theorem TauCeti.SpecialLinear.UpperTriangular.single_mem_matrixLieSubalgebra (n : ℕ) {B : Type w} [CommRing B] (i j : Fin n) (hij : i < j) (c : B) : (LieAlgebra.SpecialLinear.single i j ⋯) c ∈ matrixLieSubalgebra n B

An off-diagonal matrix unit lies in the upper-triangular special linear Lie algebra when its row precedes its column, for every coefficient, including over the zero ring.

theorem TauCeti.SpecialLinear.UpperTriangular.single_mem_matrixLieSubalgebra_iff (n : ℕ) {B : Type w} [CommRing B] (i j : Fin n) (hij : i ≠ j) {c : B} (hc : c ≠ 0) : (LieAlgebra.SpecialLinear.single i j hij) c ∈ matrixLieSubalgebra n B ↔ i < j

A nonzero off-diagonal matrix unit lies in the upper-triangular special linear Lie algebra exactly when its row precedes its column.

theorem TauCeti.SpecialLinear.UpperTriangular.single_castSucc_succ_mem_matrixLieSubalgebra {B : Type w} [CommRing B] (r : ℕ) (i : Fin r) : (LieAlgebra.SpecialLinear.single i.castSucc i.succ ⋯) 1 ∈ matrixLieSubalgebra (r + 1) B

The normalized simple-root vectors lie in the Lie algebra of the chosen upper-triangular Borel. This containment holds even over the zero ring.

theorem TauCeti.SpecialLinear.UpperTriangular.tangentLieEquivSl_symm_single_mem_lieSubalgebra_iff_isPos {B : Type w} [CommRing B] {R : Type u} [CommRing R] [Algebra R B] [Nontrivial B] (r : ℕ) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (tangentLieEquivSl (r + 1)).symm ((LieAlgebra.SpecialLinear.single (↑p).1 (↑p).2 ⋯) 1) ∈ (definingHopfIdeal R (r + 1)).lieSubalgebra ↔ (diagonalRootBase r).IsPos p

The normalized root tangent vector to SL_{r+1} lies in the Lie algebra of its chosen upper-triangular Borel exactly when the root is positive.

Use this for explicit rewriting: HopfIdeal.mem_lieSubalgebra_iff already determines the simp normal form of membership.