Documentation

Mathlib.RingTheory.ZariskisMainTheorem

Algebraic Zariski's Main Theorem #

In this file we will prove (TODO @erdOne) the algebraic version of Zariski's main theorem

The final statement would be

example {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (p : Ideal S) [p.IsPrime] [Algebra.QuasiFiniteAt R p] : ZariskiMainProperty R p

References #

source
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
Instances For
    source
    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)
    source
    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)
    source
    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) ⋯ = ⊤
    source
    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
    source
    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
    source
    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