Stacks Project, Section 58.32, defines NF by considering every ordered finite algebra-generating family, taking its longest integral prefix, and minimizing the number of remaining generators. This file constructs that literal minimum and proves that it vanishes precisely for a finite algebra.
The algebra structure records the original map φ; integrality uses its actual coefficient map. The auxiliary quotient map τ does not occur in this numerical definition. The construction works for any finite-type commutative algebra, hence for the original étale map, and allows the zero ring and empty generating families. It does not assert the subsequent positive-characteristic coordinate-modification lemma.
Source: https://stacks.math.columbia.edu/tag/0G1E
The largest length of an integral prefix in the displayed ordered family.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]def integralPrefixLength {r : ℕ} (y : Fin r → C) : ℕThe chosen prefix never exceeds the length of the family.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]theorem integralPrefixLength_le {r : ℕ} (y : Fin r → C) :
integralPrefixLength R y ≤ rEvery element in the chosen prefix is integral over the original base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]theorem integralPrefixLength_spec {r : ℕ} (y : Fin r → C) :
∀ i : Fin r, i.val < integralPrefixLength R y → IsIntegral R (y i)Any integral prefix is no longer than the constructed largest prefix.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]theorem le_integralPrefixLength {r : ℕ} (y : Fin r → C) {s : ℕ}
(hs : s ≤ r) (hy : ∀ i : Fin r, i.val < s → IsIntegral R (y i)) :
s ≤ integralPrefixLength R yThe prefix has full length exactly when all displayed generators are integral.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]theorem integralPrefixLength_eq_iff {r : ℕ} (y : Fin r → C) :
integralPrefixLength R y = r ↔ ∀ i : Fin r, IsIntegral R (y i)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem exists_ordered_algebra_generators [Algebra.FiniteType R C] :
∃ (r : ℕ) (y : Fin r → C), Algebra.adjoin R (Set.range y) = ⊤Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem exists_nonfinite_generator_count [Algebra.FiniteType R C] :
∃ d : ℕ, ∃ (r : ℕ) (y : Fin r → C),
Algebra.adjoin R (Set.range y) = ⊤ ∧ r - integralPrefixLength R y = dThe invariant NF of Stacks 58.32: the minimum, over all ordered finite algebra-generating families, of their length minus their longest integral prefix.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)def nonfiniteGeneratorCount [Algebra.FiniteType R C] : ℕThe minimum is attained by an actual ordered algebra-generating family.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem nonfiniteGeneratorCount_spec [Algebra.FiniteType R C] :
∃ (r : ℕ) (y : Fin r → C), Algebra.adjoin R (Set.range y) = ⊤ ∧
r - integralPrefixLength R y = nonfiniteGeneratorCount R CEvery displayed generating family bounds the minimum from above.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem nonfiniteGeneratorCount_le [Algebra.FiniteType R C]
{r : ℕ} (y : Fin r → C) (hy : Algebra.adjoin R (Set.range y) = ⊤) :
nonfiniteGeneratorCount R C ≤ r - integralPrefixLength R yA known integral prefix, even before computing the longest one, bounds NF. This is the bound used after modifying the polynomial coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem nonfiniteGeneratorCount_le_of_prefix [Algebra.FiniteType R C]
{r s : ℕ} (y : Fin r → C) (hy : Algebra.adjoin R (Set.range y) = ⊤)
(hs : s ≤ r) (hint : ∀ i : Fin r, i.val < s → IsIntegral R (y i)) :
nonfiniteGeneratorCount R C ≤ r - sThe original normalization-failure invariant vanishes exactly when the algebra is finite as a module over its base. No nonzero-ring hypothesis is needed.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
variable (C)theorem nonfiniteGeneratorCount_eq_zero_iff [Algebra.FiniteType R C] :
nonfiniteGeneratorCount R C = 0 ↔ Module.Finite R C