The type A full-weight carrier has determinant one

The standard Chevalley generators of sl_{r+1} act as matrix units, so their divided-power exponentials are transvections. The product of the weights of the standard representation is the trivial character. Consequently every generator used to define TauCeti.SlStd.groupScheme r has determinant one, and the carrier is a closed subgroup scheme of SL_{r+1}.

This is the determinant-one half of identifying the full-weight type A_r carrier with the special linear group scheme. The reverse inclusion, which requires a generation theorem, is not asserted here.

Main declarations

• TauCeti.SlStd.kostantRootSubgroupMatrix_eq_transvection: the represented type-A root subgroups are the standard elementary transvections.
• TauCeti.SlStd.specialLinearDefiningHopfIdeal_le_kostantToralDefiningIdeal: the determinant-one equation belongs to the carrier's defining Hopf ideal.
• TauCeti.SlStd.det_eq_one_of_mem_points: every matrix point of the carrier has determinant one.
• TauCeti.SlStd.toSpecialLinear: the canonical closed immersion from the carrier to SL_{r+1}.
• TauCeti.SlStd.toSpecialLinear_comp_groupSchemeι: composing with SL_{r+1} → GL_{r+1} recovers the carrier inclusion.

This advances Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md: the full-weight type A carrier is now proved to lie in the expected pinned ambient group. Identifying it with that group remains the generation step.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §3.

theorem TauCeti.SlStd.kostantRootSubgroupMatrix_eq_transvection (r : ℕ) {A : Type u_1} [CommRing A] (k : Fin r ⊕ Fin r) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)) : (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ k ⋯ (latticeBasis r)) q = transvectionUnit ⋯ (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv q))

The represented type-A root subgroup is the elementary transvection from the root source to the root target.

theorem TauCeti.SlStd.specialLinearDefiningHopfIdeal_le_kostantToralDefiningIdeal (r : ℕ) : SpecialLinear.definingHopfIdeal ℤ (r + 1) ≤ UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (rootGenerator r) (cartanGenerator r) (rep r) (lattice r).toAddSubgroup ⋯ ⋯ (latticeBasis r) (weight r)

The determinant-one equation belongs to the defining Hopf ideal of the full-weight type A_r carrier. Equivalently, every represented root subgroup and the represented weight torus factor through SL_{r+1}.

theorem TauCeti.SlStd.det_eq_one_of_mem_points (r : ℕ) {A : Type u_1} [CommRing A] {g : GL (Fin (r + 1)) A} (hg : g ∈ points r A) : Matrix.GeneralLinearGroup.det g = 1

Every matrix-valued point of the full-weight type A_r carrier has determinant one.

noncomputable def TauCeti.SlStd.toSpecialLinear (r : ℕ) : groupScheme r ⟶ SpecialLinear.groupScheme ℤ (r + 1)

The canonical morphism from the full-weight type A_r carrier to SL_{r+1}, induced by the containment of defining Hopf ideals.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.SlStd.isClosedImmersion_toSpecialLinear (r : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (toSpecialLinear r).hom.hom)

The canonical morphism from the type A_r carrier to SL_{r+1} is a closed immersion.

@[simp]

theorem TauCeti.SlStd.toSpecialLinear_comp_groupSchemeι (r : ℕ) : CategoryTheory.CategoryStruct.comp (toSpecialLinear r) (SpecialLinear.groupSchemeι ℤ (r + 1)) = carrierι r

Including the type A_r carrier into SL_{r+1} and then into GL_{r+1} recovers its original ambient closed immersion.