# Documentation

Mathlib.RingTheory.WittVector.IsPoly

# The is_poly predicate #

WittVector.IsPoly is a (type-valued) predicate on functions f : Π R, 𝕎 R → 𝕎 R. It asserts that there is a family of polynomials φ : ℕ → MvPolynomial ℕ ℤ, such that the nth coefficient of f x is equal to φ n evaluated on the coefficients of x. Many operations on Witt vectors satisfy this predicate (or an analogue for higher arity functions). We say that such a function f is a polynomial function.

The power of satisfying this predicate comes from WittVector.IsPoly.ext. It shows that if φ and ψ witness that f and g are polynomial functions, then f = g not merely when φ = ψ, but in fact it suffices to prove

∀ n, bind₁ φ (wittPolynomial p _ n) = bind₁ ψ (wittPolynomial p _ n)


(in other words, when evaluating the Witt polynomials on φ and ψ, we get the same values) which will then imply φ = ψ and hence f = g.

Even though this sufficient condition looks somewhat intimidating, it is rather pleasant to check in practice; more so than direct checking of φ = ψ.

In practice, we apply this technique to show that the composition of WittVector.frobenius and WittVector.verschiebung is equal to multiplication by p.

## Main declarations #

• WittVector.IsPoly, WittVector.IsPoly₂: two predicates that assert that a unary/binary function on Witt vectors is polynomial in the coefficients of the input values.
• WittVector.IsPoly.ext, WittVector.IsPoly₂.ext: two polynomial functions are equal if their families of polynomials are equal after evaluating the Witt polynomials on them.
• WittVector.IsPoly.comp (+ many variants) show that unary/binary compositions of polynomial functions are polynomial.
• WittVector.idIsPoly, WittVector.negIsPoly, WittVector.addIsPoly₂, WittVector.mulIsPoly₂: several well-known operations are polynomial functions (for Verschiebung, Frobenius, and multiplication by p, see their respective files).

## On higher arity analogues #

Ideally, there should be a predicate IsPolyₙ for functions of higher arity, together with IsPolyₙ.comp that shows how such functions compose. Since mathlib does not have a library on composition of higher arity functions, we have only implemented the unary and binary variants so far. Nullary functions (a.k.a. constants) are treated as constant functions and fall under the unary case.

## Tactics #

There are important metaprograms defined in this file: the tactics ghost_simp and ghost_calc and the attribute @[ghost_simps]. These are used in combination to discharge proofs of identities between polynomial functions.

The ghost_calc tactic makes use of the IsPoly and IsPoly₂ typeclass and its instances. (In Lean 3, there was an @[is_poly] attribute to manage these instances, because typeclass resolution did not play well with function composition. This no longer seems to be an issue, so that such instances can be defined directly.)

Any lemma doing "ring equation rewriting" with polynomial functions should be tagged @[ghost_simps], e.g.

@[ghost_simps]
lemma bind₁_frobenius_poly_wittPolynomial (n : ℕ) :
bind₁ (frobenius_poly p) (wittPolynomial p ℤ n) = (wittPolynomial p ℤ (n+1))


Proofs of identities between polynomial functions will often follow the pattern

  ghost_calc _

ghost_simp

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]