English
A similar injectivity holds for a general pair f,g with Witt polynomials, i.e., if for all n bind₁ f(wittPolynomial p n) = bind₁ g(wittPolynomial p n), then f = g.
Русский
Аналогично, если для всех n выполняется bind₁ f(wittPolynomial p n) = bind₁ g(wittPolynomial p n), то f = g.
LaTeX
$$$$\forall f,g:\mathbb{N}\to \mathrm{MvPolynomial}(\mathbb{N},\mathbb{Z}),\; (\forall n, \bind_1 f(\mathrm{wittPolynomial}(p, n)) = \bind_1 g(\mathrm{wittPolynomial}(p, n))) \Rightarrow f = g.$$$$
Lean4
theorem poly_eq_of_wittPolynomial_bind_eq [Fact p.Prime] (f g : ℕ → MvPolynomial ℕ ℤ)
(h : ∀ n, bind₁ f (wittPolynomial p _ n) = bind₁ g (wittPolynomial p _ n)) : f = g :=
by
ext1 n
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
rw [← funext_iff] at h
replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h
simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, bind₁_wittPolynomial_xInTermsOfW,
bind₁_X_right] using h
