Krull domain intersection construction

Constructs the intersection NSubring for the Anderson--Jensen proof. Starting from two adjoin-localisation subrings, one shows the intersection is a Noetherian UFD whose primes have height at most one in T, using well-founded descent on heights and the mod-principal transcendence argument.

theorem derive_mod_principal_trans {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (y : ↥R.carrier) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hx_ker : ∀ (P : Ideal T), P.IsPrime → P ≠ ⊤ → P.height ≤ 1 → ↑y ∉ P → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x) f ∈ P → Polynomial.C p ∣ f) (p : ↥R.carrier) (hp : Prime p) (hpy : ¬p ∣ y) (f : Polynomial ↥R.carrier) (hf_mem : (Polynomial.aeval x) f ∈ Ideal.span {↑p}) : Polynomial.C p ∣ f

Section 4: Main Close-Up Theorem

The Krull domain intersection construction produces an NSubring S that is an A-extension of R with c ∈ (y₁,y₂)·S.

theorem height_bound_wf_descent {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) [IsDomain ↥S_sub] [WfDvdMonoid ↥S_sub] (hR_le : R.carrier ≤ S_sub) (hRbar_le_S : ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, t ∈ ↑S_sub) (hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (hR_prime_in_S : ∀ (p : ↥R.carrier), Prime p → ↑p ∈ IsLocalRing.maximalIdeal T → Prime ⟨↑p, ⋯⟩) (hS_mem_rep : ∀ (s : ↥S_sub), ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ ↑s * b = a) (P : Ideal T) [hP_prime : P.IsPrime] (hP_ht : P.height ≤ 1) (hR_bound : (Ideal.comap R.carrier.subtype P).height ≤ 1) (hPR_bot : Ideal.comap R.carrier.subtype P ≠ ⊥) (hP_le_M : P ≤ IsLocalRing.maximalIdeal T) (x_eval : T) (y_elem : ↥R.carrier) (hy_nP : ↑y_elem ∉ P) (hx_ker : ∀ (P' : Ideal T), P'.IsPrime → P' ≠ ⊤ → P'.height ≤ 1 → ↑y_elem ∉ P' → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P' → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x_eval) f ∈ P' → Polynomial.C p ∣ f) (heval_S : ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x_eval) f ∈ S_sub) (get_witness : ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, ∃ (f : Polynomial ↥R.carrier) (n : ℕ), t * ↑y_elem ^ n = (Polynomial.aeval x_eval) f) (q : Ideal ↥S_sub) [hq_prime : q.IsPrime] (hq_lt : q < Ideal.comap S_sub.subtype P) (s : ↥S_sub) (hs_ne : s ≠ 0) (hs_q : s ∈ q) : False

theorem build_height_bound {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) (S_sub : Subring T) [UniqueFactorizationMonoid ↥S_sub] (hR_le : R.carrier ≤ S_sub) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hy₁ : ↑y₁ ≠ 0) (hy₂ : ↑y₂ ≠ 0) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (hx₁_trans : Transcendental (↥R.carrier) x₁) (hx₂_trans : Transcendental (↥R.carrier) x₂) (hx₁_ker : ∀ (P : Ideal T), P.IsPrime → P ≠ ⊤ → P.height ≤ 1 → ↑y₂ ∉ P → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₁) f ∈ P → Polynomial.C p ∣ f) (hx₂_ker : ∀ (P : Ideal T), P.IsPrime → P ≠ ⊤ → P.height ≤ 1 → ↑y₁ ∉ P → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₂) f ∈ P → Polynomial.C p ∣ f) (hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (hR_prime_in_S : ∀ (p : ↥R.carrier), Prime p → ↑p ∈ IsLocalRing.maximalIdeal T → Prime ⟨↑p, ⋯⟩) (hS_sub_eq : ↑S_sub = {t : T | ∃ (a : T) (b : T), a ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∈ intersectionSet R x₁ x₂ y₁ y₂ ∧ b ∉ IsLocalRing.maximalIdeal T ∧ t * b = a}) (hRbar_le_S : ∀ t ∈ intersectionSet R x₁ x₂ y₁ y₂, t ∈ ↑S_sub) (hx₁_Rbar : x₁ ∈ intersectionSet R x₁ x₂ y₁ y₂) (hx₂_Rbar : x₂ ∈ intersectionSet R x₁ x₂ y₁ y₂) (t : T) : t ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {t}), (Ideal.comap S_sub.subtype P).height ≤ 1

theorem build_intersection_nsubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ c : ↥R.carrier) (hc_eq : ↑c = x₁ * ↑y₁ + x₂ * ↑y₂) (hx₁_trans : Transcendental (↥R.carrier) x₁) (hx₂_trans : Transcendental (↥R.carrier) x₂) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (hy₁ : ↑y₁ ≠ 0) (hy₂ : ↑y₂ ≠ 0) (_hM_ne_bot : IsLocalRing.maximalIdeal T ≠ ⊥) (hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (_hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) (_hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hx₁_ker : ∀ (P : Ideal T), P.IsPrime → P ≠ ⊤ → P.height ≤ 1 → ↑y₂ ∉ P → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₁) f ∈ P → Polynomial.C p ∣ f) (hx₂_ker : ∀ (P : Ideal T), P.IsPrime → P ≠ ⊤ → P.height ≤ 1 → ↑y₁ ∉ P → ∀ (p : ↥R.carrier), Prime p → ↑p ∈ P → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x₂) f ∈ P → Polynomial.C p ∣ f) : ∃ (S : NSubring T), IsAExtension R S ∧ x₁ ∈ S.carrier ∧ x₂ ∈ S.carrier