English
For finite σ, the range of eval_i is the whole space, i.e. the map is surjective onto the space of all functions σ → K.
Русский
Для конечного множества σ образ отображения eval_i равен всему пространству функций σ → K; отображение сюръективно.
LaTeX
$$$\\\\mathrm{range}(\\\\mathrm{eval}_{i}) = \\top$$$
Lean4
theorem map_restrict_dom_evalₗ : (restrictDegree σ K (Fintype.card K - 1)).map (evalₗ K σ) = ⊤ :=
by
cases nonempty_fintype σ
refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)
classical
refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
· exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)
· ext n
simp only [evalₗ_apply, map_sum, smul_eval]
rw [Finset.sum_eq_single n] <;>
aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])
