Adjoint semisimple affine group schemes

A semisimple affine group scheme over a field is adjoint when its scheme-theoretic center is trivial. This file transports the Hopf-coordinate property adjointSemisimpleCommHopfAlgProperty across the anti-equivalence between semisimple finite-type commutative Hopf algebras and semisimple affine group schemes.

The coordinate characterization says that the Hopf ideal defining the center is the augmentation ideal defining the identity subgroup. By adjointSemisimpleCommHopfAlgProperty_iff_forall_isCentralPoint_eq_one, this is equivalently the all-value-algebras statement that every universally central point is the identity. In particular, adjointness here detects infinitesimal centers and is stronger than triviality of the center on points over the ground field alone.

Main declarations

• TauCeti.adjointSemisimpleAffineGroupSchemeProperty: adjointness for semisimple affine group schemes over a field.
• TauCeti.AdjointSemisimpleAffineGroupSchemeCat: the corresponding full subcategory.
• TauCeti.adjointSemisimpleAffineGroupSchemeProperty_iff: the coordinate-Hopf characterization.
• TauCeti.adjointSemisimpleCommHopfAlgCatOpEquivAdjointSemisimpleAffineGroupSchemeCat: the restricted anti-equivalence between the coordinate and scheme models.

References

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

This completes the definition-level interface for adjoint forms in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. Construction of the represented quotient by the center, its adjointness, and the classification of adjoint forms remain downstream.

def TauCeti.adjointSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (SemisimpleAffineGroupSchemeCat k)

The object property selecting adjoint semisimple affine group schemes over a field.

It is transported from the condition that the center defining ideal of the coordinate Hopf algebra is its augmentation ideal. The ambient object is already semisimple by belonging to SemisimpleAffineGroupSchemeCat k.

Equations

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

@[simp]

theorem TauCeti.adjointSemisimpleAffineGroupSchemeProperty_iff {k : Type u} [Field k] (G : SemisimpleAffineGroupSchemeCat k) : adjointSemisimpleAffineGroupSchemeProperty k G ↔ adjointSemisimpleCommHopfAlgProperty k (Opposite.unop ((semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).inverse.obj G))

A semisimple affine group scheme is adjoint exactly when its coordinate Hopf algebra has center defining ideal equal to the augmentation ideal.

instance TauCeti.instIsClosedUnderIsomorphismsSemisimpleAffineGroupSchemeCatAdjointSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] : (adjointSemisimpleAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

Adjointness of semisimple affine group schemes is invariant under isomorphism.

@[reducible, inline]

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

The category of adjoint semisimple affine group schemes over a field.

Equations

• TauCeti.AdjointSemisimpleAffineGroupSchemeCat k = (TauCeti.adjointSemisimpleAffineGroupSchemeProperty k).FullSubcategory

theorem TauCeti.adjointSemisimpleAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] : (adjointSemisimpleAffineGroupSchemeProperty k).inverseImage (semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).functor = (adjointSemisimpleCommHopfAlgProperty k).op

Pulling adjointness on semisimple affine group schemes back along Spec recovers adjointness of semisimple commutative Hopf algebras.

noncomputable def TauCeti.adjointSemisimpleCommHopfAlgCatOpEquivAdjointSemisimpleAffineGroupSchemeCat (k : Type u) [Field k] : (AdjointSemisimpleCommHopfAlgCat k)ᵒᵖ ≌ AdjointSemisimpleAffineGroupSchemeCat k

Spec restricts to an anti-equivalence from adjoint semisimple finite-type commutative Hopf algebras to adjoint semisimple affine group schemes.

Equations

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

noncomputable def TauCeti.adjointSemisimpleCommHopfAlgCatOpEquivAdjointSemisimpleAffineGroupSchemeCat.functorCompιIso (k : Type u) [Field k] : (adjointSemisimpleCommHopfAlgCatOpEquivAdjointSemisimpleAffineGroupSchemeCat k).functor.comp (adjointSemisimpleAffineGroupSchemeProperty k).ι ≅ (CategoryTheory.forget₂ (AdjointSemisimpleCommHopfAlgCat k) (SemisimpleCommHopfAlgCat k)).op.comp (semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).functor

After forgetting adjointness, the restricted anti-equivalence is the existing semisimple Hopf/group-scheme anti-equivalence.

Equations

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