Simply connected semisimple affine group schemes

A semisimple affine group scheme G over a field is simply connected when every central isogeny G' ⟶ G from another semisimple affine group scheme is an isomorphism. Restricting the source to semisimple affine group schemes is essential: the ambient category of all group schemes also contains nonsmooth finite group schemes, whose structural morphisms to the trivial group are central isogenies without being isomorphisms.

The definition is phrased in SemisimpleAffineGroupSchemeCat, so smoothness, geometric connectedness, affineness, and finite type remain separate structural properties rather than being repeated as hypotheses on every source. It is invariant under isomorphism and therefore cuts out the full subcategory SimplyConnectedSemisimpleAffineGroupSchemeCat.

For a central isogeny, being an isomorphism is equivalent to its underlying scheme morphism being monic. Indeed, an isogeny is finite, flat, and surjective; a flat, quasi-compact, surjective monomorphism of schemes is an isomorphism. This gives the kernel-free characterization simplyConnectedSemisimpleAffineGroupSchemeProperty_iff_forall_mono.

Main declarations

• TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty: simple connectivity for semisimple affine group schemes over a field.
• TauCeti.SimplyConnectedSemisimpleAffineGroupSchemeCat: the corresponding full subcategory.
• TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty_iff_forall_mono: a semisimple affine group scheme is simply connected exactly when every central isogeny onto it has monic underlying scheme morphism.
• TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty_inverseImage: pulling the scheme property back along Spec recovers the coordinate-Hopf property.
• The restricted anti-equivalence between the coordinate and scheme models is simplyConnectedSemisimpleCommHopfAlgCatOpEquivSimplyConnectedSemisimpleAffineGroupSchemeCat.

References

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

This is the simply-connected-form target in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. Central isogenies and semisimple affine group schemes are already available; construction and classification of simply connected covers remain downstream.

@[reducible, inline]

noncomputable abbrev TauCeti.semisimpleAffineGroupSchemeForget (k : Type u) [Field k] : CategoryTheory.Functor (SemisimpleAffineGroupSchemeCat k) (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)))

The forgetful functor from semisimple affine group schemes to group schemes.

Equations

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

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

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

A semisimple affine group scheme G is simply connected when every central isogeny H ⟶ G in the category of semisimple affine group schemes is an isomorphism. The source is required to be semisimple; allowing arbitrary group schemes would incorrectly include nonsmooth finite central covers among the maps tested by the definition.

Equations

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

@[simp]

theorem TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty_iff {k : Type u} [Field k] (G : SemisimpleAffineGroupSchemeCat k) : simplyConnectedSemisimpleAffineGroupSchemeProperty k G ↔ ∀ (H : SemisimpleAffineGroupSchemeCat k) (f : H ⟶ G), GroupScheme.IsCentralIsogeny ((semisimpleAffineGroupSchemeForget k).map f) → CategoryTheory.IsIso f

Membership in the simply connected semisimple affine-group-scheme property means that every central isogeny from a semisimple affine group scheme is an isomorphism.

theorem TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty.isIso {k : Type u} [Field k] {G : SemisimpleAffineGroupSchemeCat k} (hG : simplyConnectedSemisimpleAffineGroupSchemeProperty k G) {H : SemisimpleAffineGroupSchemeCat k} (f : H ⟶ G) (hf : GroupScheme.IsCentralIsogeny ((semisimpleAffineGroupSchemeForget k).map f)) : CategoryTheory.IsIso f

Every central isogeny from a semisimple affine group scheme to a simply connected one is an isomorphism.

theorem TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty.mk {k : Type u} [Field k] {G : SemisimpleAffineGroupSchemeCat k} (hG : ∀ (H : SemisimpleAffineGroupSchemeCat k) (f : H ⟶ G), GroupScheme.IsCentralIsogeny ((semisimpleAffineGroupSchemeForget k).map f) → CategoryTheory.IsIso f) : simplyConnectedSemisimpleAffineGroupSchemeProperty k G

Establish simple connectivity by proving that every central isogeny onto the group is an isomorphism.

instance TauCeti.instIsClosedUnderIsomorphismsSemisimpleAffineGroupSchemeCatSimplyConnectedSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] : (simplyConnectedSemisimpleAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

Simple connectivity of semisimple affine group schemes is invariant under isomorphism.

@[reducible, inline]

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

The category of simply connected semisimple affine group schemes over a field.

Equations

• TauCeti.SimplyConnectedSemisimpleAffineGroupSchemeCat k = (TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty k).FullSubcategory

theorem TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty_iff_forall_mono {k : Type u} [Field k] (G : SemisimpleAffineGroupSchemeCat k) : simplyConnectedSemisimpleAffineGroupSchemeProperty k G ↔ ∀ (H : SemisimpleAffineGroupSchemeCat k) (f : H ⟶ G), GroupScheme.IsCentralIsogeny ((semisimpleAffineGroupSchemeForget k).map f) → CategoryTheory.Mono (CategoryTheory.Over.Hom.left ((semisimpleAffineGroupSchemeForget k).map f).hom.hom)

A semisimple affine group scheme is simply connected exactly when the underlying scheme map of every central isogeny onto it is a monomorphism.

theorem TauCeti.semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat.isCentralIsogeny_map_iff {k : Type u} [Field k] {H K : (SemisimpleCommHopfAlgCat k)ᵒᵖ} (f : H ⟶ K) : GroupScheme.IsCentralIsogeny ((semisimpleAffineGroupSchemeForget k).map ((semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).functor.map f)) ↔ CommHopfAlgCat.IsCentralIsogeny f.unop.hom.hom

Under the semisimple Hopf/group-scheme anti-equivalence, a morphism is a coordinate central isogeny exactly when its image is a group-scheme central isogeny.

theorem TauCeti.simplyConnectedSemisimpleAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] : (simplyConnectedSemisimpleAffineGroupSchemeProperty k).inverseImage (semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).functor = (simplyConnectedSemisimpleCommHopfAlgProperty k).op

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

noncomputable def TauCeti.simplyConnectedSemisimpleCommHopfAlgCatOpEquivSimplyConnectedSemisimpleAffineGroupSchemeCat (k : Type u) [Field k] : (SimplyConnectedSemisimpleCommHopfAlgCat k)ᵒᵖ ≌ SimplyConnectedSemisimpleAffineGroupSchemeCat k

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

Equations

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

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

After forgetting simple connectivity, 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.