A global form of Zariski's main theorem

Mathlib's algebraic Zariski main theorem (Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective) is local: at a prime p of a finite type R-algebra A that is quasi-finite at p, it produces a module-finite subalgebra A' and some r ∉ p in A' with A'[1/r] = A[1/r]. When A is quasi-finite at every prime, finitely many such basic opens cover Spec A, and the subalgebras can be merged into one. This file records the resulting statement, in the form in which it is used to reduce questions about quasi-finite algebras to finite ones: a single module-finite subalgebra A' and finitely many elements r ∈ A' generating the unit ideal of A, such that every element of A is moved into A' by a large enough power of each r.

Main results

• Algebra.QuasiFinite.exists_fg_subalgebra_and_span_eq_top: the global form of Zariski's main theorem for a quasi-finite algebra of finite type.

References

• Stacks Project, Tag 00Q9, Zariski's main theorem.

theorem Algebra.QuasiFinite.exists_fg_subalgebra_and_span_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FiniteType R A] [QuasiFinite R A] : ∃ (A' : Subalgebra R A) (s : Finset A), (Subalgebra.toSubmodule A').FG ∧ ↑s ⊆ ↑A' ∧ Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, ∀ (x : A), ∀ᶠ (m : ℕ) in Filter.atTop, r ^ m * x ∈ A'

Zariski's main theorem, global form. A quasi-finite algebra A of finite type over R has a module-finite subalgebra A' and finitely many elements r ∈ A' generating the unit ideal of A, such that for every x ∈ A and every such r, all large enough powers of r move x into A'. Geometrically, Spec A is covered by finitely many basic opens D(r) on which it agrees with the finite R-scheme Spec A'.