English
The image of a singleton basis element under the decomposition map matches the corresponding direct sum element with the correct grade.
Русский
Образ единичного базисного элемента под отображением разложения совпадает с соответствующим элементом прямой суммы по нужному граду.
LaTeX
$$$\\text{decomposeAux}(\\delta_m \\cdot r) = \\text{DirectSum.of}(\\lambda i,\\text{gradeBy}(R,f,i))(f(m))\\; (\\delta_m r)$$$
Lean4
theorem decomposeAux_single (m : M) (r : R) :
decomposeAux f (Finsupp.single m r) =
DirectSum.of (fun i : ι => gradeBy R f i) (f m) ⟨Finsupp.single m r, single_mem_gradeBy _ _ _⟩ :=
by
refine (lift_single _ _ _).trans ?_
refine (DirectSum.of_smul R _ _ _).symm.trans ?_
apply DirectSum.of_eq_of_gradedMonoid_eq
refine Sigma.subtype_ext rfl ?_
refine (smul_single' _ _ _).trans ?_
rw [mul_one]
rfl
