The type A carrier over an algebraically closed field

The full-weight type A_r Kostant carrier is constructed over ℤ as the closed subgroup of GL_{r+1} generated by the numbered root subgroups and its weight torus. After extension to a field, its matrix points are already known to be exactly the determinant-one matrices. This file upgrades that pointwise statement to an equality of defining Hopf ideals over an algebraically closed field:

  baseChangeDefiningIdeal r k = SpecialLinear.definingHopfIdeal k (r + 1).

The passage from points to equations uses reduced finite-type point separation. The special-linear coordinate algebra is smooth, hence reduced, so only the determinant-one side of the comparison needs a reducedness input. The resulting quotient isomorphism identifies the base-changed explicit carrier with the coordinate Hopf algebra of SL_{r+1}.

Main declarations

• TauCeti.SlStd.mem_baseChangeDefiningPointsSubgroup_iff_mem_points: on base-ring-valued points, the transported carrier equations cut out the original integral carrier's matrices.
• TauCeti.SlStd.baseChangeDefiningIdeal_eq_specialLinearDefiningHopfIdeal: over an algebraically closed field, the transported carrier and special-linear defining ideals agree.
• TauCeti.SlStd.baseChangeCoordinateSpecialLinearIso: the induced coordinate Hopf-algebra isomorphism with SL_{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 the ReductiveGroups roadmap: it identifies the explicit full-weight type A carrier with the expected simply connected reductive group after extension to an algebraically closed field. Its consumer is milestone L0, "explicit pinned Chevalley--Demazure groups", of the CFSGStatement roadmap.

theorem TauCeti.SlStd.mem_baseChangeDefiningPointsSubgroup_iff_mem_points (r : ℕ) (k : Type u) [CommRing k] (g : ↑(HopfAlgebra.points ↧k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra k (r + 1)) (baseChangeDefiningIdeal r k) ↧k ↔ (GeneralLinear.pointsMulEquiv (r + 1)) g ∈ points r k

A base-ring-valued point satisfies the transported defining equations of the type A_r carrier exactly when its underlying matrix is a point of the original integral carrier. This holds over every commutative base ring.

theorem TauCeti.SlStd.specialLinearDefiningHopfIdeal_le_baseChangeDefiningIdeal (r : ℕ) (A : Type u) [CommRing A] : SpecialLinear.definingHopfIdeal A (r + 1) ≤ baseChangeDefiningIdeal r A

The determinant-one ideal is contained in the transported defining ideal of the full-weight type A_r carrier over every commutative ring. Equivalently, every point of the transported carrier has determinant one.

theorem TauCeti.SlStd.baseChangeDefiningIdeal_eq_specialLinearDefiningHopfIdeal (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : baseChangeDefiningIdeal r k = SpecialLinear.definingHopfIdeal k (r + 1)

Over an algebraically closed field, the transported defining ideal of the full-weight type A_r carrier is the determinant-one ideal. Thus the explicit carrier obtained from the Kostant construction is scheme-theoretically SL_{r+1}, not merely equal to it on field-valued points.

noncomputable def TauCeti.SlStd.baseChangeCoordinateSpecialLinearIso (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k (r + 1)) (baseChangeDefiningIdeal r k) ≅ SpecialLinear.coordinateHopfAlgebra k (r + 1)

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

Equations

• TauCeti.SlStd.baseChangeCoordinateSpecialLinearIso r k = CategoryTheory.eqToIso ⋯

@[simp]

theorem TauCeti.SlStd.mkQuotient_comp_baseChangeCoordinateSpecialLinearIso_hom (r : ℕ) (k : Type u) [Field k] [IsAlgClosed k] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k (r + 1)) (baseChangeDefiningIdeal r k)) (baseChangeCoordinateSpecialLinearIso r k).hom = SpecialLinear.coordinateMap k (r + 1)

The carrier--special-linear coordinate isomorphism is compatible with their quotient maps from O(GL_{r+1}/k).