English
The union of all minimal primes over I equals the set of x in R for which there exists y not in radical(I) with x*y in radical(I).
Русский
Объединение всех минимальныхPrime над I равно множество элементов x так, что существует y не в радикале(I), и xy ∈ радикал(I).
LaTeX
$$$\bigcup_{p \in I.minimalPrimes} p = \{ x \in R \mid \exists y \notin I.radical, \; x y \in I.radical \}$$$
Lean4
theorem iUnion_minimalPrimes : ⋃ p ∈ I.minimalPrimes, p = {x | ∃ y ∉ I.radical, x * y ∈ I.radical} := by
classical
ext x
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
constructor
· rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
have : p.map (algebraMap R (Localization.AtPrime p)) ≤ (I.map (algebraMap _ _)).radical :=
by
rw [Ideal.radical_eq_sInf, le_sInf_iff]
rintro q ⟨hq', hq⟩
obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
rw [Ideal.map_le_iff_le_comap] at hq' ⊢
exact hp₃ ⟨h₁, hq'⟩ h₂
obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
obtain ⟨⟨a, b⟩, hn⟩ := hn
rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
obtain ⟨t, ht⟩ := hn
refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
simp only at ht
have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by rw [mul_assoc, ← ht]; ring
rw [this]
exact I.mul_mem_left _ a.2
· rintro ⟨y, hy, hx⟩
obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by simpa [← Ideal.sInf_minimalPrimes] using hy
refine ⟨p, hp, (hp.1.1.mem_or_mem ?_).resolve_right hyp⟩
exact hp.1.1.radical_le_iff.mpr hp.1.2 hx
