Close-up: intersection theorems

Main intersection-related results for the close-up induction. When a common prime p divides the generators s' but neither a nor c, the ideal of s' meets a height-one prime the close-up is obtained by passing to an A-extension where the intersection has been resolved.

theorem close_up_aux_factor_intersection {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) 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) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (n'' : ℕ) (ih : ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (s : Finset ↥R.carrier), s.card ≤ n'' + 1 + 1 → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) (m : ℕ) (ih_m : ∀ m_1 < m, ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (a : ↥R.carrier) (s : Finset ↥R.carrier), gcdComplexity s ≤ m_1 → s.card = n'' + 1 + 1 + 1 → a ∈ s → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) {R : NSubring T} (hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) [DecidableEq ↥R.carrier] {a : ↥R.carrier} {s : Finset ↥R.carrier} (hs_gcd : gcdComplexity s ≤ m) (rest : Finset ↥R.carrier) (hrest_card : rest.card ≤ n'' + 1 + 1) (ha_rest : a ∉ rest) {b : ↥R.carrier} (hb_rest : b ∈ rest) (hgcd_rest : gcdComplexity (insert a rest) ≤ gcdComplexity s) {q' : ↥R.carrier} (hq' : Prime q') (hq'_dvd : ∀ x ∈ rest, q' ∣ x) (hq'_na : ¬q' ∣ a) {c_n : ↥R.carrier} (_hq'_nc : ¬q' ∣ c_n) (hrest_le_q' : Ideal.span ↑rest ≤ Ideal.span {q'}) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ a ∧ p ∣ q')) (hM_bot : IsLocalRing.maximalIdeal T ≠ ⊥) (ha_zero : ↑a ≠ 0) (hc_n : ↑c_n ∈ Ideal.map R.carrier.subtype (Ideal.span ↑(insert a rest))) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c_n, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑(insert a rest))

theorem close_up_aux_factor_no_factor {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) 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) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (n'' : ℕ) (ih : ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (s : Finset ↥R.carrier), s.card ≤ n'' + 1 + 1 → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) (m : ℕ) (ih_m : ∀ m_1 < m, ∀ (R : NSubring T), Cardinal.mk ↥R.carrier < Cardinal.mk T → ∀ (a : ↥R.carrier) (s : Finset ↥R.carrier), gcdComplexity s ≤ m_1 → s.card = n'' + 1 + 1 + 1 → a ∈ s → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) {R : NSubring T} (hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) [DecidableEq ↥R.carrier] {a : ↥R.carrier} (ih_a : ∀ (y : ↥R.carrier), DvdNotUnit y a → ∀ (s : Finset ↥R.carrier), gcdComplexity s ≤ m → s.card = n'' + 1 + 1 + 1 → y ∈ s → ∀ (c : ↥R.carrier), ↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) → ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)) {s : Finset ↥R.carrier} (hs_gcd : gcdComplexity s ≤ m) (rest : Finset ↥R.carrier) (hrest_card : rest.card ≤ n'' + 1 + 1) (ha_rest : a ∉ rest) {b : ↥R.carrier} (hb_rest : b ∈ rest) (hgcd_rest : gcdComplexity (insert a rest) ≤ gcdComplexity s) {c_n : ↥R.carrier} (h_factor : ∀ (q' : ↥R.carrier), Prime q' → (∀ x ∈ rest, q' ∣ x) → ¬q' ∣ a ∧ ¬q' ∣ c_n) (hc_n : ↑c_n ∈ Ideal.map R.carrier.subtype (Ideal.span ↑(insert a rest))) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c_n, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑(insert a rest))