Generation of type A full-weight carrier points

This file proves that every elementary transvection over a commutative ring is a matrix point of the full-weight type A_r carrier. Consequently, whenever elementary transvections generate the special linear group over a ring, the carrier points are exactly the image of that special linear group in the general linear group.

Main results

• TauCeti.SlStd.transvectionUnit_mem_points: every elementary transvection over a commutative ring is a point of the carrier.
• TauCeti.SlStd.points_eq_range_toGL_of_transvection_generation: transvection generation of SL_{r+1}(R) identifies its image with the carrier points over R.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §§3--4.

This advances Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md: it supplies the ring-general generation step used to identify the explicit full-weight type A carrier on field and integral points.

theorem TauCeti.SlStd.transvectionUnit_mem_points (r : ℕ) {A : Type u} [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (c : A) : transvectionUnit hij c ∈ points r A

Every elementary transvection over a commutative ring is a point of the type A_r carrier.

theorem TauCeti.SlStd.points_eq_range_toGL_of_transvection_generation (r : ℕ) {R : Type u} [CommRing R] (hgen : Subgroup.closure (Set.range Matrix.TransvectionStruct.toSpecialLinearGroup) = ⊤) : points r R = Matrix.SpecialLinearGroup.toGL.range

If elementary transvections generate SL_{r+1}(R), then the matrix points of the full-weight type A_r carrier over R are exactly the range of SL_{r+1}(R) in GL_{r+1}(R).