Simply connected semisimple affine groups in Hopf coordinates

A semisimple affine group over a field is simply connected when every central isogeny onto it is an isomorphism. In coordinate Hopf algebras the arrows reverse: a central isogeny onto the group represented by H is a finite faithfully flat morphism H ⟶ K, and simple connectivity says that every such morphism to a semisimple coordinate algebra K is an isomorphism.

The source and target of the isogenies are required to be semisimple. Allowing arbitrary affine group schemes would make the definition test central isogenies from nonsmooth finite group schemes, which is not the standard notion for semisimple algebraic groups.

This coordinate-Hopf interface is adapted from the scheme-side formalization in TauCeti.AlgebraicGeometry.AffineGroupScheme.SimplyConnected.

Because a faithfully flat coordinate morphism is injective, the only missing half of bijectivity is surjectivity. Thus simplyConnectedSemisimpleCommHopfAlgProperty_iff_forall_surjective gives the characteristic coordinate criterion: a semisimple group is simply connected exactly when every central-isogeny coordinate map out of it is surjective.

Main declarations

• TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty: simple connectivity for semisimple finite-type commutative Hopf algebras.
• TauCeti.SimplyConnectedSemisimpleCommHopfAlgCat: the corresponding full subcategory.
• TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty_iff_forall_surjective: the coordinate surjectivity criterion.

References

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

This supplies the coordinate-Hopf form of the simply-connected-form target in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. Construction of simply connected covers and their relation to root data remain downstream.

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

The object property selecting simply connected semisimple affine groups in Hopf coordinates.

For a semisimple coordinate Hopf algebra H, arrows reverse under Spec, so the central isogenies onto the represented group are precisely the coordinate morphisms H ⟶ K tested here. Requiring K to be semisimple is part of the standard definition.

Equations

• TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty k H = ∀ (K : TauCeti.SemisimpleCommHopfAlgCat k) (f : H ⟶ K), TauCeti.CommHopfAlgCat.IsCentralIsogeny f.hom.hom → CategoryTheory.IsIso f

@[simp]

theorem TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty_iff {k : Type u} [Field k] (H : SemisimpleCommHopfAlgCat k) : simplyConnectedSemisimpleCommHopfAlgProperty k H ↔ ∀ (K : SemisimpleCommHopfAlgCat k) (f : H ⟶ K), CommHopfAlgCat.IsCentralIsogeny f.hom.hom → CategoryTheory.IsIso f

Membership in the simply connected property means that every coordinate central isogeny out of the Hopf algebra and into another semisimple coordinate Hopf algebra is an isomorphism.

theorem TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty.isIso {k : Type u} [Field k] {H : SemisimpleCommHopfAlgCat k} (hH : simplyConnectedSemisimpleCommHopfAlgProperty k H) {K : SemisimpleCommHopfAlgCat k} (f : H ⟶ K) (hf : CommHopfAlgCat.IsCentralIsogeny f.hom.hom) : CategoryTheory.IsIso f

Every coordinate central isogeny out of a simply connected semisimple group is an isomorphism.

theorem TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty.mk {k : Type u} [Field k] {H : SemisimpleCommHopfAlgCat k} (hH : ∀ (K : SemisimpleCommHopfAlgCat k) (f : H ⟶ K), CommHopfAlgCat.IsCentralIsogeny f.hom.hom → CategoryTheory.IsIso f) : simplyConnectedSemisimpleCommHopfAlgProperty k H

Establish simple connectivity by proving that every coordinate central isogeny out of the group is an isomorphism.

theorem TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty.surjective {k : Type u} [Field k] {H : SemisimpleCommHopfAlgCat k} (hH : simplyConnectedSemisimpleCommHopfAlgProperty k H) {K : SemisimpleCommHopfAlgCat k} (f : H ⟶ K) (hf : CommHopfAlgCat.IsCentralIsogeny f.hom.hom) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.hom)

The coordinate map of every central isogeny out of a simply connected semisimple group is surjective.

theorem TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty_iff_forall_surjective {k : Type u} [Field k] (H : SemisimpleCommHopfAlgCat k) : simplyConnectedSemisimpleCommHopfAlgProperty k H ↔ ∀ (K : SemisimpleCommHopfAlgCat k) (f : H ⟶ K), CommHopfAlgCat.IsCentralIsogeny f.hom.hom → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.hom)

A semisimple affine group is simply connected exactly when every coordinate central isogeny out of its Hopf algebra is surjective.

Injectivity is automatic from faithful flatness, so surjectivity makes the coordinate morphism bijective and hence an isomorphism.

instance TauCeti.instIsClosedUnderIsomorphismsSemisimpleCommHopfAlgCatSimplyConnectedSemisimpleCommHopfAlgProperty (k : Type u) [Field k] : (simplyConnectedSemisimpleCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Simple connectivity in Hopf coordinates is invariant under isomorphism.

@[reducible, inline]

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

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

Equations

• TauCeti.SimplyConnectedSemisimpleCommHopfAlgCat k = (TauCeti.simplyConnectedSemisimpleCommHopfAlgProperty k).FullSubcategory