English
For f_i: M_i →+ N_i, the kernel of DirectSum.map f equals the comap of the pi-kernel data: kernel is the set of tuples with each component in ker(f_i).
Русский
Для отображений f_i: M_i →+ N_i ядро DirectSum.map f состоит из кортежей, где каждая компонента лежит в ker(f_i).
LaTeX
$$$\\ker(DirectSum.map f) = \\mathrm{comap}(\\mathrm{DirectSum.coeFnAddMonoidHom M})\\big(\\mathrm{AddSubgroup.pi}(\\mathrm{Set.univ}, i \\mapsto \\ker(f_i))\\big).$$$
Lean4
theorem ker_map [∀ i, AddCommGroup (M i)] [∀ i, AddCommMonoid (N i)] (f : ∀ i, M i →+ N i) :
(map f).ker = (AddSubgroup.pi Set.univ (f · |>.ker)).comap (DirectSum.coeFnAddMonoidHom M) :=
DFinsupp.ker_mapRangeAddMonoidHom f
