mathlib3 documentation

ring_theory.witt_vector.basic

Witt vectors #

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

This file verifies that the ring operations on witt_vector p R satisfy the axioms of a commutative ring.

Main definitions #

witt_vector.map: lifts a ring homomorphism R →+* S to a ring homomorphism 𝕎 R →+* 𝕎 S.
witt_vector.ghost_component n x: evaluates the nth Witt polynomial on the first n coefficients of x, producing a value in R. This is a ring homomorphism.
witt_vector.ghost_map: a ring homomorphism 𝕎 R →+* (ℕ → R), obtained by packaging all the ghost components together. If p is invertible in R, then the ghost map is an equivalence, which we use to define the ring operations on 𝕎 R.
witt_vector.comm_ring: the ring structure induced by the ghost components.

Notation #

We use notation 𝕎 R, entered \bbW, for the Witt vectors over R.

Implementation details #

As we prove that the ghost components respect the ring operations, we face a number of repetitive proofs. To avoid duplicating code we factor these proofs into a custom tactic, only slightly more powerful than a tactic macro. This tactic is not particularly useful outside of its applications in this file.

References #

def witt_vector.map_fun {p : ℕ} {α : Type u_4} {β : Type u_5} (f : α → β) :

witt_vector p α → witt_vector p β

f : α → β induces a map from 𝕎 α to 𝕎 β by applying f componentwise. If f is a ring homomorphism, then so is f, see witt_vector.map f.

Equations

witt_vector.map_fun f = λ (x : witt_vector p α), {coeff := f ∘ x.coeff}

theorem witt_vector.map_fun.injective {p : ℕ} {α : Type u_4} {β : Type u_5} (f : α → β) (hf : function.injective f) :

function.injective (witt_vector.map_fun f)

theorem witt_vector.map_fun.surjective {p : ℕ} {α : Type u_4} {β : Type u_5} (f : α → β) (hf : function.surjective f) :

function.surjective (witt_vector.map_fun f)

meta def witt_vector.map_fun.map_fun_tac :

Auxiliary tactic for showing that map_fun respects the ring operations.

theorem witt_vector.map_fun.zero {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) :

witt_vector.map_fun ⇑f 0 = 0

theorem witt_vector.map_fun.one {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) :

witt_vector.map_fun ⇑f 1 = 1

theorem witt_vector.map_fun.add {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x y : witt_vector p R) :

witt_vector.map_fun ⇑f (x + y) = witt_vector.map_fun ⇑f x + witt_vector.map_fun ⇑f y

theorem witt_vector.map_fun.sub {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x y : witt_vector p R) :

witt_vector.map_fun ⇑f (x - y) = witt_vector.map_fun ⇑f x - witt_vector.map_fun ⇑f y

theorem witt_vector.map_fun.mul {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x y : witt_vector p R) :

witt_vector.map_fun ⇑f (x * y) = witt_vector.map_fun ⇑f x * witt_vector.map_fun ⇑f y

theorem witt_vector.map_fun.neg {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) :

witt_vector.map_fun ⇑f (-x) = -witt_vector.map_fun ⇑f x

theorem witt_vector.map_fun.nsmul {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) (n : ℕ) :

witt_vector.map_fun ⇑f (n • x) = n • witt_vector.map_fun ⇑f x

theorem witt_vector.map_fun.zsmul {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) (z : ℤ) :

witt_vector.map_fun ⇑f (z • x) = z • witt_vector.map_fun ⇑f x

theorem witt_vector.map_fun.pow {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) (n : ℕ) :

witt_vector.map_fun ⇑f (x ^ n) = witt_vector.map_fun ⇑f x ^ n

theorem witt_vector.map_fun.nat_cast {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (n : ℕ) :

witt_vector.map_fun ⇑f ↑n = ↑n

theorem witt_vector.map_fun.int_cast {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (n : ℤ) :

witt_vector.map_fun ⇑f ↑n = ↑n

meta def tactic.interactive.ghost_fun_tac (φ fn : interactive.parse (lean.parser.pexpr std.prec.max)) :

An auxiliary tactic for proving that ghost_fun respects the ring operations.

theorem witt_vector.matrix_vec_empty_coeff {p : ℕ} {R : Type u_1} (i : fin 0) (j : ℕ) :

(matrix.vec_empty i).coeff j = matrix.vec_empty i j

@[protected, instance]

noncomputable def witt_vector.comm_ring (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] :

comm_ring (witt_vector p R)

The commutative ring structure on 𝕎 R.

Equations

witt_vector.comm_ring p R = function.surjective.comm_ring (witt_vector.map_fun ⇑(mv_polynomial.counit R)) _ _ _ _ _ _ _ _ _ _ _ _

def witt_vector.map {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) :

witt_vector p R →+* witt_vector p S

witt_vector.map f is the ring homomorphism 𝕎 R →+* 𝕎 S naturally induced by a ring homomorphism f : R →+* S. It acts coefficientwise.

Equations

witt_vector.map f = {to_fun := witt_vector.map_fun ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

theorem witt_vector.map_injective {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.injective ⇑f) :

function.injective ⇑(witt_vector.map f)

theorem witt_vector.map_surjective {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) :

function.surjective ⇑(witt_vector.map f)

@[simp]

theorem witt_vector.map_coeff {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : fact (nat.prime p)] [comm_ring R] [comm_ring S] (f : R →+* S) (x : witt_vector p R) (n : ℕ) :

(⇑(witt_vector.map f) x).coeff n = ⇑f (x.coeff n)

noncomputable def witt_vector.ghost_map {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :

witt_vector p R →+* ℕ → R

witt_vector.ghost_map is a ring homomorphism that maps each Witt vector to the sequence of its ghost components.

Equations

witt_vector.ghost_map = {to_fun := ghost_fun _inst_1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

noncomputable def witt_vector.ghost_component {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ℕ) :

witt_vector p R →+* R

Evaluates the nth Witt polynomial on the first n coefficients of x, producing a value in R.

Equations

witt_vector.ghost_component n = (pi.eval_ring_hom (λ (n : ℕ), R) n).comp witt_vector.ghost_map

theorem witt_vector.ghost_component_apply {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ℕ) (x : witt_vector p R) :

⇑(witt_vector.ghost_component n) x = ⇑(mv_polynomial.aeval x.coeff) (witt_polynomial p ℤ n)

@[simp]

theorem witt_vector.ghost_map_apply {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) (n : ℕ) :

⇑witt_vector.ghost_map x n = ⇑(witt_vector.ghost_component n) x

noncomputable def witt_vector.ghost_equiv (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible ↑p] :

witt_vector p R ≃+* (ℕ → R)

witt_vector.ghost_map is a ring isomorphism when p is invertible in R.

Equations

witt_vector.ghost_equiv p R = {to_fun := witt_vector.ghost_map.to_fun, inv_fun := (ghost_equiv' p R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[simp]

theorem witt_vector.ghost_equiv_coe (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible ↑p] :

↑(witt_vector.ghost_equiv p R) = witt_vector.ghost_map

theorem witt_vector.ghost_map.bijective_of_invertible (p : ℕ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible ↑p] :

function.bijective ⇑witt_vector.ghost_map

@[simp]

theorem witt_vector.constant_coeff_apply {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : witt_vector p R) :

⇑witt_vector.constant_coeff x = x.coeff 0

def witt_vector.constant_coeff {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :

witt_vector p R →+* R

witt_vector.coeff x 0 as a ring_hom

Equations

witt_vector.constant_coeff = {to_fun := λ (x : witt_vector p R), x.coeff 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[protected, instance]

def witt_vector.nontrivial {p : ℕ} {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] :

nontrivial (witt_vector p R)