Lifting upper-triangular invertible matrices

Upper-triangular invertible matrices lift along surjective ring homomorphisms that reflect units. This is the diagonal-block lifting step for flag stabilizers: lift only the entries on and above the diagonal, then reflect invertibility of the determinant along the ring homomorphism.

The entrywise construction follows Matrix.SpecialLinearGroup.exists_isUpperTriangular_map_eq in TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Lift.

theorem TauCeti.UpperTriangularGroup.map_surjective {n : Type u_1} [Fintype n] [LinearOrder n] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] (φ : R →+* S) [IsLocalHom φ] (hφ : Function.Surjective ⇑φ) : Function.Surjective ⇑(map φ)

A surjective ring homomorphism that reflects units induces a surjection on the upper-triangular general linear subgroup, including for an empty index type.