Adjoint semisimple affine groups in Hopf coordinates

A semisimple affine group over a field is adjoint when its scheme-theoretic center is trivial. For a commutative Hopf algebra H, closed subgroup schemes are encoded contravariantly by Hopf ideals. Thus the center is trivial precisely when its defining ideal is the augmentation ideal, which cuts out the identity subgroup.

This file packages that condition as an isomorphism-invariant property of semisimple finite-type commutative Hopf algebras. Its characteristic pointwise form says that every universally central algebra-valued point is the identity. This criterion quantifies over all commutative value algebras; testing only rational points would miss infinitesimal centers such as mu_p in characteristic p.

Main declarations

• TauCeti.adjointSemisimpleCommHopfAlgProperty: adjointness for semisimple finite-type commutative Hopf algebras.
• TauCeti.AdjointSemisimpleCommHopfAlgCat: the corresponding full subcategory.
• TauCeti.adjointSemisimpleCommHopfAlgProperty_iff_forall_isCentralPoint_eq_one: adjointness is equivalent to triviality of every universally central algebra-valued point.

References

• J. S. Milne, Algebraic Groups (2017), §§1.k and 21.4.
• T. A. Springer, Linear Algebraic Groups, §9.6.

def TauCeti.adjointSemisimpleCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (SemisimpleCommHopfAlgCat k)

The object property selecting adjoint semisimple affine groups in Hopf coordinates.

An object is already semisimple by belonging to SemisimpleCommHopfAlgCat k. Adjointness says that its represented center is the identity subgroup, so the center defining ideal is the augmentation ideal.

Equations

• TauCeti.adjointSemisimpleCommHopfAlgProperty k H = (TauCeti.CommHopfAlgCat.centerDefiningIdeal H.obj.obj = TauCeti.HopfIdeal.augmentation k ↑H.obj.obj)

@[simp]

theorem TauCeti.adjointSemisimpleCommHopfAlgProperty_iff {k : Type u} [Field k] (H : SemisimpleCommHopfAlgCat k) : adjointSemisimpleCommHopfAlgProperty k H ↔ CommHopfAlgCat.centerDefiningIdeal H.obj.obj = HopfIdeal.augmentation k ↑H.obj.obj

Membership in the adjoint property means that the center defining ideal is the augmentation ideal.

theorem TauCeti.adjointSemisimpleCommHopfAlgProperty.isCentralPoint_eq_one {k : Type u} [Field k] {H : SemisimpleCommHopfAlgCat k} (hH : adjointSemisimpleCommHopfAlgProperty k H) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) (hg : HopfAlgebra.IsCentralPoint g) : g = 1

Every universally central point of an adjoint semisimple affine group is the identity.

theorem TauCeti.adjointSemisimpleCommHopfAlgProperty_iff_forall_isCentralPoint_eq_one {k : Type u} [Field k] (H : SemisimpleCommHopfAlgCat k) : adjointSemisimpleCommHopfAlgProperty k H ↔ ∀ (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)), HopfAlgebra.IsCentralPoint g → g = 1

A semisimple affine group is adjoint exactly when every universally central point over every commutative value algebra is the identity.

instance TauCeti.instIsClosedUnderIsomorphismsSemisimpleCommHopfAlgCatAdjointSemisimpleCommHopfAlgProperty (k : Type u) [Field k] : (adjointSemisimpleCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Adjointness of semisimple commutative Hopf algebras is invariant under isomorphism.

@[reducible, inline]

abbrev TauCeti.AdjointSemisimpleCommHopfAlgCat (k : Type u) [Field k] : Type (u + 1)

The category of adjoint semisimple finite-type commutative Hopf algebras over a field.

Equations

• TauCeti.AdjointSemisimpleCommHopfAlgCat k = (TauCeti.adjointSemisimpleCommHopfAlgProperty k).FullSubcategory