English
Let p be a prime. For Φ a polynomial with integer coefficients in idx, and φ : ℕ → MvPolynomial (idx × ℕ) ℤ, if for every n we have bind₁ φ (wittPolynomial p ℤ n) = bind₁ (λ i, rename (Prod.mk i) (W_ ℤ n)) Φ, then φ equals the Witt-structure map wittStructureInt p Φ.
Русский
Пусть p — простое число. Для Φ, многочлена с целыми коэффициентами в idx, и функции φ : ℕ → MvPolynomial (idx × ℕ) ℤ, если для каждого n выполняется равенство bind₁ φ (wittPolynomial p ℤ n) = bind₁ (λ i, rename (Prod.mk i) (W_ ℤ n)) Φ, то φ совпадает с Witt-структурой, то есть φ = wittStructureInt p Φ.
LaTeX
$$$\\forall (p : \\mathbb{N}) (idx : Type*), (Φ : \\mathrm{MvPolynomial}_{idx}(\\mathbb{Z})), (\\phi : \\mathbb{N} \\to \\mathrm{MvPolynomial}_{(idx \\times \\mathbb{N})}(\\mathbb{Z})), (∀ n, \\mathrm{bind}_1 \\phi (\\mathrm{wittPolynomial} \\\\ p \\\\ \\mathbb{Z} \\\\ n) = \\mathrm{bind}_1 (\\lambda i: \\mathrm{rename}(\\mathrm{Prod.mk}\\ i)(W_\\mathbb{Z} n)) \\ Φ) \\Rightarrow \\ φ = \\mathrm{wittStructureInt} p Φ$$$
Lean4
theorem eq_wittStructureInt (Φ : MvPolynomial idx ℤ) (φ : ℕ → MvPolynomial (idx × ℕ) ℤ)
(h : ∀ n, bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ) :
φ = wittStructureInt p Φ := by
funext k
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
rw [map_wittStructureInt]
-- Porting note: was `refine' congr_fun _ k`
revert k
refine congr_fun ?_
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
· intro n
specialize h n
apply_fun map (Int.castRingHom ℚ) at h
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
AlgHom.coe_toRingHom] using h
· intro n; apply wittStructureRat_prop
