# mathlibdocumentation

ring_theory.witt_vector.basic

# Witt vectors #

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 : α → β) :
α β

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
theorem witt_vector.map_fun.injective {p : } {α : Type u_4} {β : Type u_5} (f : α → β) (hf : function.injective f) :
theorem witt_vector.map_fun.surjective {p : } {α : Type u_4} {β : Type u_5} (f : α → β) (hf : function.surjective f) :

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) :
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) :
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 : R) :
(x + 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 : R) :
(x - 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 : R) :
(x * 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 : R) :
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 : R) (n : ) :
(n 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 : R) (z : ) :
(z 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 : R) (n : ) :
(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 : ) :
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 : ) :

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 : ) :
j =
@[protected, instance]
noncomputable def witt_vector.comm_ring (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] :

The commutative ring structure on 𝕎 R.

Equations
• = _ _ _ _ _ _ _
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) :
R →+* S

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

Equations
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) :
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) :
@[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 : R) (n : ) :
( 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] :
R →+* → R

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

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

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

Equations
theorem witt_vector.ghost_component_apply {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (n : ) (x : R) :
= n)
@[simp]
theorem witt_vector.ghost_map_apply {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) (n : ) :
noncomputable def witt_vector.ghost_equiv (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible p] :
R ≃+* ( → R)

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

Equations
@[simp]
theorem witt_vector.ghost_equiv_coe (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible p] :
@[simp]
theorem witt_vector.constant_coeff_apply {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] (x : R) :
def witt_vector.constant_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] :
R →+* R

witt_vector.coeff x 0 as a ring_hom

Equations
@[protected, instance]
def witt_vector.nontrivial {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring R] [nontrivial R] :