Integral points of the type A full-weight carrier

This file identifies the integral matrix points of the full-weight type A_r carrier with the image of SL_{r+1}(ℤ). It applies the ring-general carrier generation theorem to the existing generation of the integral special linear group by transvections.

Main results

• TauCeti.SlStd.points_int_eq_range_toGL: the integral carrier points are exactly the image of SL_{r+1}(ℤ) in GL_{r+1}(ℤ).
• TauCeti.SlStd.mem_points_int_iff_det_eq_one: integral carrier-point membership is equivalent to having determinant one.

This advances Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md: it records the integral-points consequence of the ring-general generation statement for the explicit full-weight type A carrier.

theorem TauCeti.SlStd.points_int_eq_range_toGL (r : ℕ) : points r ℤ = Matrix.SpecialLinearGroup.toGL.range

Over the integers, the matrix points of the full-weight type A_r carrier are exactly the range of the canonical inclusion of SL_{r+1} into GL_{r+1}.

theorem TauCeti.SlStd.mem_points_int_iff_det_eq_one (r : ℕ) (g : GL (Fin (r + 1)) ℤ) : g ∈ points r ℤ ↔ Matrix.GeneralLinearGroup.det g = 1

Over the integers, a general linear matrix is a point of the full-weight type A_r carrier if and only if its determinant is one.