The countable Nullstellensatz over ℂ

The classical Nullstellensatz produces a ℂ-point of a nonzero commutative ℂ-algebra of finite type. Deligne's Proposition 4.5 needs a ℂ-point of the algebra over which the fibre functor is defined, and that algebra is not presented as a finite-type one; it is instead built from countably much data, so its dimension as a ℂ-vector space is at most countable. The countable-dimension hypothesis is a perfectly good replacement for the finite-type hypothesis, because the obstruction is uncountable: a field extension of ℂ containing a transcendental element x already contains the ℂ-linearly independent family (x - a)⁻¹, a : ℂ, of cardinality the continuum.

Three results are recorded. A field extension of ℂ of at most countable dimension is algebraic; a nonzero commutative ℂ-algebra of at most countable dimension maps onto ℂ; and an algebra generated by a countable set has at most countable dimension.

The finite-type predecessor is RS.exists_algHom_complex in NullPoint.lean, which runs the same last two steps — quotient by a maximal ideal, lift along IsAlgClosed.lift — over Zariski's lemma instead of the dimension count.

theorem RS.algebraic_of_countable_dimension (K : Type u_1) [Field K] [Algebra ℂ K] (h : Module.rank ℂ K ≤ Cardinal.aleph0) : Algebra.IsAlgebraic ℂ K

A field extension of ℂ of at most countable dimension is algebraic. A transcendental element x would give the ℂ-linearly independent family (x - a)⁻¹ indexed by a : ℂ, forcing the dimension to be at least the continuum.

theorem RS.exists_algHom_of_countable_dimension (R : Type u_1) [CommRing R] [Algebra ℂ R] [Nontrivial R] (h : Module.rank ℂ R ≤ Cardinal.aleph0) : Nonempty (R →ₐ[ℂ] ℂ)

The countable Nullstellensatz: a nonzero commutative ℂ-algebra of at most countable dimension admits a ℂ-point. Quotient by a maximal ideal, observe that the residue field again has at most countable dimension, hence is algebraic over ℂ, and lift along the algebraically closed base.

theorem RS.exists_smul_one_of_countable_dimension (K : Type u_1) [Field K] [Algebra ℂ K] (h : Module.rank ℂ K ≤ Cardinal.aleph0) (x : K) : ∃ (c : ℂ), x = c • 1

A field extension of the complex numbers of countable dimension is the complex numbers: every element is a complex multiple of the unit. This is the shape the scalar computation for a simple algebra consumes.