Closed points of an affine scheme over an algebraically closed field

For a finite-type algebra over an algebraically closed field, the closed points of its spectrum are exactly the kernels of algebra homomorphisms to the base field. This affine form of the weak Nullstellensatz connects the augmentation-point API to closed-point arguments on schemes. It includes nonreduced algebras.

The construction uses Zariski's lemma finite_of_finite_type_of_isJacobsonRing and IsAlgClosed.algebraMap_bijective_of_isIntegral.

References

• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Chapter 4.

@[simp]

theorem AlgHom.isClosed_singleton_kernelPoint {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (f : A →ₐ[k] k) : IsClosed {TauCeti.AlgHom.kernelPoint f}

The spectrum point defined by a base-field-valued algebra homomorphism is closed, without a finite-type assumption.

theorem PrimeSpectrum.exists_kernelPoint_eq_of_isClosed {k : Type u_1} {A : Type u_2} [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] (x : PrimeSpectrum A) (hx : IsClosed {x}) : ∃ (f : A →ₐ[k] k), TauCeti.AlgHom.kernelPoint f = x

Every closed point of a finite-type algebra over an algebraically closed field is the kernel point of a base-field-valued algebra homomorphism.

theorem TauCeti.range_kernelPoint_eq_closedPoints {k : Type u_1} {A : Type u_2} [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] : Set.range AlgHom.kernelPoint = closedPoints ↥(AlgebraicGeometry.Spec ↧A)

Rational augmentation points are exactly the closed points of a finite-type affine scheme over an algebraically closed field.