Close-up: divisibility sub-cases #
Sub-cases of the well-founded induction for the close-up construction where a common prime factor p of the generators s' divides either the distinguished generator a or the witness c. Dividing out p reduces the GCD complexity.
theorem
close_up_aux_factor_dvd_a
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain 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 : ℕ)
{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)
(hgcd_rest : gcdComplexity (insert a rest) ≤ gcdComplexity s)
{q' : ↥R.carrier}
(hq' : Prime q')
(hq'_dvd : ∀ x ∈ rest, q' ∣ x)
(hq'a : q' ∣ a)
{c_n : ↥R.carrier}
(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_dvd_c
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
(hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r}))
(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))
{R : NSubring T}
(hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T)
[DecidableEq ↥R.carrier]
{a : ↥R.carrier}
{s : Finset ↥R.carrier}
(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)
(ih_b :
∀ (y : ↥R.carrier),
DvdNotUnit y b →
∀ (rest : Finset ↥R.carrier),
rest.card ≤ n'' + 1 + 1 →
a ∉ rest →
y ∈ rest →
gcdComplexity (insert a rest) ≤ gcdComplexity s →
∀ (c_n : ↥R.carrier),
↑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)))
{q' : ↥R.carrier}
(hq' : Prime q')
(hq'_dvd : ∀ x ∈ rest, q' ∣ x)
(hq'a : ¬q' ∣ a)
{c_n : ↥R.carrier}
(hc_n : ↑c_n ∈ Ideal.map R.carrier.subtype (Ideal.span ↑(insert a rest)))
(hq'c : q' ∣ c_n)
:
∃ (S : NSubring T),
IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c_n, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑(insert a rest))