English
If x lies in the i-th component ℳ_i, then its image under the global decomposition corresponds to the i-th summand and matches x there, with other components zero.
Русский
Если x лежит в компоненте i-го индекса ℳ_i, то образ под глобальной декомпозицией соответствует i-й компоненте и совпадает с x, а прочие компоненты равны нулю.
LaTeX
$$$\text{If } x\in \mathcal{M}_i,\ \mathrm{decompose}(x) = \mathrm{of}_{i}(x) \oplus 0$$$
Lean4
/-- A convenience method to construct a decomposition from an `AddMonoidHom`, such that the proofs
of left and right inverse can be constructed via `ext`. -/
abbrev ofAddHom (decompose : M →+ ⨁ i, ℳ i) (h_left_inv : (DirectSum.coeAddMonoidHom ℳ).comp decompose = .id _)
(h_right_inv : decompose.comp (DirectSum.coeAddMonoidHom ℳ) = .id _) : Decomposition ℳ
where
decompose' := decompose
left_inv := DFunLike.congr_fun h_left_inv
right_inv := DFunLike.congr_fun h_right_inv
