English
The additive monoid hom that evaluates the DirectSum by coordinates equals the dfinsupp sum of the coordinates after coercing each coordinate into the ambient space.
Русский
Аддитивный однородный гомоморфизм, определяющий DirectSum по координатам, равен dfinsupp-сумме координат после вложения координат в оболочку пространства.
LaTeX
$$$$\\operatorname{DirectSum.coeAddMonoidHom} A\\; x = \\mathrm{DFinsupp.sum}\\; x\\; (\\lambda i\, y:\\; A(i),\\; \\uparrow y).$$$$
Lean4
theorem coeAddMonoidHom_eq_dfinsuppSum [DecidableEq ι] {M S : Type*} [DecidableEq M] [AddCommMonoid M] [SetLike S M]
[AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun i => A i) :
DirectSum.coeAddMonoidHom A x = DFinsupp.sum x fun i => (fun x : A i => ↑x) :=
by
simp only [DirectSum.coeAddMonoidHom, toAddMonoid, DFinsupp.liftAddHom, AddEquiv.coe_mk, Equiv.coe_fn_mk]
exact DFinsupp.sumAddHom_apply _ x
