Theorems · Theorem · algebraic geometry

Algebra.ZariskisMainProperty.of_finiteType

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.QuasiFiniteAt R p], Algebra.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.

Defined in

Mathlib.RingTheory.ZariskisMainTheorem

Cited by

3 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.FiniteTypeIdeal.IsPrimeAlgebra.QuasiFiniteAt