Geometric connectedness of affine group schemes

This file compares geometric connectedness of a commutative Hopf algebra with Mathlib's scheme-theoretic GeometricallyConnected predicate on its Hopf spectrum.

Main declarations

• TauCeti.geometricallyConnectedAffineGroupSchemeProperty: geometric connectedness of the structural morphism as an object property on affine group schemes.
• TauCeti.geometricallyConnectedCommHopfAlg_iff_geometricallyConnected_hopfSpec: compatibility of the coordinate-ring and scheme-theoretic predicates.
• TauCeti.geometricallyConnected_iff_geometricallyConnected_coordinate: geometric connectedness of a finite-type affine group scheme in terms of its coordinate algebra.
• TauCeti.geometricallyConnected_hopfSpec_iff_idempotent_eq_zero_or_one: the idempotent characterization of geometric connectedness for a Hopf spectrum.

References

• J. S. Milne, Algebraic Groups (2017), §2.a.

This is the geometric-connectedness prerequisite for Layer 3, "Identity component and component group", of the ReductiveGroups roadmap.

def TauCeti.geometricallyConnectedAffineGroupSchemeProperty (S : CommRingCat) : CategoryTheory.ObjectProperty (AffineGroupSchemeCat S)

The object property on affine group schemes selecting those whose structural morphism is geometrically connected.

Equations

• TauCeti.geometricallyConnectedAffineGroupSchemeProperty S G = AlgebraicGeometry.GeometricallyConnected G.obj.X.hom

@[simp]

theorem TauCeti.geometricallyConnectedAffineGroupSchemeProperty_iff (S : CommRingCat) (G : AffineGroupSchemeCat S) : geometricallyConnectedAffineGroupSchemeProperty S G ↔ AlgebraicGeometry.GeometricallyConnected G.obj.X.hom

Membership in the geometrically connected affine-group-scheme object property.

instance TauCeti.instIsClosedUnderIsomorphismsAffineGroupSchemeCatGeometricallyConnectedAffineGroupSchemeProperty (S : CommRingCat) : (geometricallyConnectedAffineGroupSchemeProperty S).IsClosedUnderIsomorphisms

Geometric connectedness of the structural morphism is invariant under isomorphism of affine group schemes.

theorem TauCeti.geometricallyConnectedCommHopfAlg_iff_geometricallyConnected_hopfSpec (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty k H ↔ AlgebraicGeometry.GeometricallyConnected ((AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H)).X.hom

Geometric connectedness agrees across the affine-group-scheme and coordinate-ring models. The structural morphism of a Hopf spectrum is geometrically connected if and only if its coordinate algebra is geometrically connected after every field extension.

theorem TauCeti.geometricallyConnectedAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] : (geometricallyConnectedAffineGroupSchemeProperty ↧k).inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧k).functor = (geometricallyConnectedCommHopfAlgProperty k).op

Under the affine Hopf/group-scheme anti-equivalence, the inverse image of geometric connectedness on affine group schemes is geometric connectedness of coordinate Hopf algebras.

theorem TauCeti.geometricallyConnected_iff_geometricallyConnected_coordinate (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) : AlgebraicGeometry.GeometricallyConnected G.obj.obj.X.hom ↔ geometricallyConnectedCommHopfAlgProperty k (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G)).obj

A finite-type affine group scheme has geometrically connected structural morphism exactly when its coordinate algebra supplied by the affine anti-equivalence is geometrically connected.

theorem TauCeti.geometricallyConnected_hopfSpec_iff_idempotent_eq_zero_or_one (k : Type u) [Field k] (H : CommHopfAlgCat k) : AlgebraicGeometry.GeometricallyConnected ((AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H)).X.hom ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] (e : TensorProduct k (↑H) K), IsIdempotentElem e → e = 0 ∨ e = 1

The structural morphism of a Hopf spectrum is geometrically connected exactly when, after every extension K / k of the base field, every idempotent of H ⊗[k] K is zero or one.