English
Let R be a commutative semiring, S1 a type, s a function from S1 to R, y an element of R, and f a multivariate polynomial in the variables indexed by Option S1 with coefficients in R. Then the evaluation of f with the map that sends None to y and Some x to the evaluation at x via s equals the evaluation at y of the polynomial obtained by first transforming f via the left-option equivalence and then applying the evaluation map on S1.
Русский
Пусть R — коммутативная полускольная кольцо, S1 — множество (тип), s : S1 → R, y ∈ R, и f — многочлен с переменными в Option S1 над R. Тогда вычисление f по отображению, отправляющему None в y, а Some x — в s(x), равно вычислению при y полинома, полученного сначала из f через левостороннюю опцию-эквивалентность, а затем через отображение eval.
LaTeX
$$$ \\operatorname{eval}\\bigl(\\lambda x.\\,\\operatorname{Option.elim}\\, x\\ y\\ s\\bigr) f \;=\\; \\operatorname{Polynomial}.eval\\ y\\left( \\operatorname{Polynomial}.map(\\operatorname{eval} s)\\bigl(\\operatorname{optionEquivLeft} R S_1\\;f\\bigr)\\right)$$$
Lean4
theorem optionEquivLeft_elim_eval (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) :
eval (fun x ↦ Option.elim x y s) f = Polynomial.eval y (Polynomial.map (eval s) (optionEquivLeft R S₁ f)) := by
-- turn this into a def `Polynomial.mapAlgHom`
let φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
{ Polynomial.mapRingHom (eval s) with
commutes' := fun r => by
convert Polynomial.map_C (eval s)
exact (eval_C _).symm }
change aeval (fun x ↦ Option.elim x y s) f = (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f
congr 2
apply MvPolynomial.algHom_ext
rw [Option.forall]
simp only [aeval_X, Option.elim_none, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
AlgHom.coe_mk, coe_mapRingHom, AlgHom.coe_coe, comp_apply, optionEquivLeft_apply, Polynomial.map_X,
Polynomial.eval_X, Option.elim_some, Polynomial.map_C, eval_X, Polynomial.eval_C, implies_true, and_self, φ]
