English
For a family f_i: β1_i → β2_i of linear maps, the kernel of the global mapRange.linearMap f is exactly the family-wise kernel: the i-th component lies in ker(f_i) for all i.
Русский
Для семейства линейных отображений f_i: β1_i → β2_i ядро глобального отображения mapRange.linearMap f состоит из тех dfinsupp-элементов, у которых каждый i-й компонент лежит в ker(f_i).
LaTeX
$$$\\ker(\\mathrm{mapRange.linearMap}\\; f) = \\Big( \\mathrm{Submodule.pi} \\; \\mathrm{Set.univ} \\; (\\lambda i, \\ker(f_i)) \\Big).\\mathrm{comap}\\; (\\mathrm{coeFnLinearMap}\\; R)$$$
Lean4
theorem ker_mapRangeLinearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
LinearMap.ker (mapRange.linearMap f) =
(Submodule.pi Set.univ (fun i ↦ LinearMap.ker (f i))).comap (coeFnLinearMap R) :=
Submodule.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)
