English
An element x lies in the span of the image of a under the algebra map if and only if there exists y in span a and z in M with x = IsLocalization.mk'(S) y z.
Русский
Элемент x лежит в порождаемом образе изображения a через алгебраическое отображение ⇔ существует y ∈ span(a) и z ∈ M с x = IsLocalization.mk'(S) y z.
LaTeX
$$mem_span_map : x ∈ Ideal.span (algebraMap R S '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z : M, x = mk' S y z$$
Lean4
theorem mem_span_map {x : S} {a : Set R} :
x ∈ Ideal.span (algebraMap R S '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z : M, x = mk' S y z :=
by
refine (mem_span_iff M).trans ?_
constructor
· rw [← coeSubmodule_span]
rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩
refine ⟨y, hy, z, ?_⟩
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
· rintro ⟨y, hy, z, hz⟩
refine ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, ?_⟩
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
