Connectedness over an algebraically closed field

A connected algebra over an algebraically closed field remains connected after any extension of that field. No finite-type or reducedness assumption on the connected algebra is needed.

Thus ordinary connectedness of an affine scheme over an algebraically closed field implies geometric connectedness. In particular, this applies to identity components of affine groups.

References

• The Stacks Project, Section 10.48, Geometrically connected algebras, https://stacks.math.columbia.edu/tag/05DV.

theorem TauCeti.exists_eq_tmul_one_of_isIdempotentElem {k : Type u_1} {A : Type u_2} {B : Type u_3} [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A] [ConnectedSpace (PrimeSpectrum A)] [CommRing B] [Algebra k B] [Algebra.FiniteType k B] [IsReduced B] {e : TensorProduct k B A} (he : IsIdempotentElem e) : ∃ (c : B), e = c ⊗ₜ[k] 1

An idempotent in a family over a reduced finite-type parameter algebra is scalar when the other factor has connected spectrum and the ground field is algebraically closed.

theorem TauCeti.connectedSpace_primeSpectrum_tensorProduct_of_isAlgClosed (k : Type u_1) (A : Type u_2) (K : Type u_3) [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A] [ConnectedSpace (PrimeSpectrum A)] [Field K] [Algebra k K] : ConnectedSpace (PrimeSpectrum (TensorProduct k A K))

A connected algebra over an algebraically closed field remains connected after every field extension, without finite-type or reducedness assumptions.