Close-up: intersection helpers #
Auxiliary lemmas for the intersection sub-case of the close-up well-founded induction. Handles the situation where the ideal generated by s' has large intersection with a prime, and proves the strict decrease of GCD complexity after dividing by a common prime factor.
theorem
close_up_aux_factor_intersection_large
{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 : ℕ)
(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}
[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)
{S₁ : NSubring T}
(hAext₁ : IsAExtension R S₁)
(hle₁ : R.carrier ≤ S₁.carrier)
(hS₁_card : Cardinal.mk ↥S₁.carrier < Cardinal.mk T)
(w : ↥S₁.carrier)
(div_q_b2 : ↥R.carrier → ↥R.carrier)
(hdiv_b2 : ∀ x ∈ rest, x = q' * div_q_b2 x)
(rest'2 : Finset ↥R.carrier)
(hrest'2_def : rest'2 = Finset.image div_q_b2 rest)
(_h_ml_b2 : Ideal.span {q'} * Ideal.span ↑(insert a rest'2) ≤ Ideal.span ↑(insert a rest))
(hw_mem_T : ↑w ∈ Ideal.map R.carrier.subtype (Ideal.span ↑(insert a rest'2)))
(ha_rest'2 : a ∉ rest'2)
(hrest'2_card : rest'2.card = n'' + 1 + 1)
(hb_rest'2 : div_q_b2 b ∈ rest'2)
:
∃ (S₂ : NSubring T),
IsAExtension S₁ S₂ ∧ ∃ (hle₂ : S₁.carrier ≤ S₂.carrier),
⟨↑w, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle₂) (Ideal.map (Subring.inclusion hle₁) (Ideal.span ↑(insert a rest'2)))
theorem
gcdComplexity_div_prime_strict
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
{R : NSubring T}
[DecidableEq ↥R.carrier]
{a : ↥R.carrier}
{s s' : Finset ↥R.carrier}
(hs_insert : s = insert a s')
(hs'_def : s' = s.erase a)
(hs'_card_ge : 2 ≤ s'.card)
{p : ↥R.carrier}
(hp : Prime p)
(div_f : ↥R.carrier → ↥R.carrier)
(hdiv : ∀ x ∈ s', x = p * div_f x)
(ha_sdiv : a ∉ Finset.image div_f s')
: