Critical growth of a finite-dimensional coordinate space

If multiplication by the coordinates enlarges a finite-dimensional space by only one dimension, commutativity forces all coordinates to be affine in one transcendental coordinate over an algebraically closed field.

theorem CCDN.affine_of_critical_growth_of_point {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [IsDomain A] [Algebra K A] (φ : A →ₐ[K] K) (U V : Submodule K A) [Module.Finite K ↥U] [Module.Finite K ↥V] (hUV : U ≤ V) (hUone : 1 ∈ U) (hd : Module.finrank K ↥V = Module.finrank K ↥U + 1) {x y : A} (hx : Transcendental K x) (hxU : ∀ u ∈ U, x * u ∈ V) (hyU : ∀ u ∈ U, y * u ∈ V) : ∃ (c : K) (d : K), y = c • x + (algebraMap K A) d

Critical growth over an arbitrary field, provided that the coordinate ring has a base-field-valued point.