English
Given a chain a :: as and a finsupp c with support contained in {m | m.val ≤ as}, the finsupp sum of the evaluated terms lies in the span of evaluations up to a::as.
Русский
Пусть a :: as образует нечётную цепь, и для c с опорой ⊆ {m | m.val ≤ as}. сумма Finsupp от c умноженная на значения eval лежит в span функций eval с аргументами не превосходящими a :: as.
LaTeX
$$$ (Finsupp.sum\ c\ (fun a_1 b \mapsto e (\pi C (\cdot \in s)) a * b \; \cdot\; Products.eval (\pi C (\cdot \in s)) a_1)) \in\ Submodule.span\ ℤ (Products.eval (\pi C (\cdot \in s)) '' {m \mid m.val \le a :: as}) $$$
Lean4
theorem finsuppSum_mem_span_eval {a : I} {as : List I} (ha : List.IsChain (· > ·) (a :: as)) {c : Products I →₀ ℤ}
(hc : (c.support : Set (Products I)) ⊆ {m | m.val ≤ as}) :
(Finsupp.sum c fun a_1 b ↦ e (π C (· ∈ s)) a * b • Products.eval (π C (· ∈ s)) a_1) ∈
Submodule.span ℤ (Products.eval (π C (· ∈ s)) '' {m | m.val ≤ a :: as}) :=
by
apply Submodule.finsuppSum_mem
intro m hm
have hsm := (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)).map_smul
dsimp at hsm
rw [hsm]
apply Submodule.smul_mem
apply Submodule.subset_span
have hmas : m.val ≤ as := by
apply hc
simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm
refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩
simp only [Products.eval, List.map, List.prod_cons]
