mathlib documentation

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

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.

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
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 : witt_vector p R) :

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

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

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

@[instance]
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) :

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 : witt_vector p R) (n : ) :

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

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

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

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

Equations
@[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 : ) :

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