Separation by algebraically closed points

Let A be a commutative algebra of finite type over a field k, and let K be an algebraically closed extension of k. An element of A vanishes under every k-algebra homomorphism A →ₐ[k] K exactly when it is nilpotent. In particular, when A is reduced, its K-valued points separate elements of A.

The proof is the weak Nullstellensatz in intrinsic form. A finite-type algebra over a field is a Jacobson ring, so a non-nilpotent element is avoided by some maximal ideal. The residue field at that ideal is finite over k by Zariski's lemma and therefore embeds into K.

Main declarations

• TauCeti.exists_algHom_apply_ne_zero_of_notMem_radical: an element outside the radical of an ideal is nonzero at some algebraically closed point annihilating the ideal.
• TauCeti.mem_radical_iff_forall_algHom_apply_eq_zero: the intrinsic affine Nullstellensatz for finite-type algebras.
• TauCeti.exists_algHom_apply_ne_zero_of_not_isNilpotent: a non-nilpotent element is nonzero at some algebraically closed point.
• TauCeti.forall_algHom_apply_eq_zero_iff_isNilpotent: the common kernel of all algebraically closed points is the nilradical.
• TauCeti.eq_one_of_isIdempotentElem_of_forall_algHom_apply_eq_one: an idempotent evaluating to one at every algebraically closed point is one.
• TauCeti.eq_of_isIdempotentElem_of_forall_algHom_apply_eq: two idempotents that agree at every algebraically closed point are equal.
• TauCeti.exists_algHom_apply_ne_of_ne: points of a reduced finite-type algebra distinguish distinct elements.
• TauCeti.eq_of_forall_algHom_apply_eq: the corresponding point-separation principle.

References

• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Chapter 4.
• The Stacks Project, Tag 00FV, Hilbert Nullstellensatz.

This is the reduced finite-type point-separation prerequisite for Layer 5, "Unipotent groups", of TauCetiRoadmap/ReductiveGroups/README.md. It turns pointwise identities over an algebraic closure into identities in a smooth affine group's coordinate algebra.

theorem TauCeti.exists_algHom_apply_ne_zero_of_notMem_radical {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] (I : Ideal A) {x : A} (hx : x ∉ I.radical) : ∃ (f : A →ₐ[k] K), I ≤ RingHom.ker f.toRingHom ∧ f x ≠ 0

An element outside the radical of an ideal in a finite-type algebra over a field is nonzero at some algebraically closed point annihilating that ideal.

theorem TauCeti.mem_radical_iff_forall_algHom_apply_eq_zero {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] (I : Ideal A) (x : A) : x ∈ I.radical ↔ ∀ (f : A →ₐ[k] K), I ≤ RingHom.ker f.toRingHom → f x = 0

The intrinsic affine Nullstellensatz for a finite-type algebra over a field: an element lies in the radical of an ideal exactly when every algebraically closed point annihilating the ideal also annihilates the element.

theorem TauCeti.exists_algHom_apply_ne_zero_of_not_isNilpotent {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] {x : A} (hx : ¬IsNilpotent x) : ∃ (f : A →ₐ[k] K), f x ≠ 0

A non-nilpotent element of a finite-type algebra over a field is nonzero at some point valued in any algebraically closed extension of the ground field.

theorem TauCeti.forall_algHom_apply_eq_zero_iff_isNilpotent {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] (x : A) : (∀ (f : A →ₐ[k] K), f x = 0) ↔ IsNilpotent x

An element of a finite-type algebra over a field vanishes at every point valued in an algebraically closed extension exactly when it is nilpotent. Equivalently, the common kernel of all such points is the nilradical.

theorem TauCeti.eq_one_of_isIdempotentElem_of_forall_algHom_apply_eq_one {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] {a : A} (ha : IsIdempotentElem a) (h : ∀ (f : A →ₐ[k] K), f a = 1) : a = 1

An idempotent in a finite-type algebra that evaluates to one at every algebraically closed point is one.

theorem TauCeti.eq_of_isIdempotentElem_of_forall_algHom_apply_eq {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] {a b : A} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (h : ∀ (f : A →ₐ[k] K), f a = f b) : a = b

Two idempotents in a finite-type algebra are equal when they have the same value at every point valued in an algebraically closed extension of the ground field. No reducedness assumption is needed: idempotents are already insensitive to nilpotents.

theorem TauCeti.exists_algHom_apply_ne_zero_of_ne_zero {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] [IsReduced A] {x : A} (hx : x ≠ 0) : ∃ (f : A →ₐ[k] K), f x ≠ 0

A nonzero element of a reduced finite-type algebra over a field is nonzero at some point valued in any algebraically closed extension of the ground field.

theorem TauCeti.exists_algHom_apply_ne_of_ne {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] [IsReduced A] {x y : A} (hxy : x ≠ y) : ∃ (f : A →ₐ[k] K), f x ≠ f y

Two elements of a reduced finite-type algebra over a field are distinguished by a point valued in any algebraically closed extension whenever they are distinct.

theorem TauCeti.eq_of_forall_algHom_apply_eq {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] [IsReduced A] {x y : A} (h : ∀ (f : A →ₐ[k] K), f x = f y) : x = y

Algebraically closed points separate the elements of a reduced finite-type algebra over a field.

theorem TauCeti.algHom_evaluation_injective {k : Type u} {A : Type v} {K : Type w} [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [Field K] [Algebra k K] [IsAlgClosed K] [IsReduced A] : Function.Injective fun (x : A) (f : A →ₐ[k] K) => f x

Evaluation on all algebraically closed points is injective for a reduced finite-type algebra over a field.