Algebraically closed points of faithfully flat algebras

Let K be an algebraically closed field over a commutative ring k, and let f : A →ₐ[k] B be faithfully flat and of finite type. Every K-point of A lifts to a K-point of B.

Faithful flatness first gives a prime of B over the kernel of the prescribed point. The affine Nullstellensatz then gives a K-point of B whose kernel contains that prime. Its restriction to A agrees with the prescribed point. This last step is carried out in the fiber over the prescribed point, which is a nontrivial finite-type K-algebra and therefore has a K-point.

Main declarations

• AlgHom.exists_comp_eq_of_comap_eq_ker: a point lifts when its kernel lies in the spectral image of a finite-type map.
• AlgHom.surjective_comp_right_of_comap_surjective: a map surjective on prime spectra is surjective on algebraically closed points when the map is of finite type.
• AlgHom.surjective_comp_right_of_faithfullyFlat: precomposition along a faithfully flat map of finite type is surjective on algebraically closed points.

References

• The Stacks Project, Tag 00HQ, Lemma 10.39.16.
• The Stacks Project, Tag 00FV, Hilbert Nullstellensatz.

This is the algebraically-closed-point lifting prerequisite for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. It is the pointwise bridge needed to transfer unipotence from a finite-type affine group onto the scheme-theoretic image of a faithfully flat group morphism.

theorem AlgHom.exists_comp_eq_of_comap_eq_ker {k : Type u} {A : Type v} {B : Type w} {K : Type x} [CommRing k] [CommRing A] [Algebra k A] [CommRing B] [Algebra k B] [Field K] [Algebra k K] [IsAlgClosed K] (f : A →ₐ[k] B) (hft : f.FiniteType) (p : A →ₐ[k] K) (P : PrimeSpectrum B) (hP : PrimeSpectrum.comap f.toRingHom P = { asIdeal := RingHom.ker p.toRingHom, isPrime := ⋯ }) : ∃ (q : B →ₐ[k] K), q.comp f = p

A point of A lifts through f if a prime of B lies over its kernel.

theorem AlgHom.surjective_comp_right_of_comap_surjective {k : Type u} {A : Type v} {B : Type w} {K : Type x} [CommRing k] [CommRing A] [Algebra k A] [CommRing B] [Algebra k B] [Field K] [Algebra k K] [IsAlgClosed K] (f : A →ₐ[k] B) (hft : f.FiniteType) (hf : Function.Surjective (PrimeSpectrum.comap f.toRingHom)) : Function.Surjective fun (q : B →ₐ[k] K) => q.comp f

Precomposition is surjective on algebraically closed points when the underlying map is of finite type and surjective on prime spectra.

theorem AlgHom.surjective_comp_right_of_faithfullyFlat {k : Type u} {A : Type v} {B : Type w} {K : Type x} [CommRing k] [CommRing A] [Algebra k A] [CommRing B] [Algebra k B] [Field K] [Algebra k K] [IsAlgClosed K] (f : A →ₐ[k] B) (hft : f.FiniteType) (hf : f.FaithfullyFlat) : Function.Surjective fun (q : B →ₐ[k] K) => q.comp f

Precomposition along a faithfully flat morphism is surjective on points valued in an algebraically closed field over the base ring, provided the morphism is of finite type.

In scheme language, a faithfully flat morphism of finite type Spec B ⟶ Spec A is surjective on K-points for every algebraically closed field K with a k-algebra structure.