English
Two linear maps from M to N that agree on every piece ℳ_i (via composing with the inclusion maps (ℳ_i).subtype) are equal.
Русский
Две линейные аппроксимации из M в N, совпадающие на каждой компоненте, равны между собой.
LaTeX
$$$\forall i,\ f \circ (\mathcal{M}_i).\text{subtype} = g \circ (\mathcal{M}_i).\text{subtype} \implies f = g$$$
Lean4
/-- Two linear maps from a module with a decomposition agree if they agree on every piece.
Note this cannot be `@[ext]` as `ℳ` cannot be inferred. -/
theorem decompose_lhom_ext {N} [AddCommMonoid N] [Module R N] ⦃f g : M →ₗ[R] N⦄
(h : ∀ i, f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype) : f = g :=
LinearMap.ext <|
(decomposeLinearEquiv ℳ).symm.surjective.forall.mpr <|
suffices f ∘ₗ (decomposeLinearEquiv ℳ).symm = (g ∘ₗ (decomposeLinearEquiv ℳ).symm : (⨁ i, ℳ i) →ₗ[R] N) from
DFunLike.congr_fun this
linearMap_ext _ fun i => by simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]
