English
If s is a finite subset of I, then the good products span all LocallyConstant ℤ-valued functions on C.
Русский
Если s — конечное подмножество I, то хорошие произведения порождают всю модуль-структуру LocallyConstant C ℤ.
LaTeX
$$\top \le \operatorname{span}_{\mathbb{Z}} (\operatorname{Set.range} (\mathrm{eval}\ C))$$
Lean4
/-- If `s` is a finite subset of `I`, then the good products span. -/
theorem spanFin [WellFoundedLT I] : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (· ∈ s)))) :=
by
rw [span_iff_products]
refine le_trans (spanFinBasis.span C s) ?_
rw [Submodule.span_le]
rintro _ ⟨x, rfl⟩
rw [← factors_prod_eq_basis]
let l := s.sort (· ≥ ·)
dsimp [factors]
suffices
l.IsChain (· > ·) →
(l.map (fun i ↦ if x.val i = true then e (π C (· ∈ s)) i else (1 - (e (π C (· ∈ s)) i)))).prod ∈
Submodule.span ℤ ((Products.eval (π C (· ∈ s))) '' {m | m.val ≤ l})
from Submodule.span_mono (Set.image_subset_range _ _) (this (Finset.sort_sorted_gt _).isChain)
induction l with
| nil =>
intro _
apply Submodule.subset_span
exact ⟨⟨[], List.isChain_nil⟩, ⟨Or.inl rfl, rfl⟩⟩
| cons a as ih =>
rw [List.map_cons, List.prod_cons]
intro ha
specialize ih (by rw [List.isChain_cons'] at ha; exact ha.2)
rw [Finsupp.mem_span_image_iff_linearCombination] at ih
simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih
obtain ⟨c, hc, hc'⟩ := ih
rw [← hc']; clear hc'
have hmap := fun g ↦ map_finsuppSum (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)) c g
dsimp at hmap ⊢
split_ifs
· rw [hmap]
exact finsuppSum_mem_span_eval _ _ ha hc
· noncomm_ring
-- we use `noncomm_ring` even though this is a commutative ring, because we want a weaker
-- normalization which preserves multiplication order (i.e. doesn't use commutativity rules)
rw [hmap]
apply Submodule.add_mem
· apply Submodule.finsuppSum_mem
intro m hm
apply Submodule.smul_mem
apply Submodule.subset_span
refine ⟨m, ⟨?_, rfl⟩⟩
simp only [Set.mem_setOf_eq]
have hmas : m.val ≤ as := hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
refine le_trans hmas ?_
cases as with
| nil => exact (List.nil_lt_cons a []).le
| cons b bs =>
apply le_of_lt
rw [List.isChain_cons_cons] at ha
exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)
· apply Submodule.smul_mem
exact finsuppSum_mem_span_eval _ _ ha hc
