Reductivity of the type A standard carrier

The full-weight type A_r standard carrier is an explicit closed subgroup of GL_{r+1} over ℤ, constructed from its numbered root subgroups and weight torus. After specialization to an algebraically closed field, its defining Hopf ideal is the determinant-one ideal by TauCeti.SlStd.baseChangeDefiningIdeal_eq_specialLinearDefiningHopfIdeal. Thus its coordinate Hopf algebra is isomorphic to that of SL_{r+1}.

This file packages the specialized carrier as a finite-type commutative Hopf algebra, lifts the coordinate isomorphism to that category, and transports the reductivity of SL_{r+1} across it. Consequently the explicit type A carrier has the substantive reductive-group property required of a Chevalley--Demazure carrier over every algebraically closed field, in arbitrary characteristic.

Main declarations

• TauCeti.SlStd.finiteTypeSpecialization: the specialized type A_r carrier as a finite-type commutative Hopf algebra.
• TauCeti.SlStd.finiteTypeSpecializationSpecialLinearIso: its canonical isomorphism with the coordinate Hopf algebra of SL_{r+1} over an algebraically closed field.
• TauCeti.SlStd.reductiveCommHopfAlgProperty_finiteTypeSpecialization: the specialized type A_r carrier is reductive.

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 the ReductiveGroups roadmap: the explicit type A carrier is now reductive over the algebraically closed fields on which the finite groups of Lie type are constructed. Its consumer is milestone L0, "pinned ambient groups", of the CFSGStatement roadmap.

noncomputable def TauCeti.SlStd.finiteTypeSpecialization (r : ℕ) (k : Type u) [CommRing k] : FiniteTypeCommHopfAlgCat k

The specialization of the full-weight type A_r carrier to k, bundled with its finite-type property. It is the quotient of O(GL_{r+1}/k) by the transported integral carrier equations.

Equations

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

@[simp]

theorem TauCeti.SlStd.finiteTypeSpecialization_obj (r : ℕ) (k : Type u) [CommRing k] : (finiteTypeSpecialization r k).obj = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k (r + 1)) (baseChangeDefiningIdeal r k)

The object underlying the finite-type specialization is the quotient coordinate Hopf algebra used by the base-change presentation of the carrier.

noncomputable def TauCeti.SlStd.finiteTypeSpecializationSpecialLinearIso (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : finiteTypeSpecialization r k ≅ SpecialLinear.finiteTypeCoordinateHopfAlgebra k (r + 1)

Over an algebraically closed field, the specialized full-weight type A_r carrier is canonically isomorphic to the finite-type coordinate Hopf algebra of SL_{r+1}.

Equations

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

@[simp]

theorem TauCeti.SlStd.finiteTypeSpecializationSpecialLinearIso_hom_hom (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : (finiteTypeSpecializationSpecialLinearIso r k).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ baseChangeCoordinateSpecialLinearIso r k ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying coordinate morphism of the finite-type carrier--special-linear isomorphism is the canonical composite obtained from the quotient-coordinate isomorphism.

theorem TauCeti.SlStd.reductiveCommHopfAlgProperty_finiteTypeSpecialization (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : reductiveCommHopfAlgProperty k (finiteTypeSpecialization r k)

The full-weight type A_r carrier is reductive over every algebraically closed field.

The statement is valid in arbitrary characteristic. It transports the reductivity of SL_{r+1} across the scheme-theoretic identification of the explicit carrier with SL_{r+1}.