# mathlib3documentation

ring_theory.witt_vector.is_poly

# The is_poly predicate #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## Main declarations #

• witt_vector.is_poly, witt_vector.is_poly₂: two predicates that assert that a unary/binary function on Witt vectors is polynomial in the coefficients of the input values.
• witt_vector.is_poly.ext, witt_vector.is_poly₂.ext: two polynomial functions are equal if their families of polynomials are equal after evaluating the Witt polynomials on them.
• witt_vector.is_poly.comp (+ many variants) show that unary/binary compositions of polynomial functions are polynomial.
• witt_vector.id_is_poly, witt_vector.neg_is_poly, witt_vector.add_is_poly₂, witt_vector.mul_is_poly₂: 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 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


## References #

A macro for a common simplification when rewriting with ghost component equations.

ghost_calc is a tactic for proving identities between polynomial functions. Typically, when faced with a goal like

∀ (x y : 𝕎 R), verschiebung (x * frobenius y) = verschiebung x * y


you can

1. call ghost_calc
2. do a small amount of manual work -- maybe nothing, maybe rintro, etc
3. call ghost_simp

and this will close the goal.

ghost_calc cannot detect whether you are dealing with unary or binary polynomial functions. You must give it arguments to determine this. If you are proving a universally quantified goal like the above, call ghost_calc _ _. If the variables are introduced already, call ghost_calc x y. In the unary case, use ghost_calc _ or ghost_calc x.

ghost_calc is a light wrapper around type class inference. All it does is apply the appropriate extensionality lemma and try to infer the resulting goals. This is subtle and Lean's elaborator doesn't like it because of the HO unification involved, so it is easier (and prettier) to put it in a tactic script.

### The is_poly predicate #

theorem witt_vector.poly_eq_of_witt_polynomial_bind_eq' (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (f g : mv_polynomial (idx × ) ) (h : (n : ), n) = n)) :
f = g
theorem witt_vector.poly_eq_of_witt_polynomial_bind_eq (p : ) [hp : fact (nat.prime p)] (f g : ) (h : (n : ), n) = n)) :
f = g
@[class]
structure witt_vector.is_poly (p : ) (f : Π ⦃R : Type u_3⦄ [_inst_3 : , R R) :
Prop

A function f : Π R, 𝕎 R → 𝕎 R that maps Witt vectors to Witt vectors over arbitrary base rings is said to be polynomial if there is a family of polynomials φₙ over ℤ such that the nth coefficient of f x is given by evaluating φₙ at the coefficients of x.

See also witt_vector.is_poly₂ for the binary variant.

The ghost_calc tactic treats is_poly as a type class, and the @[is_poly] attribute derives certain specialized composition instances for declarations of type is_poly f. For the most part, users are not expected to treat is_poly as a class.

Instances of this typeclass
Instances of other typeclasses for witt_vector.is_poly
@[protected, instance]
def witt_vector.id_is_poly (p : ) :
(λ (_x : Type u_1) (_x_1 : comm_ring _x), id)

The identity function on Witt vectors is a polynomial function.

@[protected, instance]
def witt_vector.id_is_poly_i' (p : ) :
(λ (_x : Type u_1) (_x_1 : comm_ring _x) (a : _x), a)
@[protected, instance]
def witt_vector.is_poly.inhabited (p : ) :
inhabited (λ (_x : Type u_1) (_x_1 : comm_ring _x), id))
Equations
theorem witt_vector.is_poly.ext {p : } [hp : fact (nat.prime p)] {f g : Π ⦃R : Type u⦄ [_inst_3 : , R R} (hf : f) (hg : g) (h : (R : Type u) [_Rcr : (x : R) (n : ), (f x) = (g x)) (R : Type u) [comm_ring R] (x : R) :
f x = g x
theorem witt_vector.is_poly.comp {p : } {g f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} (hg : g) (hf : f) :
(λ (R : Type u_1) (_Rcr : , g f)

The composition of polynomial functions is polynomial.

@[class]
structure witt_vector.is_poly₂ (p : ) (f : Π ⦃R : Type u_3⦄ [_inst_3 : , R R R) :
Prop

A binary function f : Π R, 𝕎 R → 𝕎 R → 𝕎 R on Witt vectors is said to be polynomial if there is a family of polynomials φₙ over ℤ such that the nth coefficient of f x y is given by evaluating φₙ at the coefficients of x and y.

See also witt_vector.is_poly for the unary variant.

The ghost_calc tactic treats is_poly₂ as a type class, and the @[is_poly] attribute derives certain specialized composition instances for declarations of type is_poly₂ f. For the most part, users are not expected to treat is_poly₂ as a class.

Instances of this typeclass
Instances of other typeclasses for witt_vector.is_poly₂
theorem witt_vector.is_poly₂.comp {p : } {h : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R} {f g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} (hh : h) (hf : f) (hg : g) :
(λ (R : Type u_1) (_Rcr : (x y : R), h (f x) (g y))

The composition of polynomial functions is polynomial.

theorem witt_vector.is_poly.comp₂ {p : } {g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} {f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R} (hg : g) (hf : f) :
(λ (R : Type u_1) (_Rcr : (x y : R), g (f x y))

The composition of a polynomial function with a binary polynomial function is polynomial.

theorem witt_vector.is_poly₂.diag {p : } {f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R} (hf : f) :
(λ (R : Type u_1) (_Rcr : (x : R), f x x)

The diagonal λ x, f x x of a polynomial function f is polynomial.

### The @[is_poly] attribute #

This attribute is used to derive specialized composition instances for is_poly and is_poly₂ declarations.

meta def witt_vector.tactic.mk_poly_comp_lemmas (n : name) (vars : list expr) (p : expr) :

If n is the name of a lemma with opened type ∀ vars, is_poly p _, mk_poly_comp_lemmas n vars p adds composition instances to the environment n.comp_i and n.comp₂_i.

meta def witt_vector.tactic.mk_poly₂_comp_lemmas (n : name) (vars : list expr) (p : expr) :

If n is the name of a lemma with opened type ∀ vars, is_poly₂ p _, mk_poly₂_comp_lemmas n vars p adds composition instances to the environment n.comp₂_i and n.comp_diag.

The after_set function for @[is_poly]. Calls mk_poly(₂)_comp_lemmas.

@[is_poly] is applied to lemmas of the form is_poly f φ or is_poly₂ f φ. These lemmas should not be tagged as instances, and only atomic is_poly defs should be tagged: composition lemmas should not. Roughly speaking, lemmas that take is_poly proofs as arguments should not be tagged.

Type class inference struggles with function composition, and the higher order unification problems involved in inferring is_poly proofs are complex. The standard style writing these proofs by hand doesn't work very well. Instead, we construct the type class hierarchy "under the hood", with limited forms of composition.

Applying @[is_poly] to a lemma creates a number of instances. Roughly, if the tagged lemma is a proof of is_poly f φ, the instances added have the form

∀ g ψ, [is_poly g ψ] → is_poly (f ∘ g) _


Since f is fixed in this instance, it restricts the HO unification needed when the instance is applied. Composition lemmas relating is_poly with is_poly₂ are also added. id_is_poly is an atomic instance.

The user-written lemmas are not instances. Users should be able to assemble is_poly proofs by hand "as normal" if the tactic fails.

### is_poly instances #

These are not declared as instances at the top level, but the @[is_poly] attribute adds instances based on each one. Users are expected to use the non-instance versions manually.

@[instance]
def witt_vector.neg_is_poly.comp₂_i {p : } [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : (x y : R), (λ (R : Type u_1) (_x : , has_neg.neg) R _Rcr (f x y))
@[instance]
def witt_vector.neg_is_poly.comp_i {p : } [hp : fact (nat.prime p)] (f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R) [hf : f] :
(λ (R : Type u_1) (_Rcr : , (λ (R : Type u_1) (_x : , has_neg.neg) R _Rcr f)
theorem witt_vector.neg_is_poly {p : } [hp : fact (nat.prime p)] :
(λ (R : Type u_1) (_x : , has_neg.neg)

The additive negation is a polynomial function on Witt vectors.

@[protected, instance]
def witt_vector.zero_is_poly {p : } [hp : fact (nat.prime p)] :
(λ (_x : Type u_1) (_x_1 : comm_ring _x) (_x_2 : _x), 0)

The function that is constantly zero on Witt vectors is a polynomial function.

@[simp]
theorem witt_vector.bind₁_zero_witt_polynomial {p : } {R : Type u} [hp : fact (nat.prime p)] [comm_ring R] (n : ) :
R n) = 0
noncomputable def witt_vector.one_poly (n : ) :

The coefficients of 1 : 𝕎 R as polynomials.

Equations
@[simp]
@[protected, instance]
def witt_vector.one_is_poly {p : } [hp : fact (nat.prime p)] :
(λ (_x : Type u_1) (_x_1 : comm_ring _x) (_x_2 : _x), 1)

The function that is constantly one on Witt vectors is a polynomial function.

@[instance]
def witt_vector.add_is_poly₂.comp₂_i {p : } [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} [hf : f] [hg : g] :
(λ (R : Type u_1) (_Rcr : (x y : R), f x + g y)
@[instance]
def witt_vector.add_is_poly₂.comp_diag {p : } [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} [hf : f] [hg : g] :
(λ (R : Type u_1) (_Rcr : (x : R), f x + g x)
theorem witt_vector.add_is_poly₂ {p : } [fact (nat.prime p)] :

Addition of Witt vectors is a polynomial function.

theorem witt_vector.mul_is_poly₂ {p : } [fact (nat.prime p)] :
(λ (_x : Type u_1) (_x_1 : comm_ring _x), has_mul.mul)

Multiplication of Witt vectors is a polynomial function.

@[instance]
def witt_vector.mul_is_poly₂.comp_diag {p : } [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} [hf : f] [hg : g] :
(λ (R : Type u_1) (_Rcr : (x : R), f x * g x)
@[instance]
def witt_vector.mul_is_poly₂.comp₂_i {p : } [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} [hf : f] [hg : g] :
(λ (R : Type u_1) (_Rcr : (x y : R), f x * g y)
theorem witt_vector.is_poly.map {p : } {R S : Type u} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] {f : Π ⦃R : Type u⦄ [_inst_3 : , R R} (hf : f) (g : R →+* S) (x : R) :
(f x) = f ( x)
@[protected, instance]
def witt_vector.is_poly₂.inhabited {p : } [fact (nat.prime p)] :
Equations
theorem witt_vector.is_poly₂.comp_left {p : } {g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R} {f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} (hg : g) (hf : f) :
(λ (R : Type u_1) (_Rcr : (x y : R), g (f x) y)

The composition of a binary polynomial function with a unary polynomial function in the first argument is polynomial.

theorem witt_vector.is_poly₂.comp_right {p : } {g : Π ⦃R : Type u_1⦄ [_inst_3 : , R R R} {f : Π ⦃R : Type u_1⦄ [_inst_3 : , R R} (hg : g) (hf : f) :
(λ (R : Type u_1) (_Rcr : (x y : R), g x (f y))

The composition of a binary polynomial function with a unary polynomial function in the second argument is polynomial.

theorem witt_vector.is_poly₂.ext {p : } [hp : fact (nat.prime p)] {f g : Π ⦃R : Type u⦄ [_inst_3 : , R R R} (hf : f) (hg : g) (h : (R : Type u) [_Rcr : (x y : R) (n : ), (f x y) = (g x y)) (R : Type u) [comm_ring R] (x y : R) :
f x y = g x y
theorem witt_vector.is_poly₂.map {p : } {R S : Type u} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] {f : Π ⦃R : Type u⦄ [_inst_3 : , R R R} (hf : f) (g : R →+* S) (x y : R) :
(f x y) = f ( x) ( y)