English
Kernel characterization for mapRange.linearMap: the kernel equals the comap of coordinatewise kernels.
Русский
Характеризация ядра для mapRange.linearMap: ядро равно комапу координатных ядер.
LaTeX
$$$\\ker(\\mathrm{mapRange.linearMap}\\; f) = (\\mathrm{Submodule.pi}\\; \\mathrm{Set.univ}\\; (\\ker (f i))).\\mathrm{comap}\\; (\\mathrm{coeFnLinearMap}\\; R)$$$
Lean4
/-- A variant of `Submodule.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded.
See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
theorem mem_iSup_iff_exists_dfinsupp' (p : ι → Submodule R N) [∀ (i) (x : p i), Decidable (x ≠ 0)] (x : N) :
x ∈ iSup p ↔ ∃ f : Π₀ i, p i, (f.sum fun _ xi => ↑xi) = x :=
by
rw [mem_iSup_iff_exists_dfinsupp]
simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply, LinearMap.toAddMonoidHom_coe, coe_subtype]
