English
Let R be a commutative semiring, S a submonoid of R, M an AddCommMonoid with a compatible R-module structure, and f: M →ₗ[R] M′ a linear map with IsLocalizedModule S f. Then for every x ∈ M and every finite s ⊆ M′, if f(x) ∈ span_R(s), there exists m ∈ S such that m·x ∈ span_R(finsetIntegerMultiple(S, f, s)).
Русский
Пусть R — коммутативная полугруппа, S — подмоном R, M — аддитивная коммутативная моноида с структурой модуля над R, и f: M →ₗ[R] M′ линейное отображение с условием IsLocalizedModule S f. Тогда для любого x ∈ M и любого конечного s ⊆ M′, если f(x) ∈ span_R(s), существует m ∈ S такое, что m·x ∈ span_R(finsetIntegerMultiple(S, f, s)).
LaTeX
$$$\\forall x\\in M\\,\\forall s\\subseteq M'\\text{ finite},\\ f(x)\\in\\operatorname{span}_R(s)\\ \\Rightarrow\\ \\exists m\\in S:\\ m\\cdot x\\in\\operatorname{span}_R\\big(\\operatorname{finsetIntegerMultiple}(S,f,s)\\big).$$$
Lean4
theorem smul_mem_finsetIntegerMultiple_span [DecidableEq M] (x : M) (s : Finset M') (hx : f x ∈ Submodule.span R s) :
∃ (m : S), m • x ∈ Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s) :=
by
let y : S := IsLocalizedModule.commonDenomOfFinset S f s
have hx₁ : y • (s : Set M') = f '' _ := (IsLocalizedModule.finsetIntegerMultiple_image S f s).symm
apply congrArg (Submodule.span R)at hx₁
rw [Submodule.span_smul] at hx₁
replace hx : _ ∈ y • Submodule.span R (s : Set M') := Set.smul_mem_smul_set hx
rw [hx₁, ← f.map_smul, ← Submodule.map_span f] at hx
obtain ⟨x', hx', hx''⟩ := hx
obtain ⟨a, ha⟩ := (IsLocalizedModule.eq_iff_exists S f).mp hx''
use a * y
convert (Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s : Set M)).smul_mem a hx' using 1
convert ha.symm using 1
simp only [Submonoid.smul_def, ← smul_smul]
