English
If l is a maximal product and certain boundedness condition holds, then l.val.Tail is a good product with respect to C'.
Русский
Если l — максимальный произведение и выполняется требуемая ограниченность, то l.val.Tail является хорошим произведением относительно C'.
LaTeX
$$$$\\operatorname{maxTail\\_isGood}\\; (C\\,hC\\,ho)\\; (l)\\; (h_1) :\\; l.\\mathrm{val}.\\mathrm{Tail} \\in \\mathrm{isGood}(C'\\,C\\;ho)$$$$
Lean4
/-- Removing the leading `o` from a term of `MaxProducts C` yields a list which `isGood` with respect to
`C'`.
-/
theorem maxTail_isGood (l : MaxProducts C ho) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (ord I · < o))))) :
l.val.Tail.isGood (C' C ho) :=
by
have : Inhabited I :=
⟨term I ho⟩
-- Write `l.Tail` as a linear combination of smaller products:
intro h
rw [Finsupp.mem_span_image_iff_linearCombination, ← max_eq_eval C hsC ho] at h
obtain ⟨m, ⟨hmmem, hmsum⟩⟩ := h
rw [Finsupp.linearCombination_apply] at hmsum
have :
(Linear_CC' C hsC ho) (l.val.eval C) =
(Linear_CC' C hsC ho) (Finsupp.sum m fun i a ↦ a • ((term I ho :: i.1).map (e C)).prod) :=
by
rw [← hmsum]
simp only [map_finsuppSum]
apply Finsupp.sum_congr
intro q hq
rw [LinearMap.map_smul]
rw [Finsupp.mem_supported] at hmmem
have hx'' : q < l.val.Tail := hmmem hq
have : ∃ (p : Products I), p.val ≠ [] ∧ p.val.head! = term I ho ∧ q = p.Tail :=
⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q hx''⟩,
⟨List.cons_ne_nil _ _, by simp only [List.head!_cons], by
simp only [Products.Tail, List.tail_cons, Subtype.coe_eta]⟩⟩
obtain ⟨p, hp⟩ := this
rw [hp.2.2, ← Products.max_eq_eval C hsC ho p hp.1 hp.2.1]
dsimp [Products.eval]
rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1, List.map_cons, List.prod_cons]
have hse := succ_exact C hC hsC ho
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker] at hse
dsimp [ModuleCat.ofHom] at hse
rw [← LinearMap.sub_mem_ker_iff, ← hse] at this
obtain ⟨(n : LocallyConstant (π C (ord I · < o)) ℤ), hn⟩ := this
rw [eq_sub_iff_add_eq] at hn
have hn' := h₁ (Submodule.mem_top : n ∈ ⊤)
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn'
obtain ⟨w, hc⟩ := hn'
rw [← hc, map_finsuppSum] at hn
apply l.prop.1
rw [← hn]
-- Now we just need to prove that a sum of two terms belongs to a span:
apply Submodule.add_mem
· apply Submodule.finsuppSum_mem
intro q _
rw [LinearMap.map_smul]
apply Submodule.smul_mem
apply Submodule.subset_span
dsimp only [eval]
rw [Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)]
refine ⟨q.val, ⟨?_, rfl⟩⟩
simp only [Products.lt_iff_lex_lt, Set.mem_setOf_eq]
exact good_lt_maxProducts C hsC ho q l
· apply Submodule.finsuppSum_mem
intro q hq
apply Submodule.smul_mem
apply Submodule.subset_span
rw [Finsupp.mem_supported] at hmmem
rw [← Finsupp.mem_support_iff] at hq
refine ⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q (hmmem hq)⟩, ⟨?_, rfl⟩⟩
simp only [Products.lt_iff_lex_lt, Set.mem_setOf_eq]
rw [max_eq_o_cons_tail C hsC ho l]
exact List.Lex.cons ((Products.lt_iff_lex_lt q l.val.Tail).mp (hmmem hq))
