English
The operator decompose' assigns to a polynomial φ a direct-sum decomposition into weighted homogeneous pieces, indexed by M via the weight map.
Русский
Оператор decompose' присваивает полином φ разложение поDirectSum в взвешенно однородные части, индексируемые M через весовую карту.
LaTeX
$$$\\text{decompose}'(R,w)(\\varphi) = \\mathrm{DirectSum.mk}\\Big(\\lambda i. \\text{weightedHomogeneousSubmodule}(R,w,i), \\text{Finset.image}(\\text{weight}(w), \\operatorname{supp}(\\varphi)), \\lambda m. \\langle \\text{weightedHomogeneousComponent}(w,m,\\varphi), \\text{weightedHomogeneousComponent\_mem}(w,\\varphi,m)\\rangle\\Big)$$$
Lean4
/-- The `decompose'` argument of `weightedDecomposition`. -/
def decompose' [DecidableEq M] := fun φ : MvPolynomial σ R =>
DirectSum.mk (fun i : M => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (weight w) φ.support) fun m =>
⟨weightedHomogeneousComponent w m φ, weightedHomogeneousComponent_mem w φ m⟩
