Borel subgroups in Hopf coordinates

A closed subgroup of a finite-type affine group over a field is encoded contravariantly by a Hopf ideal in its coordinate algebra. This file defines a Borel subgroup to be a smooth, geometrically connected, geometrically solvable closed subgroup whose base change to an algebraic closure is maximal among closed subgroups with those properties.

Smoothness remains explicit: the ambient affine group need not be smooth, and geometric connectedness and solvability alone do not exclude nonreduced subgroup schemes. Because Hopf ideals reverse subgroup inclusion, maximality of the represented subgroup is minimality of its defining ideal among ideals satisfying the three geometric properties after base change to an algebraic closure. This geometric maximality is essential over a non-algebraically-closed field: maximality only among subgroups defined over the ground field is not the Borel condition.

Main declarations

• TauCeti.HopfIdeal.IsBorelCandidate: a smooth, geometrically connected, geometrically solvable closed subgroup, before imposing maximality.
• TauCeti.HopfIdeal.IsBorelOverAlgClosed: the Borel-subgroup predicate over an algebraically closed field.
• TauCeti.HopfIdeal.IsBorelOverAlgClosed.comapOfIso and TauCeti.HopfIdeal.IsBorelOverAlgClosed.of_map_eq: transport of the algebraically closed Borel property across an ambient Hopf-algebra isomorphism.
• TauCeti.HopfIdeal.IsBorel: the Borel-subgroup predicate in Hopf coordinates.
• TauCeti.HopfIdeal.IsBorel.comapOfIso_iff: Borel status is invariant under an ambient Hopf-algebra isomorphism.

References

• J. S. Milne, Algebraic Groups (2017), Section 17.a.
• T. A. Springer, Linear Algebraic Groups, Sections 6.2--6.3.

def TauCeti.HopfIdeal.IsBorelCandidate (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : Prop

A Hopf ideal is a Borel candidate when its quotient coordinate algebra represents a smooth, geometrically connected, geometrically solvable closed subgroup.

Over an algebraically closed field, a Borel subgroup is a maximal such candidate. Over a general field, IsBorel instead requires maximality after base change to an algebraic closure. Keeping the non-maximal condition named is useful for constructing Borels by a maximal-dimension argument and for asking that a Borel contain a prescribed smooth, geometrically connected, geometrically solvable subgroup.

Equations

• TauCeti.HopfIdeal.IsBorelCandidate k H I = TauCeti.HopfIdeal.borelQuotientProperty✝ k (H.quotient I)

@[simp]

theorem TauCeti.HopfIdeal.isBorelCandidate_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : IsBorelCandidate k H I ↔ smoothCommHopfAlgProperty k (H.quotient I).obj ∧ geometricallyConnectedCommHopfAlgProperty k (H.quotient I).obj ∧ geometricallySolvablePointsCommHopfAlgProperty k (H.quotient I).obj

The three geometric conditions defining a Borel candidate.

theorem TauCeti.HopfIdeal.IsBorelCandidate.mk {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (h_smooth : smoothCommHopfAlgProperty k (H.quotient I).obj) (h_connected : geometricallyConnectedCommHopfAlgProperty k (H.quotient I).obj) (h_solvable : geometricallySolvablePointsCommHopfAlgProperty k (H.quotient I).obj) : IsBorelCandidate k H I

Construct a Borel candidate from smoothness, geometric connectedness, and geometric solvability.

theorem TauCeti.HopfIdeal.IsBorelCandidate.smooth {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelCandidate k H I) : smoothCommHopfAlgProperty k (H.quotient I).obj

A Borel candidate is smooth.

theorem TauCeti.HopfIdeal.IsBorelCandidate.geometricallyConnected {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelCandidate k H I) : geometricallyConnectedCommHopfAlgProperty k (H.quotient I).obj

A Borel candidate is geometrically connected.

theorem TauCeti.HopfIdeal.IsBorelCandidate.geometricallySolvable {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelCandidate k H I) : geometricallySolvablePointsCommHopfAlgProperty k (H.quotient I).obj

A Borel candidate has a solvable group of geometric points.

theorem TauCeti.HopfIdeal.IsBorelCandidate.comapOfIso {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelCandidate k H I) {L : FiniteTypeCommHopfAlgCat k} (e : L ≅ H) : IsBorelCandidate k L (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling back along an ambient Hopf-algebra isomorphism preserves Borel candidatehood.

def TauCeti.HopfIdeal.IsBorelOverAlgClosed (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : Prop

Over an algebraically closed field, a Hopf ideal defines a Borel subgroup when it is minimal among Borel candidates. In the contravariant Hopf-ideal order, this means that the represented closed subgroup is maximal among smooth, geometrically connected, geometrically solvable closed subgroups.

Equations

• TauCeti.HopfIdeal.IsBorelOverAlgClosed k H I = (IsAlgClosed k ∧ Minimal (TauCeti.HopfIdeal.IsBorelCandidate k H) I)

@[simp]

theorem TauCeti.HopfIdeal.isBorelOverAlgClosed_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : IsBorelOverAlgClosed k H I ↔ IsAlgClosed k ∧ Minimal (IsBorelCandidate k H) I

The algebraically-closed-field Borel condition asserts algebraic closedness and minimality among Borel candidates.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.comapOfIso {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} {J : HopfIdeal k ↑L.obj} (hJ : IsBorelOverAlgClosed k L J) (e : H ≅ L) : IsBorelOverAlgClosed k H (J.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling an algebraically closed Borel subgroup back across an ambient Hopf-algebra isomorphism gives an algebraically closed Borel subgroup in the source.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.of_map_eq {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} {J : HopfIdeal k ↑L.obj} (e : H ≅ L) (hmap : I.map (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) = J) (hJ : IsBorelOverAlgClosed k L J) : IsBorelOverAlgClosed k H I

Transport the algebraically closed Borel property across an ambient Hopf-algebra isomorphism that maps one defining ideal to the other.

def TauCeti.HopfIdeal.IsBorel (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : Prop

A Hopf ideal defines a Borel subgroup when, after base change to an algebraic closure, its quotient coordinate algebra is smooth, geometrically connected, and geometrically solvable, and no strictly larger closed subgroup has all three properties.

The order is contravariant: J ≤ I says that the subgroup cut out by I is contained in the subgroup cut out by J.

Equations

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

theorem TauCeti.HopfIdeal.isBorel_iff_isBorelOverAlgClosed_baseChange (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : let K := AlgebraicClosure k; let H' := FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }; have I' := CommHopfAlgCat.baseChangeHopfIdeal I; IsBorel k H I ↔ IsBorelOverAlgClosed K H' I'

The general-field Borel predicate is the algebraically-closed-field Borel predicate after base change to an algebraic closure.

@[simp]

theorem TauCeti.HopfIdeal.isBorel_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : let K := AlgebraicClosure k; let H' := FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }; have I' := CommHopfAlgCat.baseChangeHopfIdeal I; IsBorel k H I ↔ smoothCommHopfAlgProperty K (H'.quotient I').obj ∧ geometricallyConnectedCommHopfAlgProperty K (H'.quotient I').obj ∧ geometricallySolvablePointsCommHopfAlgProperty K (H'.quotient I').obj ∧ ∀ (J : HopfIdeal K ↑H'.obj), smoothCommHopfAlgProperty K (H'.quotient J).obj → geometricallyConnectedCommHopfAlgProperty K (H'.quotient J).obj → geometricallySolvablePointsCommHopfAlgProperty K (H'.quotient J).obj → J ≤ I' → I' ≤ J

The Hopf-ideal criterion for a Borel subgroup: after algebraic-closure base change, its quotient is smooth, geometrically connected, and geometrically solvable, and it is maximal among such closed subgroups.

theorem TauCeti.HopfIdeal.IsBorel.comapOfIso {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑L.obj} (hI : IsBorel k L.obj I) (e : H ≅ L) : IsBorel k H.obj (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling a Borel subgroup back across an ambient Hopf-algebra isomorphism gives a Borel subgroup in the source.

theorem TauCeti.HopfIdeal.IsBorel.comapOfIso_iff {k : Type u} [Field k] {H L : FiniteTypeCommHopfAlgCat k} (e : H ≅ L) (I : HopfIdeal k ↑L.obj) : IsBorel k H.obj (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯) ↔ IsBorel k L.obj I

Borel status is invariant under pulling the defining ideal back across an ambient Hopf-algebra isomorphism.