Lifting special-linear matrices #
A special-linear matrix lifts across a quotient by a nilpotent ideal. Lift its entries arbitrarily; its determinant is then a unit because it is one modulo the ideal. Scaling one row by the inverse determinant corrects the lift without changing its image.
Main declaration #
Matrix.SpecialLinearGroup.map_quotient_mk_surjective_of_isNilpotent: entrywise reduction modulo a nilpotent ideal is surjective on special-linear groups.
References #
- J. S. Milne, Algebraic Groups (2017), Chapter 2.
theorem
Matrix.SpecialLinearGroup.map_quotient_mk_surjective_of_isNilpotent
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{R : Type u}
[CommRing R]
(I : Ideal R)
(hI : IsNilpotent I)
:
Every determinant-one matrix modulo a nilpotent ideal lifts to a determinant-one matrix.
The statement includes the empty index type, where both special-linear groups are trivial.