English
Variant form of ker_map_of_surjective: the kernel of map R R A B coincides with the comap of finsupp_map via algebraic linear combination.
Русский
Вариант формы ker_map_of_surjective: ядро отображения R→B совпадает с comap finsupp_map через линейную комбинацию Финиссуфф.
LaTeX
$$$\\ker(\\mathrm{map}\\,R\\,R\\,A\\,B) = (\\ker(\\mathrm{finsupp\\_map})).comap(\\mathrm{Finsupp.linearCombination}\\,A\\,D\\,R\\,A)$$$
Lean4
theorem ker_map_of_surjective (h : Function.Surjective (algebraMap A B)) :
LinearMap.ker (map R R A B) = (LinearMap.ker finsupp_map).map (Finsupp.linearCombination A (D R A)) :=
by
rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup, Submodule.map_sup, ← kerTotal_eq, ←
Submodule.comap_bot, Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _), bot_sup_eq,
Submodule.map_span, ← Set.range_comp]
convert bot_sup_eq _
rw [Submodule.span_eq_bot]; simp
