Close-up: base case

Base cases of the close-up construction (Heitmann, Lemma 4). For a principal ideal (a) in a Noetherian local domain T with an A-extension R, one produces a new A-extension containing a/p for suitable primes p. The divisibility case follows by induction on the UFD factorisation in R.

Base case: principal ideals (n = 1)

If I = yR for y prime in R, and c ∈ yT ∩ R, then c ∈ yR already. This follows from the N-subring height condition.

theorem eq_of_prime_le_prime_height_le_one {S : Type u_2} [CommRing S] [IsDomain S] {P Q : Ideal S} [hP_prime : P.IsPrime] [hQ_prime : Q.IsPrime] (hPQ : P ≤ Q) (hP_ne_bot : P ≠ ⊥) (hht : Q.height ≤ 1) : P = Q

Close-up for principal prime ideals: if y is prime in R and c ∈ yT ∩ R, then c ∈ yR. Uses N-subring condition (3): for P ∈ Ass(T/yT), ht(P ∩ R) ≤ 1, forcing P ∩ R = yR.

theorem close_up_principal {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (y : ↥R.carrier) (hy : Prime y) (c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y}) : c ∈ Ideal.span {y}

Generalized close-up for arbitrary elements

In a UFD N-subring R, if y ∈ R and c ∈ yT ∩ R, then c ∈ yR. Proved by well-founded induction on divisibility, reducing to close_up_principal.

theorem close_up_dvd {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (y c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y}) : c ∈ Ideal.span {y}

Generalized close-up for arbitrary elements: if y ∈ R (NSubring, UFD) and c ∈ yT ∩ R, then c ∈ yR. Proved by induction on prime factorization.