English
Define eval by evaluating a family of polynomials φ at the coefficients of a family of Witt vectors x, obtaining a Witt vector: (eval φ x)_n = peval(φ(n), i ↦ x(i).coeff).
Русский
Определяем eval как оценку семейства многочленов φ по коэффициентам семейства Witt‑векторов x, получая Witt‑вектор: (eval φ x)_n = peval(φ(n), i ↦ x(i).coeff).
LaTeX
$$$\\forall k,\\; \\forall φ : \\mathbb{N} \\to \\mathrm{MvPolynomial}(\\mathrm{Fin\\,k} \\times \\mathbb{N})\\,\\mathbb{Z},\\ \\forall x : \\mathrm{Fin\\,k} \\to \\mathbb{W}R,\\n(\\mathrm{WittVector.eval}\\; φ\\; x)_{n} = \\mathrm{peval}(φ(n), i \\mapsto x(i).\\mathrm{coeff})$$$
Lean4
/-- Let `φ` be a family of polynomials, indexed by natural numbers, whose variables come from the
disjoint union of `k` copies of `ℕ`, and let `xᵢ` be a Witt vector for `0 ≤ i < k`.
`eval φ x` evaluates `φ` mapping the variable `X_(i, n)` to the `n`th coefficient of `xᵢ`.
Instantiating `φ` with certain polynomials defined in
`Mathlib/RingTheory/WittVector/StructurePolynomial.lean` establishes the
ring operations on `𝕎 R`. For example, `WittVector.wittAdd` is such a `φ` with `k = 2`;
evaluating this at `(x₀, x₁)` gives us the sum of two Witt vectors `x₀ + x₁`.
-/
def eval {k : ℕ} (φ : ℕ → MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → 𝕎 R) : 𝕎 R :=
mk p fun n => peval (φ n) fun i => (x i).coeff
