English
If two polynomial-parameterized Witt-vector operations agree on all ghost components, they are equal as functions.
Русский
Если две полиномиальные по координатам Witt операции согласованы по всем компонентам призраков, то они равны как функции.
LaTeX
$$$\forall f,g\;\text{IsPoly₂ } p f, \; \text{IsPoly₂ } p g, \; (\forall R\, x\, y\, n,\ ghostComponent_n(f\ x\ y)=ghostComponent_n(g\ x\ y)) \Rightarrow \forall R\ x\ y,\ f\ x\ y = g\ x\ y.$$$
Lean4
theorem ext [Fact p.Prime] {f g} (hf : IsPoly₂ p f) (hg : IsPoly₂ p g)
(h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), ghostComponent n (f x y) = ghostComponent n (g x y)) :
∀ (R) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y :=
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 (0, i)⟩) (mk p fun i => ⟨x (1, 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
ext ⟨b, _⟩
fin_cases b <;> simp only [coeff_mk, uncurry] <;>
rfl
-- unfortunately this is not universe polymorphic, merely because `f` isn't
