Algebraic Zariski's Main Theorem

The statement of Zariski's main theorem is the following: Given a finite type R-algebra S, and p a prime of S such that S is quasi-finite at R, then there exists a f ∉ p such that S[1/f] is isomorphic to R'[1/f] where R' is the integral closure of R in S.

We follow https://stacks.math.columbia.edu/tag/00PI and proceed in the following steps

1. Algebra.ZariskisMainProperty.of_adjoin_eq_top: The case where S = R[X]/I. The key is Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt which shows that there exists some g ∈ I such that some coefficient gᵢ ∉ p. Then one basically takes f = gᵢ and g becomes monic in R[1/gᵢ][X] up to some minor technical issues, and then S[1/gᵢ] is basically integral over R[1/gᵢ].
2. Algebra.ZariskisMainProperty.of_algHom_polynomial: The case where S is finite over R⟨x⟩ for some x : S. The following key results are first esablished:

• isStronglyTranscendental_mk_radical_conductor: Let 𝔣 be the conductor of x (i.e. the largest S-ideal in R⟨x⟩). x as an element of S/√𝔣 is strongly transcendental over R.
• Algebra.not_quasiFiniteAt_of_stronglyTranscendental: If S is reduced, then x : S is not strongly transcendental over R. One first reduces to when R ⊆ S are domains, and then to when R is integrally closed. A going down theorem is now available, which could be applied to Polynomial.map_under_lt_comap_of_quasiFiniteAt:(p ∩ R)[X] < p ∩ R<x> to get a contradiction. The second result applied to S/√𝔣 together with the first result implies that p does not contain 𝔣. The claim then follows from Localization.localRingHom_bijective_of_not_conductor_le.

3. Algebra.ZariskisMainProperty.of_algHom_mvPolynomial: The case where S is finite over R⟨x₁,...,xₙ⟩. This is proved using induction on n.

Main definiton and results

• Algebra.ZariskisMainProperty: We say that an R algebra S satisfies the Zariski's main property at a prime p of S if there exists r ∉ p in the integral closure S' of R in S, such that S'[1/r] = S[1/r].
• Algebra.ZariskisMainProperty.of_finiteType: If S is finite type over R and quasi-finite at p, then ZariskisMainProperty holds.
• Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective: If S is finite type over R and quasi-finite at p, then there exists a subalgebra S' of R that is finitely generated as an R-module, and some r ∈ S' such that r ∉ p and S'[1/r] = S[1/r].

def Algebra.ZariskisMainProperty (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) : Prop

We say that an R algebra S satisfies the Zariski's main property at a prime p of S if there exists r ∉ p in the integral closure S' of R in S, such that S'[1/r] = S[1/r].

Equations

• Algebra.ZariskisMainProperty R p = ∃ (r : ↥(integralClosure R S)), ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom r)

theorem Algebra.zariskisMainProperty_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} : ZariskisMainProperty R p ↔ ∃ r ∉ p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

theorem Algebra.zariskisMainProperty_iff' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} : ZariskisMainProperty R p ↔ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

theorem Algebra.zariskisMainProperty_iff_exists_saturation_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} : ZariskisMainProperty R p ↔ ∃ r ∉ p, ∃ (h : IsIntegral R r), (integralClosure R S).saturation (Submonoid.powers r) ⋯ = ⊤

theorem Algebra.ZariskisMainProperty.restrictScalars {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IsIntegral R S] {p : Ideal T} (H : ZariskisMainProperty S p) : ZariskisMainProperty R p

theorem Algebra.ZariskisMainProperty.trans {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (p : Ideal T) [p.IsPrime] (h₁ : ZariskisMainProperty R (Ideal.under S p)) (h₂ : ∃ r ∉ Ideal.under S p, ⊥.saturation (Submonoid.powers ((algebraMap S T) r)) ⋯ = ⊤) : ZariskisMainProperty R p

theorem Algebra.ZariskisMainProperty.of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) [p.IsPrime] [Algebra.IsIntegral R S] : ZariskisMainProperty R p

theorem isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : Polynomial R →ₐ[R] S) (t : S) (p r : Polynomial R) (ht : φ.IsIntegralElem t) (hpm : p.Monic) (hpr : r.natDegree < p.natDegree) (hp : φ p * t = φ r) : IsIntegral R t

Given a map φ : R[X] →ₐ[R] S. Suppose t = φ r / φ p is integral over R[X] where p is monic with deg p > deg r, then t is also integral over R.

theorem exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R) (ht : φ.IsIntegralElem t) (hpm : p.Monic) (hp : φ p * t ∈ φ.range) : ∃ (q : Polynomial R), IsIntegral R (t - φ q)

Stacks Tag 00PT

theorem exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R) (ht : φ.IsIntegralElem t) (hp : φ p * t ∈ φ.range) : ∃ (q : Polynomial R) (n : ℕ), IsIntegral R (p.leadingCoeff ^ n • t - φ q)

Stacks Tag 00PV

theorem exists_leadingCoeff_pow_smul_mem_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R) (hRS : integralClosure R S = ⊥) (hφ : φ.Finite) (hp : φ p * t ∈ conductor R (φ Polynomial.X)) : ∃ (n : ℕ), p.leadingCoeff ^ n • t ∈ conductor R (φ Polynomial.X)

Stacks Tag 00PX

theorem exists_leadingCoeff_pow_smul_mem_radical_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R) (hRS : integralClosure R S = ⊥) (hφ : φ.Finite) (hp : φ p * t ∈ (conductor R (φ Polynomial.X)).radical) (i : ℕ) : p.coeff i • t ∈ (conductor R (φ Polynomial.X)).radical

Stacks Tag 00PY

theorem isStronglyTranscendental_mk_radical_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (hRS : integralClosure R S = ⊥) (x : S) (hx : (Polynomial.aeval x).Finite) : IsStronglyTranscendental R ((Ideal.Quotient.mk (conductor R x).radical) x)

Stacks Tag 00PY

theorem Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsReduced S] {x : S} (hx' : (Polynomial.aeval x).Finite) (P : Ideal S) [P.IsPrime] [WeaklyQuasiFiniteAt R P] : ¬IsStronglyTranscendental R x

theorem Algebra.not_isStronglyTranscendental_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsReduced S] {x : S} (hx' : (Polynomial.aeval x).Finite) (P : Ideal S) [P.IsPrime] [QuasiFiniteAt R P] : ¬IsStronglyTranscendental R x

Stacks Tag 00Q2

theorem Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) [p.IsPrime] [WeaklyQuasiFiniteAt R p] : ZariskisMainProperty R p

Stacks Tag 00Q9

theorem Algebra.ZariskisMainProperty.of_finiteType {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) [p.IsPrime] [QuasiFiniteAt R p] : ZariskisMainProperty R p

The algebraic version of Zariski's Main Theorem: Given a finite type R-algebra S that is quasi-finite at a prime p, there exists a f ∉ p such that S[1/f] is isomorphic to R'[1/f] where R' is the integral closure of R in S.

theorem Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) (H : ZariskisMainProperty R p) : ∃ (S' : Subalgebra R S), (Subalgebra.toSubmodule S').FG ∧ ∃ (r : ↥S'), ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)

theorem Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) [p.IsPrime] [WeaklyQuasiFiniteAt R p] : ∃ (S' : Subalgebra R S), (Subalgebra.toSubmodule S').FG ∧ ∃ (r : ↥S'), ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)

theorem Algebra.ZariskisMainProperty.quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) [p.IsPrime] (H : ZariskisMainProperty R p) : QuasiFiniteAt R p

theorem Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal S) [p.IsPrime] [WeaklyQuasiFiniteAt R p] : QuasiFiniteAt R p