The rank-one Kostant elementary group on field-valued points

This file identifies the elementary group obtained by applying the Kostant construction to the standard two-dimensional representation of sl₂ with the determinant-one matrices. Over an arbitrary commutative ring its two Kostant root subgroups are the upper and lower elementary transvections TauCeti.transvectionUnit, so the elementary group always lies in the image of SL₂; only the reverse inclusion needs a field, where those transvections generate SL₂.

Main declarations

• TauCeti.Sl2Std.kostantRootSubgroupMatrix_eq_transvectionUnit and TauCeti.Sl2Std.map_kostantRootSubgroupParam_eq_transvectionUnit: over any commutative ring the two Kostant root subgroups are the standard upper and lower root subgroups of SL₂, in matrix and in parameter form.
• TauCeti.Sl2Std.transvectionUnit_mem_map_kostantElementarySubgroup and TauCeti.Sl2Std.map_kostantElementarySubgroup_le_range_toGL: over any commutative ring the standard transvections lie in the matrix image of the Kostant elementary group, and that image lies in the image of SL₂.
• TauCeti.Sl2Std.map_kostantElementarySubgroup_eq_range_toGL: over a field, the standard rank-one Kostant elementary group is exactly the image of SL₂ in GL₂.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 8.2.
• J. E. Humphreys, Linear Algebraic Groups, §26.

This verifies the elementary-group side of the rank-one point-generation case of Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md. Together with TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_generatedPoints, it places every SL₂ point inside the points of the constructed group scheme; identifying that scheme with the standard special-linear scheme is a separate scheme-theoretic step.

theorem TauCeti.Sl2Std.kostantRootSubgroupMatrix_eq_transvectionUnit {A : Type u_1} [CommRing A] (i : Fin 2) (t : Multiplicative A) : (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ i ⋯ (integralLatticeAddSubgroupBasis 1)) (AdditiveGroup.gaPointsMulEquiv.symm t) = transvectionUnit ⋯ (Multiplicative.toAdd t)

The rank-one Kostant root subgroups are the standard transvections. The matrix of a Kostant root-subgroup element for the root i is the determinant-one transvection at the index pair (i, i.rev), over an arbitrary commutative ring.

theorem TauCeti.Sl2Std.map_kostantRootSubgroupParam_eq_transvectionUnit (A : Type) [CommRing A] (i : Fin 2) (t : Multiplicative A) : (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1))).toMulEquiv) ((UniversalEnvelopingAlgebra.kostantRootSubgroupParam ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ i ⋯ ↧A) t) = transvectionUnit ⋯ (Multiplicative.toAdd t)

In basis coordinates a rank-one Kostant root-subgroup parameter value is the standard transvection of the same parameter.

theorem TauCeti.Sl2Std.transvectionUnit_mem_map_kostantElementarySubgroup (A : Type) [CommRing A] {i j : Fin 2} (hij : i ≠ j) (t : A) : transvectionUnit hij t ∈ Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1))).toMulEquiv) (UniversalEnvelopingAlgebra.kostantElementarySubgroup ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ ⋯ ↧A)

Every standard rank-one transvection belongs to the matrix image of the Kostant elementary group, over an arbitrary commutative ring.

theorem TauCeti.Sl2Std.map_kostantElementarySubgroup_le_range_toGL (A : Type) [CommRing A] : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (integralLatticeAddSubgroupBasis 1))).toMulEquiv) (UniversalEnvelopingAlgebra.kostantElementarySubgroup ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ ⋯ ↧A) ≤ Matrix.SpecialLinearGroup.toGL.range

Over an arbitrary commutative ring the matrix image of the standard rank-one Kostant elementary group lies in the image of SL₂ in GL₂: it is generated by transvections, which have determinant one.

theorem TauCeti.Sl2Std.map_kostantElementarySubgroup_eq_range_toGL (F : Type) [Field F] : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange F (integralLatticeAddSubgroupBasis 1))).toMulEquiv) (UniversalEnvelopingAlgebra.kostantElementarySubgroup ![(slFinTwoBasis ℚ) 0, (slFinTwoBasis ℚ) 1] ![(slFinTwoBasis ℚ) 2] (repEnveloping ℚ 1) (integralLattice 1).toAddSubgroup ⋯ ⋯ ↧F) = Matrix.SpecialLinearGroup.toGL.range

The rank-one elementary-group identification for the Kostant construction. Over a field, the matrix image of the elementary group constructed from the standard two-dimensional sl₂ lattice is exactly the image of SL₂ in GL₂.