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.

Since the correction only rescales one row, it keeps every entry that vanishes in the original lift; in particular, upper-triangular determinant-one matrices lift to upper-triangular ones.

Main declarations

• Matrix.SpecialLinearGroup.exists_map_eq_of_map_eq_of_isNilpotent: a lift of a determinant-one matrix corrects to a determinant-one lift with at least the same vanishing entries.
• Matrix.SpecialLinearGroup.map_quotient_mk_surjective_of_isNilpotent: entrywise reduction modulo a nilpotent ideal is surjective on special-linear groups.
• Matrix.SpecialLinearGroup.exists_isUpperTriangular_map_eq_of_isNilpotent: the same holds for upper-triangular determinant-one matrices.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 2.

theorem Matrix.SpecialLinearGroup.exists_map_eq_of_map_eq_of_isNilpotent {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (I : Ideal R) (hI : IsNilpotent I) (A : SpecialLinearGroup n (R ⧸ I)) (M : Matrix n n R) (hM : M.map ⇑(Ideal.Quotient.mk I) = ↑A) : ∃ (N : SpecialLinearGroup n R), (map (Ideal.Quotient.mk I)) N = A ∧ ∀ (i j : n), M i j = 0 → ↑N i j = 0

A matrix lifting a determinant-one matrix modulo a nilpotent ideal can be corrected to a determinant-one lift that vanishes wherever the original lift does: its determinant is a unit, and scaling one row by the inverse determinant changes neither its image nor its zero entries.

The statement includes the empty index type, where both special-linear groups are trivial.

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) : Function.Surjective ⇑(map (Ideal.Quotient.mk 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.

theorem Matrix.SpecialLinearGroup.exists_isUpperTriangular_map_eq_of_isNilpotent {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] [LinearOrder n] (I : Ideal R) (hI : IsNilpotent I) (A : SpecialLinearGroup n (R ⧸ I)) (hA : (↑A).IsUpperTriangular) : ∃ (N : SpecialLinearGroup n R), (↑N).IsUpperTriangular ∧ (map (Ideal.Quotient.mk I)) N = A

Every upper-triangular determinant-one matrix modulo a nilpotent ideal lifts to an upper-triangular determinant-one matrix.