English
For I an ideal, a function f: ι → M, and x ∈ M, x ∈ I • span R (range f) iff there exists a finite support I-valued function a with a ∈ I such that sum a_i f(i) = x.
Русский
Для идеала I, отображения f и x ∈ M верно: x ∈ I • span R (range f) тогда и только тогда, когда существует суммафинитного выражения с элементами из I, которая даёт x.
LaTeX
$$$x \\in I \\cdot \\operatorname{span} R (\\operatorname{range} f) \\iff \\exists a \\colon \\iota \\to_R, \\text{finite support}, a(i) \\in I, \\sum_i a(i) f(i) = x$$$
Lean4
/-- If `x` is an `I`-multiple of the submodule spanned by `f '' s`,
then we can write `x` as an `I`-linear combination of the elements of `f '' s`. -/
theorem mem_ideal_smul_span_iff_exists_sum {ι : Type*} (f : ι → M) (x : M) :
x ∈ I • span R (Set.range f) ↔ ∃ (a : ι →₀ R) (_ : ∀ i, a i ∈ I), (a.sum fun i c => c • f i) = x :=
by
constructor; swap
· rintro ⟨a, ha, rfl⟩
exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _
refine fun hx => span_induction ?_ ?_ ?_ ?_ (mem_smul_span.mp hx)
· simp only [Set.mem_iUnion, Set.mem_range, Set.mem_singleton_iff]
rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩
refine ⟨Finsupp.single i y, fun j => ?_, ?_⟩
· letI := Classical.decEq ι
rw [Finsupp.single_apply]
split_ifs
· assumption
· exact I.zero_mem
refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_
simp
· exact ⟨0, fun _ => I.zero_mem, Finsupp.sum_zero_index⟩
· rintro x y - - ⟨ax, hax, rfl⟩ ⟨ay, hay, rfl⟩
refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩ <;> intros <;>
simp only [zero_smul, add_smul]
· rintro c x - ⟨a, ha, rfl⟩
refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]
