English
For a family of additive monoid homomorphisms f_i, the kernel of the global mapRange addMonoidHom is the comap of coeFnAddMonoidHom from the product of kernels.
Русский
Для семейства гомоморфизмовAddMonoid f_i ядро глобального mapRange.addMonoidHom равно комапу по коэFnAddMonoidHom из произведения ядер.
LaTeX
$$$\\ker(\\mathrm{mapRange.addMonoidHom}\\; f) = \\mathrm{AddSubmonoid.comap}\\; (\\mathrm{coeFnAddMonoidHom})\\; (\\mathrm{AddSubgroup.pi}\\; \\mathrm{Set.univ} \\; (\\lambda i, \\ker f_i))$$$
Lean4
theorem ker_mapRangeAddMonoidHom [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommMonoid (β₂ i)] (f : ∀ i, β₁ i →+ β₂ i) :
(mapRange.addMonoidHom f).ker = (AddSubgroup.pi Set.univ (f · |>.ker)).comap coeFnAddMonoidHom :=
AddSubgroup.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom f
