Maximal tori in Hopf coordinates

A closed subgroup of an affine group is encoded contravariantly by a Hopf ideal in its coordinate algebra. This file defines a maximal torus to be a torus closed subgroup which is not properly contained in another torus. Thus, if I is maximal and J ≤ I defines a torus, then I = J.

Main declarations

• TauCeti.HopfIdeal.IsMaximalTorus: maximality among torus Hopf ideals.
• TauCeti.HopfIdeal.isMaximalTorus_of_baseChange: maximality descends from an algebraic closure along a base-change isomorphism of the ambient coordinate Hopf algebra.

References

• J. S. Milne, Algebraic Groups (2017), §§12 and 17.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §8.

The isomorphism-invariance API follows the formal organization of TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Isomorphism and TauCeti.Algebra.AlgebraicGroup.Solvable.Radical.Isomorphism.

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

A Hopf ideal defines a maximal torus when its quotient coordinate Hopf algebra is a torus and every torus closed subgroup containing it is equal to it.

Because coordinate rings reverse arrows, 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.

@[simp]

theorem TauCeti.HopfIdeal.isMaximalTorus_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I : HopfIdeal k ↑H) : IsMaximalTorus k H I ↔ torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := H, property := ⋯ } I) ∧ ∀ (J : HopfIdeal k ↑H), torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := H, property := ⋯ } J) → J ≤ I → I ≤ J

The Hopf-ideal criterion for a maximal torus: the quotient is a torus and no strictly larger torus closed subgroup contains it.

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

Pulling a maximal torus back across an ambient Hopf-algebra isomorphism gives a maximal torus in the source.

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

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

theorem TauCeti.HopfIdeal.isMaximalTorus_of_baseChange {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {H' : CommHopfAlgCat (AlgebraicClosure k)} [Algebra.FiniteType (AlgebraicClosure k) ↑H'] (I : HopfIdeal k ↑H) (I' : HopfIdeal (AlgebraicClosure k) ↑H') (e : CommHopfAlgCat.baseChange H ≅ H') (hI : torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := H, property := ⋯ } I)) (hmap : (CommHopfAlgCat.baseChangeHopfIdeal I).map (CommHopfAlgCat.Hom.hom e.hom) = I') (hmax : IsMaximalTorus (AlgebraicClosure k) H' I') : IsMaximalTorus k H I

Maximality of a torus descends from an algebraic closure. If I cuts out a torus over k and its base change, transported along an isomorphism e of the base-changed ambient coordinate Hopf algebra, is a maximal torus over the algebraic closure, then I is a maximal torus over k.