English
Let α be a type, M,N be modules over rings R and R2 respectively, and φ, ψ be R-linear maps from the finitely supported functions α →₀ M to N. If φ and ψ agree on every elementary function single a b (i.e., on each basis element of the Finsupp direct sum), then φ = ψ. In other words, a linear map out of a direct sum is determined by its values on the natural basis elements.
Русский
Пусть α — тип, M и N — модули над кольцами R и R2 соответственно, и φ, ψ — R-линейные отображения из сконструированного как сумма с конечной опорой вида α →₀ M в N. Тогда если φ и ψ совпадают на каждом базисном элементе single a b, то φ = ψ. То есть линейное отображение из прямой суммы определяется его значениями на элементарных базисах.
LaTeX
$$$\\forall \\varphi,\\psi : (\\alpha \\to_0 M) \\to_\\sigma N,\\; (\\forall a\\in\\alpha,\\forall b\\in M: \\varphi(\\mathrm{single}\\,a\\,b)=\\psi(\\mathrm{single}\\,a\\,b)) \\Rightarrow \\varphi=\\psi$$$
Lean4
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere. -/
theorem lhom_ext ⦃φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N⦄ (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ :=
LinearMap.toAddMonoidHom_injective <| addHom_ext h
