English
If two polynomial maps f and g on Witt vectors agree on ghost components for all rings, then f = g.
Русский
Если два полиномных отображения f и g на Witt-вектора согласованы по всем ghost-компонентам для всех колец, тогда f = g.
LaTeX
$$$$\forall R\,[\text{CommRing }R],\ x\in 𝕎R,\ f x = g x \text{ if }\ ghostComponent_n(f x) = ghostComponent_n(g x)\ \forall n.$$$$
Lean4
theorem ext [Fact p.Prime] {f g} (hf : IsPoly p f) (hg : IsPoly p g)
(h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), ghostComponent n (f x) = ghostComponent n (g x)) :
∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x :=
by
obtain ⟨φ, hf⟩ := hf
obtain ⟨ψ, hg⟩ := hg
intros
ext n
rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]
intro k
apply MvPolynomial.funext
intro x
simp only [hom_bind₁]
specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k
simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
convert h using 1
all_goals
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
ext1
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
simp only [coeff_mk]; rfl
