English
Let R be a commutative semiring, M an additive commutative monoid, σ a type, and w: σ → M a weight function. Then the submodule of weighted homogeneous elements in MvPolynomial σ R carries a natural graded algebra structure, with grading indexed by M and with components given by weightedHomogeneousSubmodule R w m.
Русский
Пусть R — коммутативный полукольцо, M — аддитивная коммутативная абелева кость, σ — множество, w: σ → M — весовая функция. Тогда подпространство взвешенно однородных элементов в MvPolynomial σ R естественным образом образует градуированную алгебру, градуировка задаётся M, а компоненты задаются как weightedHomogeneousSubmodule R w m.
LaTeX
$$$\\operatorname{GradedAlgebra}\\bigl( \\operatorname{weightedHomogeneousSubmodule} R w \\bigr)\\,,$$$
Lean4
/-- Given a weight, `MvPolynomial` as a graded algebra -/
def weightedGradedAlgebra [DecidableEq M] : GradedAlgebra (weightedHomogeneousSubmodule R w)
where
toDecomposition := weightedDecomposition R w
toGradedMonoid := WeightedHomogeneousSubmodule.gradedMonoid
