Solvability of the upper triangular tangent Lie algebra

The Lie algebra of the upper triangular general linear group is solvable over every commutative coefficient ring. The tangent-image criterion identifies its image inside the ambient general-linear Lie algebra with upper triangular matrices, so root-space containment can be tested in matrix coordinates. The weight-parabolic tangent equivalence also identifies the subgroup's own Lie algebra with these matrices. This lets solvability pass to the Lie algebra of a group embedded in the upper triangular group, as in the Lie--Kolchin theorem.

The identification uses GeneralLinear.weightParabolicTangentLieEquiv with the standard strictly decreasing weights, and solvability is TauCeti.isSolvable_upperTriangular.

theorem TauCeti.GeneralLinear.UpperTriangular.mem_lieSubalgebra_definingHopfIdeal_iff {R : Type u} [CommRing R] {B : Type v} [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 ↔ (tangentMatrix n) d ∈ upperTriangular B (Fin n)

A tangent vector lies in the upper-triangular subgroup exactly when its matrix is upper triangular, over any coefficient algebra.

instance TauCeti.GeneralLinear.UpperTriangular.isSolvable_tangentLieAlgebra {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (n : ℕ) : LieAlgebra.IsSolvable (Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B))

The coefficient-valued tangent Lie algebra of the upper triangular general linear group is solvable over every commutative coefficient ring.