English
If s is finite, and f : ι → Ideal R with IsPrime f(i) for i ∈ s, then I ⊆ ⋃ i ∈ s, f i implies ∃ i ∈ s, I ≤ f i.
Русский
Если s конечно, и для каждого i ∈ s f(i) прост, то I ⊆ ⋃ i ∈ s f(i) влечет существование i ∈ s, с I ≤ f(i).
LaTeX
$$$s.finite → (I ⊆ ⋃ i ∈ s, f i) \Rightarrow ∃ i ∈ s, I ≤ f i$ (при соответствующих предпосылках о простоте)$$
Lean4
/-- Prime avoidance. Atiyah-Macdonald 1.11, Eisenbud 3.3, Matsumura Ex.1.6. -/
@[stacks 00DS]
theorem subset_union_prime {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι)
(hp : ∀ i ∈ s, i ≠ a → i ≠ b → IsPrime (f i)) {I : Ideal R} :
((I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i) ↔ ∃ i ∈ s, I ≤ f i :=
suffices ((I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i) → ∃ i, i ∈ s ∧ I ≤ f i
by
have aux := fun h => (bex_def.2 <| this h)
simp_rw [exists_prop] at aux
refine ⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩
apply Set.subset_biUnion_of_mem (show i ∈ (↑s : Set ι) from his)
fun h : (I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), f i => by
classical
by_cases has : a ∈ s
· obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s := ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
by_cases hbt : b ∈ t
· obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
have hp' : ∀ i ∈ u, IsPrime (f i) := by
intro i hiu
refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;> rintro rfl <;>
solve_by_elim only [Finset.mem_insert_of_mem, *]
rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ← Set.union_assoc,
subset_union_prime' hp'] at h
rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
· have hp' : ∀ j ∈ t, IsPrime (f j) := by
intro j hj
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
solve_by_elim only [Finset.mem_insert_of_mem, *]
rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R), subset_union_prime' hp', ← or_assoc,
or_self_iff] at h
rwa [Finset.exists_mem_insert]
· by_cases hbs : b ∈ s
· obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
have hp' : ∀ j ∈ t, IsPrime (f j) := by
intro j hj
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
solve_by_elim only [Finset.mem_insert_of_mem, *]
rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R), subset_union_prime' hp', ← or_assoc,
or_self_iff] at h
rwa [Finset.exists_mem_insert]
rcases s.eq_empty_or_nonempty with hse | hsne
· subst hse
rw [Finset.coe_empty, Set.biUnion_empty, Set.subset_empty_iff] at h
have : (I : Set R) ≠ ∅ := Set.Nonempty.ne_empty (Set.nonempty_of_mem I.zero_mem)
exact absurd h this
· obtain ⟨i, his⟩ := hsne
obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s := ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
have hp' : ∀ j ∈ t, IsPrime (f j) := by
intro j hj
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
solve_by_elim only [Finset.mem_insert_of_mem, *]
rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R), subset_union_prime' hp', ← or_assoc,
or_self_iff] at h
rwa [Finset.exists_mem_insert]
