English
If a subset s of a ring R is absorbing under multiplication on both sides by all elements of R, then span(s) equals the AddSubgroup closure of the set s ∪ (s·R) ∪ (R·s) ∪ (R·s·R).
Русский
Если подмножество s кольца R поглощает умножение слева и справа на произвольные элементы кольца, то span(s) совпадает с замыканием по сложению множества s ∪ (sR) ∪ (Rs) ∪ (R s R).
LaTeX
$$$ z \\in \\operatorname{span}(s) \\iff z \\in \\operatorname{closure}\\Bigl(s \\cup (s\\cdot \\mathrm{univ}) \\cup (\\mathrm{univ}\\cdot s) \\cup (\\mathrm{univ}\\cdot s \\cdot \\mathrm{univ})\\Bigr)$$$
Lean4
/-- If `s : Set R` is absorbing under multiplication, then its `TwoSidedIdeal.span` coincides with
its `AddSubgroup.closure`, as sets. -/
theorem mem_span_iff_mem_addSubgroup_closure_absorbing {s : Set R} (h_left : ∀ x y, y ∈ s → x * y ∈ s)
(h_right : ∀ y x, y ∈ s → y * x ∈ s) {z : R} : z ∈ span s ↔ z ∈ closure s :=
by
have h_left' {x y} (hy : y ∈ closure s) : x * y ∈ closure s :=
by
have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
refine closure_mono ?_ this
rintro - ⟨y, hy, rfl⟩
exact h_left x y hy
have h_right' {y x} (hy : y ∈ closure s) : y * x ∈ closure s :=
by
have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
refine closure_mono ?_ this
rintro - ⟨y, hy, rfl⟩
exact h_right y x hy
let I : TwoSidedIdeal R :=
.mk' (closure s) (AddSubgroup.zero_mem _) (AddSubgroup.add_mem _) (AddSubgroup.neg_mem _) h_left' h_right'
suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]
rw [mem_span_iff]
-- Suppose that for every ideal `J` with `s ⊆ J`, then `z ∈ J`. Apply this to `I` to get `z ∈ I`.
refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩
case mem_closure_of_forall => simpa only [I, SetLike.mem_coe, mem_mk'] using subset_closure hx
case mem_ideal_of_subset =>
simp only [I, SetLike.mem_coe, mem_mk'] at hz
induction hz using closure_induction with
| mem x hx => exact hJ hx
| zero => exact zero_mem _
| add x y _ _ hx hy => exact J.add_mem hx hy
| neg x _ hx => exact J.neg_mem hx
