theorem
Proposition39_g159.proposition_39_codim2_extension
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsNoetherianRing A]
[IsIntegrallyClosed A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(I : Ideal A)
(hI : 2 ≤ I.height)
(x : K)
(hx : ∀ (p : PrimeSpectrum A), ¬I ≤ p.asIdeal → x ∈ Localization.subalgebra.ofField K p.asIdeal.primeCompl ⋯)
:
Proposition 39 (codimension-2 extension): if A is a Noetherian normal domain with
fraction field K, I is an ideal of height at least 2, and x ∈ K lies in the
localisation A_p at every prime p not containing I, then x ∈ A.
theorem
Proposition39_g159.proposition_39_range
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsNoetherianRing A]
[IsIntegrallyClosed A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(I : Ideal A)
(hI : 2 ≤ I.height)
:
Set.range ⇑(algebraMap A K) = ⋂ (p : PrimeSpectrum A), ⋂ (_ : ¬I ≤ p.asIdeal), ↑(Localization.subalgebra.ofField K p.asIdeal.primeCompl ⋯)
Reformulation of Proposition 39 as an intersection: the image of A inside K equals
the intersection of all localisations at primes not containing I, whenever I has
height at least 2.