English
Given a finite family of monomials monoms, genericPolyMap assigns to each index an element of the FreeCommRing encoding monomials with controlled supports; it yields an indexed family suitable for evaluating to any collection p of polynomials with support contained in monoms.
Русский
Дано конечное семейство мономов monoms; genericPolyMap задаёт для каждого индекса элемент из FreeCommRing, кодирующий мономы с контролируемой опорой; получается индексированная семья, пригодная для отображения в любую коллекцию полиномов с опорой в мономах.
LaTeX
$$$\\text{genericPolyMap}(\\text{monoms}) : ι \\to \\mathrm{FreeCommRing}(((\\Sigma i:ι, monoms i) \\oplus κ))$$$
Lean4
/-- Given a finite set of monomials `monoms : ι → Finset (κ →₀ ℕ)`, the
`genericPolyMap monoms` is an indexed collection of elements of the `FreeCommRing`,
that can be evaluated to any collection `p : ι → MvPolynomial κ R` of
polynomials such that `∀ i, (p i).support ⊆ monoms i`. -/
def genericPolyMap (monoms : ι → Finset (κ →₀ ℕ)) : ι → FreeCommRing ((Σ i : ι, monoms i) ⊕ κ) := fun i =>
(monoms i).attach.sum
(fun m => FreeCommRing.of (Sum.inl ⟨i, m⟩) * Finsupp.prod m.1 (fun j n => FreeCommRing.of (Sum.inr j) ^ n))
