Field-valued points of the type A full-weight carrier

This file proves that over a field the matrix points of the full-weight type A_r carrier are exactly SL_{r+1}. The ring-general transvection generation step is proved in TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.Generation; Mathlib's generation of special linear groups by transvections then gives the result.

The result is the reverse, on field-valued points, of the determinant-one containment proved in TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.DeterminantOne. It is a pointwise generation step toward identifying the integral carrier group scheme with the special linear group scheme; the equality of their defining Hopf ideals over ℤ is not asserted here.

Main results

• TauCeti.SlStd.toGL_mem_points: every determinant-one matrix over a field is a point of the carrier.
• TauCeti.SlStd.mem_points_iff_det_eq_one: over a field, carrier-point membership is equivalent to having determinant one.
• TauCeti.SlStd.points_eq_range_toGL: over a field, the carrier points are exactly the image of SL_{r+1} in GL_{r+1}.

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 proves the missing generation statement for the explicit full-weight type A carrier on points over fields.

theorem TauCeti.SlStd.points_eq_range_toGL (r : ℕ) {K : Type u} [Field K] : points r K = Matrix.SpecialLinearGroup.toGL.range

Over a field, 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.toGL_mem_points (r : ℕ) {K : Type u} [Field K] (g : Matrix.SpecialLinearGroup (Fin (r + 1)) K) : Matrix.SpecialLinearGroup.toGL g ∈ points r K

The canonical inclusion of every determinant-one matrix over a field is a point of the full-weight type A_r carrier.

theorem TauCeti.SlStd.mem_points_iff_det_eq_one (r : ℕ) {K : Type u} [Field K] (g : GL (Fin (r + 1)) K) : g ∈ points r K ↔ Matrix.GeneralLinearGroup.det g = 1

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