English
Canonical grade decomposition map from the monoid algebra to the direct sum of graded components.
Русский
Каноническая карта разложения по градам из моноидной алгебры в прямую сумму градуированных компонент.
LaTeX
$$$\\text{decomposeAux} : R[M] \\to_{\\mathbb{R}} \\bigoplus_{i \\in ι} \\text{gradeBy}(R,f,i)$$$
Lean4
/-- Auxiliary definition; the canonical grade decomposition, used to provide
`DirectSum.decompose`. -/
def decomposeAux : R[M] →ₐ[R] ⨁ i : ι, gradeBy R f i :=
AddMonoidAlgebra.lift R M _
{ toFun := fun m =>
DirectSum.of (fun i : ι => gradeBy R f i) (f m.toAdd) ⟨Finsupp.single m.toAdd 1, single_mem_gradeBy _ _ _⟩
map_one' := DirectSum.of_eq_of_gradedMonoid_eq (by congr 2 <;> simp)
map_mul' := fun i j => by
symm
dsimp only [toAdd_one, Eq.ndrec, Set.mem_setOf_eq, ne_eq, OneHom.toFun_eq_coe, OneHom.coe_mk, toAdd_mul]
convert DirectSum.of_mul_of (A := (fun i : ι => gradeBy R f i)) _ _
repeat { rw [AddMonoidHom.map_add]
}
simp only [SetLike.coe_gMul]
exact Eq.trans (by rw [one_mul]) (single_mul_single ..).symm }
