English
Given a family monoms and a function f on a sum type built from these monoms and κ, the lift of f along the generic polynomial map coincides with a specific evaluation of f, where the arguments are assembled from the inverse isomorphism applied to the left-hand component. This expresses the compatibility of the lifting operation with the mv-polynomial representation.
Русский
Дано семейство monoms и функция f на сумма́льном типе, построенном из этих monoms и κ. Подъём f вдоль общей полиномной карты совпадает с конкретной оценкой f, где аргументы собираются из обратного изоморфизма, применённого к левой части. Отражает совместимость подъёма с представлением mv-полиномов.
LaTeX
$$$\\mathrm{lift}\; f\\; (\\text{genericPolyMap } monoms\\; i) = \\mathrm{MvPolynomial.eval}(f \\circ \\mathrm{Sum.inr})\\big(((\\mathrm mvPolynomialSupportLEEquiv\\; monoms).symm (f \\circ \\mathrm Sum.inl)).1\\; i\\big)$$$
Lean4
@[simp]
theorem lift_genericPolyMap [DecidableEq κ] [CommRing R] [DecidableEq R] (monoms : ι → Finset (κ →₀ ℕ))
(f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R) (i : ι) :
FreeCommRing.lift f (genericPolyMap monoms i) =
MvPolynomial.eval (f ∘ Sum.inr) (((mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)).1 i) :=
by
simp only [genericPolyMap, map_sum, map_mul, lift_of, support, mvPolynomialSupportLEEquiv, coeff, Finset.sum_filter,
MvPolynomial.eval_eq, ne_eq, Function.comp, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]
conv_rhs => rw [← Finset.sum_attach]
refine Finset.sum_congr rfl ?_
intro m _
simp only [Finsupp.prod, map_prod, map_pow, lift_of, Subtype.coe_eta, Finset.coe_mem, exists_prop, true_and,
dite_eq_ite, ite_true, ite_not]
split_ifs with h0 <;> simp_all
