mathlibdocumentation

ring_theory.witt_vector.is_poly

The is_poly predicate #

witt_vector.is_poly is a (type-valued) predicate on functions f : Π R, 𝕎 R → 𝕎 R. It asserts that there is a family of polynomials φ : ℕ → mv_polynomial ℕ ℤ, 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 is_poly.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₁ φ (witt_polynomial p _ n) = bind₁ ψ (witt_polynomial 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 witt_vector.frobenius and witt_vector.verschiebung is equal to multiplication by p.

On higher arity analogues #

Ideally, there should be a predicate is_polyₙ for functions of higher arity, together with is_polyₙ.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 attributes @[is_poly] and @[ghost_simps]. These are used in combination to discharge proofs of identities between polynomial functions.

Any atomic proof of is_poly or is_poly₂ (i.e. not taking additional is_poly arguments) should be tagged as @[is_poly].

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

@[ghost_simps]
lemma bind₁_frobenius_poly_witt_polynomial (n : ) :
bind₁ (frobenius_poly p) (witt_polynomial p  n) = (witt_polynomial p  (n+1))

Proofs of identities between polynomial functions will often follow the pattern

begin
ghost_calc _,
<minor preprocessing>,
ghost_simp
end