English
A further refinement ensuring the renaming is compatible with the p-adic structure via a map to rational polynomials.
Русский
Дальнейшее уточнение обеспечивает совместимость переименования с p-адической структурой через переход к рациональным полиномам.
LaTeX
$$$bind₁ (fun b => rename (fun i => (b,i)) (expand p (W_ ℚ n))) Φ = bind₁ (fun i => expand p (wittStructureRat p Φ i)) (W_ ℚ n)$$$
Lean4
theorem wittStructureRat_existsUnique (Φ : MvPolynomial idx ℚ) :
∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ, ∀ n : ℕ, bind₁ φ (W_ ℚ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℚ n)) Φ :=
by
refine ⟨wittStructureRat p Φ, ?_, ?_⟩
· intro n; apply wittStructureRat_prop
· intro φ H
funext n
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
rw [bind₁_bind₁]
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl
