Testing geometric connectedness over algebraically closed fields

For a commutative Hopf algebra H over a field k, geometric connectedness may be tested only after algebraically closed extensions of k. For an arbitrary extension K / k, its algebraic closure Ω is again a k-algebra. The map

H ⊗[k] K → H ⊗[k] Ω

is injective because H is flat over the field k. Connectedness of the target therefore descends to the source by the idempotent characterization of connected affine spectra.

Over an algebraically closed ground field, ordinary connectedness is already geometric connectedness; no finite-type hypothesis is required.

Main declarations

• TauCeti.geometricallyConnectedCommHopfAlgProperty_iff_connectedSpace: over an algebraically closed field, geometric connectedness is equivalent to ordinary connectedness.
• TauCeti.geometricallyConnectedCommHopfAlgProperty_iff_connectedSpace_of_isAlgClosed: geometric connectedness is equivalent to connectedness after every algebraically closed field extension.
• TauCeti.HopfAlgebra.rightTranslationAlgHom_eq_self_of_path: a domain-valued path from the identity to a point makes that point's translation fix every idempotent.
• TauCeti.HopfAlgebra.connectedSpace_primeSpectrum_of_forall_rightTranslationAlgHom_eq_self: if every point translation fixes every idempotent, the spectrum is connected.

References

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

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty_iff_connectedSpace_of_isAlgClosed (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty k H ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] [IsAlgClosed K], ConnectedSpace (PrimeSpectrum (TensorProduct k (↑H) K))

Geometric connectedness of a commutative Hopf algebra can be tested after algebraically closed field extensions.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty_iff_connectedSpace (k : Type u) [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty k H ↔ ConnectedSpace (PrimeSpectrum ↑H)

Over an algebraically closed field, a commutative Hopf algebra is geometrically connected exactly when its prime spectrum is connected. No finite-type assumption is needed.

theorem TauCeti.HopfAlgebra.rightTranslationAlgHom_eq_self_of_path {K H D : Type u} [Field K] [CommRing H] [HopfAlgebra K H] [Algebra.FiniteType K H] [CommRing D] [Algebra K D] [IsDomain D] [IsAlgClosed K] (e : H) (he : IsIdempotentElem e) (g : WithConv (H →ₐ[K] K)) (x : WithConv (H →ₐ[K] D)) (phi psi : D →ₐ[K] K) (hphi : (AlgHom.mapValue phi) x = g) (hpsi : (AlgHom.mapValue psi) x = 1) : (rightTranslationAlgHom g) e = e

If a point of a finite-type Hopf algebra is connected to the identity by a path valued in a domain, its right translation fixes every idempotent.

theorem TauCeti.HopfAlgebra.connectedSpace_primeSpectrum_of_forall_rightTranslationAlgHom_eq_self {K H : Type u} [Field K] [CommRing H] [HopfAlgebra K H] [Algebra.FiniteType K H] [IsAlgClosed K] (htranslate : ∀ (e : H), IsIdempotentElem e → ∀ (g : WithConv (H →ₐ[K] K)), (rightTranslationAlgHom g) e = e) : ConnectedSpace (PrimeSpectrum H)

If right translation by every rational point fixes every idempotent of a finite-type Hopf algebra over an algebraically closed field, its prime spectrum is connected.