English
There exists a unique integer Witt-structure function producing the same outputs as the rational Witt-structure mapped via Int.cast, ensuring a canonical integer realization.
Русский
Существует уникальная целочисленная Witt-структурная функция, порождающая те же выводы, что рациональная Witt-структура после отображения Int.cast, обеспечивая каноническое целочисленное представление.
LaTeX
$$$\exists! \Psi : \mathbb{N} \to \mathrm{MvPolynomial}_{idx \times \mathbb{N}} \mathbb{Z},\ \forall n, bind_₁ \Psi (W_ ℤ n) = bind_₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ$$$
Lean4
/-- `wittStructureRat Φ` is a family of polynomials `ℕ → MvPolynomial (idx × ℕ) ℚ`
that are uniquely characterised by the property that
```
bind₁ (wittStructureRat p Φ) (wittPolynomial p ℚ n) =
bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℚ n))) Φ
```
In other words: evaluating the `n`-th Witt polynomial on the family `wittStructureRat Φ`
is the same as evaluating `Φ` on the (appropriately renamed) `n`-th Witt polynomials.
See `wittStructureRat_prop` for this property,
and `wittStructureRat_existsUnique` for the fact that `wittStructureRat`
gives the unique family of polynomials with this property.
These polynomials turn out to have integral coefficients,
but it requires some effort to show this.
See `wittStructureInt` for the version with integral coefficients,
and `map_wittStructureInt` for the fact that it is equal to `wittStructureRat`
when mapped to polynomials over the rationals. -/
noncomputable def wittStructureRat (Φ : MvPolynomial idx ℚ) (n : ℕ) : MvPolynomial (idx × ℕ) ℚ :=
bind₁ (fun k => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)
