English
If s ⊆ R and I,J are ideals with s ⊆ radical(I ⊔ J), then there exists t: s → R with range ⊆ I such that s ⊆ radical(span(range t) ⊔ J).
Русский
Если s ⊆ R и I,J — идеалы, причём s ⊆ radical(I ⊔ J), то существует t: s → R с образами в I так, что s ⊆ radical(span(range t) ⊔ J).
LaTeX
$$$\\exists t: s \\to R,\\ range(t) \\subseteq I \\quad \\wedge \\ s \\subseteq (\\operatorname{span}(\\operatorname{range}(t)) \\cup J)^{\\mathrm{radical}}$$$
Lean4
theorem exists_subset_radical_span_sup_of_subset_radical_sup {R : Type*} [CommSemiring R] (s : Set R) (I J : Ideal R)
(hs : s ⊆ (I ⊔ J).radical) : ∃ (t : s → R), Set.range t ⊆ I ∧ s ⊆ (span (Set.range t) ⊔ J).radical :=
by
replace hs : ∀ z : s, ∃ (m : ℕ) (a b : R) (ha : a ∈ I) (hb : b ∈ J), a + b = z ^ m :=
by
rintro ⟨z, hzs⟩
simp only [Ideal.radical, Submodule.mem_sup] at hs
obtain ⟨m, y, hyq, b, hb, hy⟩ := hs hzs
exact ⟨m, y, b, hyq, hb, hy⟩
choose m a b ha hb heq using hs
refine ⟨a, by rwa [Set.range_subset_iff], fun z hz ↦ ⟨m ⟨z, hz⟩, heq ⟨z, hz⟩ ▸ ?_⟩⟩
exact Ideal.add_mem _ (mem_sup_left (subset_span ⟨⟨z, hz⟩, rfl⟩)) (mem_sup_right <| hb _)
