The IsPoly 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 _
  <minor preprocessing>
  ghost_simp

References

• [Hazewinkel, Witt Vectors][Haze09]

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

The IsPoly predicate

theorem WittVector.poly_eq_of_wittPolynomial_bind_eq' (p : ℕ) {idx : Type u_1} [Fact (Nat.Prime p)] (f : ℕ → MvPolynomial (idx × ℕ) ℤ) (g : ℕ → MvPolynomial (idx × ℕ) ℤ) (h : ∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)) : f = g

theorem WittVector.poly_eq_of_wittPolynomial_bind_eq (p : ℕ) [Fact (Nat.Prime p)] (f : ℕ → MvPolynomial ℕ ℤ) (g : ℕ → MvPolynomial ℕ ℤ) (h : ∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)) : f = g

class WittVector.IsPoly (p : ℕ) (f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p 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 WittVector.IsPoly₂ for the binary variant.

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.)

• mk' :: (
• poly : ∃ (φ : ℕ → MvPolynomial ℕ ℤ), ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : WittVector p R), (f x).coeff = fun (n : ℕ) => (MvPolynomial.aeval x.coeff) (φ n)
• )

theorem WittVector.IsPoly.poly {p : ℕ} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [self : WittVector.IsPoly p f] : ∃ (φ : ℕ → MvPolynomial ℕ ℤ), ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : WittVector p R), (f x).coeff = fun (n : ℕ) => (MvPolynomial.aeval x.coeff) (φ n)

instance WittVector.idIsPoly (p : ℕ) : WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) => id

The identity function on Witt vectors is a polynomial function.

Equations

• ⋯ = ⋯

instance WittVector.idIsPolyI' (p : ℕ) : WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) (a : WittVector p x) => a

Equations

• ⋯ = ⋯

instance WittVector.IsPoly.instInhabitedId (p : ℕ) : Inhabited (WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) => id)

Equations

• WittVector.IsPoly.instInhabitedId p = { default := ⋯ }

theorem WittVector.IsPoly.ext {p : ℕ} [Fact (Nat.Prime p)] {f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} {g : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} (hf : WittVector.IsPoly p f) (hg : WittVector.IsPoly p g) (h : ∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (n : ℕ), (WittVector.ghostComponent n) (f x) = (WittVector.ghostComponent n) (g x)) (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) : f x = g x

instance WittVector.IsPoly.comp {p : ℕ} {g : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [hg : WittVector.IsPoly p g] [hf : WittVector.IsPoly p f] : WittVector.IsPoly p fun (R : Type u_2) (_Rcr : CommRing R) => g ∘ f

The composition of polynomial functions is polynomial.

Equations

• ⋯ = ⋯

class WittVector.IsPoly₂ (p : ℕ) (f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p 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 WittVector.IsPoly for the unary variant.

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.)

• mk' :: (
• poly : ∃ (φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ), ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : WittVector p R), (f x y).coeff = fun (n : ℕ) => WittVector.peval (φ n) ![x.coeff, y.coeff]
• )

theorem WittVector.IsPoly₂.poly {p : ℕ} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} [self : WittVector.IsPoly₂ p f] : ∃ (φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ), ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : WittVector p R), (f x y).coeff = fun (n : ℕ) => WittVector.peval (φ n) ![x.coeff, y.coeff]

instance WittVector.IsPoly₂.comp {p : ℕ} {h : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} {g : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [hh : WittVector.IsPoly₂ p h] [hf : WittVector.IsPoly p f] [hg : WittVector.IsPoly p g] : WittVector.IsPoly₂ p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : WittVector p x) => h (f x_1) (g y)

The composition of polynomial functions is polynomial.

Equations

• ⋯ = ⋯

instance WittVector.IsPoly.comp₂ {p : ℕ} {g : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} [hg : WittVector.IsPoly p g] [hf : WittVector.IsPoly₂ p f] : WittVector.IsPoly₂ p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 y : WittVector p x) => g (f x_1 y)

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

Equations

• ⋯ = ⋯

instance WittVector.IsPoly₂.diag {p : ℕ} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} [hf : WittVector.IsPoly₂ p f] : WittVector.IsPoly p fun (x : Type u_2) (_Rcr : CommRing x) (x_1 : WittVector p x) => f x_1 x_1

The diagonal fun x ↦ f x x of a polynomial function f is polynomial.

Equations

• ⋯ = ⋯

instance WittVector.negIsPoly {p : ℕ} [Fact (Nat.Prime p)] : WittVector.IsPoly p fun (R : Type u_2) (x : CommRing R) => Neg.neg

The additive negation is a polynomial function on Witt vectors.

Equations

• ⋯ = ⋯

instance WittVector.zeroIsPoly {p : ℕ} [Fact (Nat.Prime p)] : WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : WittVector p x) => 0

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

Equations

• ⋯ = ⋯

@[simp]

theorem WittVector.bind₁_zero_wittPolynomial {p : ℕ} {R : Type u} [CommRing R] [Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.bind₁ 0) (wittPolynomial p R n) = 0

def WittVector.onePoly (n : ℕ) : MvPolynomial ℕ ℤ

The coefficients of 1 : 𝕎 R as polynomials.

Equations

• WittVector.onePoly n = if n = 0 then 1 else 0

@[simp]

theorem WittVector.bind₁_onePoly_wittPolynomial {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : (MvPolynomial.bind₁ WittVector.onePoly) (wittPolynomial p ℤ n) = 1

instance WittVector.oneIsPoly {p : ℕ} [Fact (Nat.Prime p)] : WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : WittVector p x) => 1

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

Equations

• ⋯ = ⋯

instance WittVector.addIsPoly₂ {p : ℕ} [Fact (Nat.Prime p)] : WittVector.IsPoly₂ p fun (x : Type u_2) (x_1 : CommRing x) (x1 x2 : WittVector p x) => x1 + x2

Addition of Witt vectors is a polynomial function.

Equations

• ⋯ = ⋯

instance WittVector.mulIsPoly₂ {p : ℕ} [Fact (Nat.Prime p)] : WittVector.IsPoly₂ p fun (x : Type u_2) (x_1 : CommRing x) (x1 x2 : WittVector p x) => x1 * x2

Multiplication of Witt vectors is a polynomial function.

Equations

• ⋯ = ⋯

theorem WittVector.IsPoly.map {p : ℕ} {R : Type u} {S : Type u} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] {f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} (hf : WittVector.IsPoly p f) (g : R →+* S) (x : WittVector p R) : (WittVector.map g) (f x) = f ((WittVector.map g) x)

instance WittVector.IsPoly₂.instInhabitedHAdd {p : ℕ} [Fact (Nat.Prime p)] : Inhabited (WittVector.IsPoly₂ p fun (x : Type u_2) (x_1 : CommRing x) (x1 x2 : WittVector p x) => x1 + x2)

Equations

• WittVector.IsPoly₂.instInhabitedHAdd = { default := ⋯ }

theorem WittVector.IsPoly₂.compLeft {p : ℕ} {g : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [WittVector.IsPoly₂ p g] [WittVector.IsPoly p f] : WittVector.IsPoly₂ p fun (_R : Type u_2) (_Rcr : CommRing _R) (x y : WittVector p _R) => g (f x) y

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

theorem WittVector.IsPoly₂.compRight {p : ℕ} {g : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} {f : ⦃R : Type u_2⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [WittVector.IsPoly₂ p g] [WittVector.IsPoly p f] : WittVector.IsPoly₂ p fun (_R : Type u_2) (_Rcr : CommRing _R) (x y : WittVector p _R) => g x (f y)

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

theorem WittVector.IsPoly₂.ext {p : ℕ} [Fact (Nat.Prime p)] {f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} {g : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} (hf : WittVector.IsPoly₂ p f) (hg : WittVector.IsPoly₂ p g) (h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : WittVector p R) (n : ℕ), (WittVector.ghostComponent n) (f x y) = (WittVector.ghostComponent n) (g x y)) (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (y : WittVector p R) : f x y = g x y

theorem WittVector.IsPoly₂.map {p : ℕ} {R : Type u} {S : Type u} [CommRing R] [CommRing S] [Fact (Nat.Prime p)] {f : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R} (hf : WittVector.IsPoly₂ p f) (g : R →+* S) (x : WittVector p R) (y : WittVector p R) : (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

def WittVector.Tactic.ghostSimp : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

def WittVector.Tactic.ghostCalc : Lean.ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.