English
Linear independence of eval C over integers is equivalent to the linear independence of SumEval C ho.
Русский
Линейная независимость eval C над целыми числами эквивалентна линейной независимости SumEval C ho.
LaTeX
$$$\\mathrm{LinearIndependent}_{\\mathbb{Z}}(\\mathrm{eval}\\ C) \\iff \\mathrm{LinearIndependent}_{\\mathbb{Z}}(\\mathrm{SumEval}\\ C\\ ho)$$$
Lean4
/-- Let
`N := LocallyConstant (π C (ord I · < o)) ℤ`
`M := LocallyConstant C ℤ`
`P := LocallyConstant (C' C ho) ℤ`
`ι := GoodProducts (π C (ord I · < o))`
`ι' := GoodProducts (C' C ho')`
`v : ι → N := GoodProducts.eval (π C (ord I · < o))`
Then `SumEval C ho` is the map `u` in the diagram below. It is linearly independent if and only if
`GoodProducts.eval C` is, see `linearIndependent_iff_sum`. The top row is the exact sequence given
by `succ_exact` and `succ_mono`. The left square commutes by `GoodProducts.square_commutes`.
```
0 --→ N --→ M --→ P
↑ ↑ ↑
v| u| |
ι → ι ⊕ ι' ← ι'
```
-/
def SumEval : GoodProducts (π C (ord I · < o)) ⊕ MaxProducts C ho → LocallyConstant C ℤ :=
Sum.elim (fun l ↦ l.1.eval C) (fun l ↦ l.1.eval C)
