English
For any subset s of R, the preimage of its image in R/I equals the union over i ∈ I of i + s.
Русский
Для любого подмножества s ⊆ R прообраз образа в R/I равен объединению по i∈I множества i + s.
LaTeX
$$$(\\pi_I)^{-1}(\\pi_I''s) = \\bigcup_{i \\in I} (i + s)$$$
Lean4
/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
theorem quotient_ring_saturate (s : Set R) : mk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s :=
by
ext x
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
exact
⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
