mathlib3 documentation

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 #

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 #

source
meta def tactic.interactive.ghost_simp (lems : interactive.parse tactic.simp_arg_list) :
tactic unit

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

source
meta def tactic.interactive.ghost_calc (ids' : interactive.parse (lean.parser.many interactive.types.ident_)) :
tactic unit

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 #

source
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 : ℕ), ⇑(mv_polynomial.bind₁ f) (witt_polynomial p ℤ n) = ⇑(mv_polynomial.bind₁ g) (witt_polynomial p ℤ n)) :
f = g
source
theorem witt_vector.poly_eq_of_witt_polynomial_bind_eq (p : ℕ) [hp : fact (nat.prime p)] (f g : ℕ → mv_polynomial ℕ ℤ) (h : ∀ (n : ℕ), ⇑(mv_polynomial.bind₁ f) (witt_polynomial p ℤ n) = ⇑(mv_polynomial.bind₁ g) (witt_polynomial p ℤ n)) :
f = g
source
@[class]
structure witt_vector.is_poly (p : ℕ) (f : Π ⦃R : Type u_3⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector 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 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
source
@[protected, instance]
def witt_vector.id_is_poly (p : ℕ) :
witt_vector.is_poly p (λ (_x : Type u_1) (_x_1 : comm_ring _x), id)

The identity function on Witt vectors is a polynomial function.

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

The composition of polynomial functions is polynomial.

source
@[class]
structure witt_vector.is_poly₂ (p : ℕ) (f : Π ⦃R : Type u_3⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector 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 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₂
source
theorem witt_vector.is_poly₂.comp {p : ℕ} {h : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R} {f g : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R} (hh : witt_vector.is_poly₂ p h) (hf : witt_vector.is_poly p f) (hg : witt_vector.is_poly p g) :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), h (f x) (g y))

The composition of polynomial functions is polynomial.

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

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

source
theorem witt_vector.is_poly₂.diag {p : ℕ} {f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R} (hf : witt_vector.is_poly₂ p f) :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p 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.

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

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.

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

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.

source
meta def witt_vector.tactic.mk_comp_lemmas (n : name) :
tactic unit

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

source
meta def witt_vector.tactic.is_poly_attr  :
(user_attribute unit)

@[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.

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

The additive negation is a polynomial function on Witt vectors.

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

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

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

The coefficients of 1 : 𝕎 R as polynomials.

Equations
source
@[simp]
theorem witt_vector.bind₁_one_poly_witt_polynomial {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) :
⇑(mv_polynomial.bind₁ witt_vector.one_poly) (witt_polynomial p ℤ n) = 1
source
@[protected, instance]
def witt_vector.one_is_poly {p : ℕ} [hp : fact (nat.prime p)] :
witt_vector.is_poly p (λ (_x : Type u_1) (_x_1 : comm_ring _x) (_x_2 : witt_vector p _x), 1)

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

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

Addition of Witt vectors is a polynomial function.

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

Multiplication of Witt vectors is a polynomial function.

source
@[instance]
def witt_vector.mul_is_poly₂.comp_diag {p : ℕ} [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R} [hf : witt_vector.is_poly p f] [hg : witt_vector.is_poly p g] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R) (x : witt_vector p R), f x * g x)
source
@[instance]
def witt_vector.mul_is_poly₂.comp₂_i {p : ℕ} [fact (nat.prime p)] {f g : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R} [hf : witt_vector.is_poly p f] [hg : witt_vector.is_poly p g] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), f x * g y)
source
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 : comm_ring R], witt_vector p R → witt_vector p R} (hf : witt_vector.is_poly p f) (g : R →+* S) (x : witt_vector p R) :
⇑(witt_vector.map g) (f x) = f (⇑(witt_vector.map g) x)
source
@[protected, instance]
def witt_vector.is_poly₂.inhabited {p : ℕ} [fact (nat.prime p)] :
inhabited (witt_vector.is_poly₂ p (λ (_x : Type u_1) (_x_1 : comm_ring _x), has_add.add))
Equations
source
theorem witt_vector.is_poly₂.comp_left {p : ℕ} {g : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R} {f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R} (hg : witt_vector.is_poly₂ p g) (hf : witt_vector.is_poly p f) :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), g (f x) y)

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

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

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

source
theorem witt_vector.is_poly₂.ext {p : ℕ} [hp : fact (nat.prime p)] {f g : Π ⦃R : Type u⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R} (hf : witt_vector.is_poly₂ p f) (hg : witt_vector.is_poly₂ p g) (h : ∀ (R : Type u) [_Rcr : comm_ring R] (x y : witt_vector p R) (n : ℕ), ⇑(witt_vector.ghost_component n) (f x y) = ⇑(witt_vector.ghost_component n) (g x y)) (R : Type u) [comm_ring R] (x y : witt_vector p R) :
f x y = g x y
source
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 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R} (hf : witt_vector.is_poly₂ p f) (g : R →+* S) (x y : witt_vector p R) :
⇑(witt_vector.map g) (f x y) = f (⇑(witt_vector.map g) x) (⇑(witt_vector.map g) y)