Documentation

TauCeti.Algebra.AlgebraicGroup.Borel.Over

Borel subgroups of affine group schemes over a ring #

Let H be the coordinate Hopf algebra of a finite-type affine group G over a commutative ring R, and let I be a Hopf ideal of H, cutting out a closed subgroup B of G. Then B is a Borel subgroup of G when it is smooth over R and every geometric fiber of B is a Borel subgroup of the corresponding geometric fiber of G: for every algebraically closed field k with an R-algebra structure, the base-changed ideal I_k is minimal among the defining ideals of smooth, connected, solvable closed subgroups of G_k.

This is the relative notion of Borel subgroup used for reductive group schemes, where a pinning consists of a split maximal torus, a Borel subgroup containing it, and root vectors for the simple roots. Smoothness over the base is imposed explicitly, as in the relative definition; the fiberwise condition alone only controls the geometric fibers.

Over a field k, a Borel subgroup in this sense is in particular a Borel subgroup in the sense of TauCeti.HopfIdeal.IsBorel, which only tests the base change to AlgebraicClosure k.

Borel subgroups over a ring are transported along isomorphisms of coordinate Hopf algebras and are stable under arbitrary base change R → S, so a Borel subgroup chosen over ℤ specializes to every commutative ring.

Main declarations #

References #

source
def TauCeti.HopfIdeal.IsBorelOver (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Algebra.FiniteType R ↑H] (I : HopfIdeal R ↑H) :
Prop

A Hopf ideal I of the coordinate Hopf algebra H of a finite-type affine group G over R cuts out a Borel subgroup of G when the closed subgroup it defines is smooth over R and, on every geometric fiber, is a Borel subgroup of the geometric fiber of G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.HopfIdeal.isBorelOver_iff (R : Type u) [CommRing R] (H : CommHopfAlgCat R) [Algebra.FiniteType R ↑H] (I : HopfIdeal R ↑H) :
    IsBorelOver R H I ↔ Algebra.Smooth R ↑(CommHopfAlgCat.quotient H I) ∧ ∀ (k : Type u) [inst : Field k] [inst_1 : Algebra R k] [IsAlgClosed k], IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }) (CommHopfAlgCat.baseChangeHopfIdeal I)

    A Borel subgroup over a ring is a smooth closed subgroup whose geometric fibers are Borel subgroups.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.mk {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {I : HopfIdeal R ↑H} (h_smooth : Algebra.Smooth R ↑(CommHopfAlgCat.quotient H I)) (h_fiber : ∀ (k : Type u) [inst : Field k] [inst_1 : Algebra R k] [IsAlgClosed k], IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }) (CommHopfAlgCat.baseChangeHopfIdeal I)) :
    IsBorelOver R H I

    Construct a Borel subgroup over a ring from smoothness over the base and the Borel property of every geometric fiber.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.smooth {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {I : HopfIdeal R ↑H} (hI : IsBorelOver R H I) :
    Algebra.Smooth R ↑(CommHopfAlgCat.quotient H I)

    A Borel subgroup over a ring is smooth over the base.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.geometricFiber {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {I : HopfIdeal R ↑H} (hI : IsBorelOver R H I) (k : Type u) [Field k] [Algebra R k] [IsAlgClosed k] :
    IsBorelOverAlgClosed k (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }) (CommHopfAlgCat.baseChangeHopfIdeal I)

    Every geometric fiber of a Borel subgroup over a ring is a Borel subgroup of the geometric fiber of the ambient group.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.isBorel {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorelOver k H I) :
    IsBorel k H I

    Over a field, a Borel subgroup over the base is a Borel subgroup: its base change to the algebraic closure is a Borel subgroup there.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.comapOfIso {R : Type u} [CommRing R] {H L : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] [Algebra.FiniteType R ↑L] {J : HopfIdeal R ↑L} (hJ : IsBorelOver R L J) (e : H ≅ L) :
    IsBorelOver R H (J.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯)

    Pulling a Borel subgroup back across an isomorphism e : H ≅ L of coordinate Hopf algebras gives a Borel subgroup of the source.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.comapOfIso_iff {R : Type u} [CommRing R] {H L : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] [Algebra.FiniteType R ↑L] (J : HopfIdeal R ↑L) (e : H ≅ L) :
    IsBorelOver R H (J.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯) ↔ IsBorelOver R L J

    Borel status over a ring is invariant under pulling the defining ideal back across an isomorphism of coordinate Hopf algebras.

    source
    theorem TauCeti.HopfIdeal.IsBorelOver.baseChange {R : Type u} [CommRing R] {H : CommHopfAlgCat R} [Algebra.FiniteType R ↑H] {I : HopfIdeal R ↑H} (S : Type u) [CommRing S] [Algebra R S] (hI : IsBorelOver R H I) :
    IsBorelOver S (CommHopfAlgCat.baseChange H) (CommHopfAlgCat.baseChangeHopfIdeal I)

    Base change of a Borel subgroup along R → S: the base-changed ideal cuts out a Borel subgroup of the base-changed affine group. Its geometric fibers are geometric fibers of the original Borel subgroup.