Documentation

TauCeti.Algebra.AlgebraicGroup.Reductive.Over

Reductive affine group schemes over a ring #

A reductive affine group scheme over Spec R is smooth over R and has connected reductive geometric fibers. In Hopf coordinates, its geometric fibers are the scalar extensions k ⊗[R] H for algebraically closed fields k equipped with an R-algebra structure. The finite-type ambient category and smoothness give finite presentation; neither reducedness of R nor a field hypothesis on R is required.

reductiveCommHopfAlgPropertyOver keeps this condition separate from the ambient category and from the choice of a maximal torus. Its base-change theorem permits an integral group scheme and its specializations to be recognized using the same condition.

References #

source
def TauCeti.reductiveCommHopfAlgPropertyOver (R : Type u) [CommRing R] :
CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat R)

A finite-type affine group scheme over a commutative ring is reductive when it is smooth and all of its geometric fibers are connected reductive groups.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.reductiveCommHopfAlgPropertyOver_iff (R : Type u) [CommRing R] (H : FiniteTypeCommHopfAlgCat R) :
    reductiveCommHopfAlgPropertyOver R H ↔ Algebra.Smooth R ↑H.obj ∧ ∀ (k : Type u) [inst : Field k] [inst_1 : Algebra R k] [IsAlgClosed k], reductiveCommHopfAlgProperty k H.baseChange

    The geometric-fiber characterization of a reductive affine group scheme over a ring.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatReductiveCommHopfAlgPropertyOver (R : Type u) [CommRing R] :
    (reductiveCommHopfAlgPropertyOver R).IsClosedUnderIsomorphisms

    Reductivity over a ring is invariant under coordinate-Hopf-algebra isomorphism.

    source
    theorem TauCeti.reductiveCommHopfAlgPropertyOver.smooth {R : Type u} [CommRing R] {H : FiniteTypeCommHopfAlgCat R} (hH : reductiveCommHopfAlgPropertyOver R H) :
    Algebra.Smooth R ↑H.obj

    A reductive group scheme is smooth over its base.

    source
    theorem TauCeti.reductiveCommHopfAlgPropertyOver.geometricFiber {R : Type u} [CommRing R] {H : FiniteTypeCommHopfAlgCat R} (hH : reductiveCommHopfAlgPropertyOver R H) (k : Type u) [Field k] [Algebra R k] [IsAlgClosed k] :
    reductiveCommHopfAlgProperty k H.baseChange

    Every geometric fiber of a reductive group scheme is reductive.

    source
    theorem TauCeti.reductiveCommHopfAlgPropertyOver.baseChange {R : Type u} [CommRing R] {H : FiniteTypeCommHopfAlgCat R} (hH : reductiveCommHopfAlgPropertyOver R H) (S : Type u) [CommRing S] [Algebra R S] :
    reductiveCommHopfAlgPropertyOver S H.baseChange

    Reductivity of affine group schemes is preserved by arbitrary base change.