English
The kernel of the linear map toLin'(diagonal w) can be described as the supremum of ranges of single-entry maps at indices where w_i = 0.
Русский
Ядро отображения toLin'(diagonal w) совпадает с объединением (супремумом) образов линейных отображений-элементов на индексах i, где w_i = 0.
LaTeX
$$ker (toLin'(diagonal w)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.single K (fun _ => K) i)$$
Lean4
theorem ker_diagonal_toLin' [DecidableEq m] (w : m → K) :
ker (toLin' (diagonal w)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.single K (fun _ => K) i) :=
by
rw [← comap_bot, ← iInf_ker_proj, comap_iInf]
have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
simp only [← this, proj_diagonal, ker_smul']
have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ := by rw [Set.union_compl_self]
exact (iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this (Set.toFinite _)).symm
