English
If the evaluation on C is linearly independent, then the composition with the Good/CC' maps is also linearly independent.
Русский
Если отображение оценки на C линейно независимо, то композиция с линейными картами Good/CC' тоже линейно независима.
LaTeX
$$$$\\text{LinearIndependent}\\;\\mathbb{Z}\\;\\big( \\mathrm{eval}\\; (C'\\,C\\;ho) \\big) \\Rightarrow \\text{LinearIndependent}\\;\\mathbb{Z}\\;\\big( \\mathrm{ModuleCat.ofHom}(\\mathrm{Linear\\_CC'}\\; C\\; hsC\\; ho) \\circ \\mathrm{SumEval}\\; C\\; ho \\circ \\mathrm{Sum}.\\mathrm{inr} \\big)$$$$
Lean4
theorem linearIndependent_comp_of_eval (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (ord I · < o))))) :
LinearIndependent ℤ (eval (C' C ho)) →
LinearIndependent ℤ (ModuleCat.ofHom (Linear_CC' C hsC ho) ∘ SumEval C ho ∘ Sum.inr) :=
by
dsimp [SumEval, ModuleCat.ofHom]
rw [max_eq_eval_unapply C hsC ho]
intro h
let f := MaxToGood C hC hsC ho h₁
have hf : f.Injective := maxToGood_injective C hC hsC ho h₁
have hh : (fun l ↦ Products.eval (C' C ho) l.val.Tail) = eval (C' C ho) ∘ f := rfl
rw [hh]
exact h.comp f hf
