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 #

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

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 : ) :
noncomputable 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
noncomputable 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]
noncomputable def witt_vector.ghost_equiv (p : ) (R : Type u_1) [hp : fact (nat.prime p)] [comm_ring R] [invertible p] :

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

Equations
@[simp]
def witt_vector.constant_coeff {p : } {R : Type u_1} [hp : fact (nat.prime p)] [comm_ring 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] :