English
For Φ a polynomial in idx with integer coefficients, there exists a unique φ : ℕ → MvPolynomial (idx × ℕ) ℤ such that ∀ n, bind₁ φ (wittPolynomial p ℤ n) = bind₁ (λ i, rename (Prod.mk i) (W_ℤ n)) Φ.
Русский
Для Φ, многочлена с целыми коэффициентами в idx, существует единственный φ : ℕ → MvPolynomial (idx × ℕ) ℤ такой, что для всех n выполняется bind₁ φ (wittPolynomial p ℤ n) = bind₁ (λ i, rename (Prod.mk i) (W_ℤ n)) Φ.
LaTeX
$$$\\exists!\\, φ : \\mathbb{N} \\to \\mathrm{MvPolynomial}_{(idx \\times \\mathbb{N})}(\\mathbb{Z}), \\; (\\forall n : \\mathbb{N}, \\; \\mathrm{bind}_1\\, φ (\\mathrm{wittPolynomial} p \\mathbb{Z} n) = \\mathrm{bind}_1 (\\lambda i : idx, \\ rename (Prod.mk i) (W_\\mathbb{Z} n)) Φ)$$$
Lean4
theorem wittStructureInt_existsUnique (Φ : MvPolynomial idx ℤ) :
∃! φ : ℕ → MvPolynomial (idx × ℕ) ℤ,
∀ n : ℕ, bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i : idx => rename (Prod.mk i) (W_ ℤ n)) Φ :=
⟨wittStructureInt p Φ, wittStructureInt_prop _ _, eq_wittStructureInt _ _⟩
