English
The multiplication in the direct sum is given by the double sum over the supports: a * a' equals the sum over all index pairs (i, j) of a_i * a'_j placed in DirectSum via the appropriate basis.
Русский
Умножение в прямой сумме задаётся двойной суммой по множествам опор: a * a' равняется сумме по всем парам индексов (i, j) произведений a_i и a'_j, вставленных в DirectSum через соответствующую базисную схему.
LaTeX
$$$a * a' = \sum_{i, j} a_i a'_j$$
Lean4
theorem mul_eq_dfinsuppSum [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
a * a' = a.sum fun _ ai => a'.sum fun _ aj => DirectSum.of _ _ <| GradedMonoid.GMul.mul ai aj :=
by
change
mulHom _ a a' =
_
-- Porting note: I have no idea how the proof from ml3 worked it used to be
-- simpa only [mul_hom, to_add_monoid, dfinsupp.lift_add_hom_apply, dfinsupp.sum_add_hom_apply,
-- add_monoid_hom.dfinsupp_sum_apply, flip_apply, add_monoid_hom.dfinsupp_sum_add_hom_apply],
rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]
dsimp only [DirectSum]
rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsuppSum_apply]
apply congrArg _
simp_rw [flip_apply]
funext x
erw [DFinsupp.sumAddHom_apply]
simp only [gMulHom, AddMonoidHom.dfinsuppSum_apply, flip_apply, coe_comp, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
Function.comp_apply, AddMonoidHom.compHom_apply_apply]
