Truncated Witt vectors

The ring of truncated Witt vectors (of length n) is a quotient of the ring of Witt vectors. It retains the first n coefficients of each Witt vector. In this file, we set up the basic quotient API for this ring.

The ring of Witt vectors is the projective limit of all the rings of truncated Witt vectors.

Main declarations

• TruncatedWittVector: the underlying type of the ring of truncated Witt vectors
• TruncatedWittVector.instCommRing: the ring structure on truncated Witt vectors
• WittVector.truncate: the quotient homomorphism that truncates a Witt vector, to obtain a truncated Witt vector
• TruncatedWittVector.truncate: the homomorphism that truncates a truncated Witt vector of length n to one of length m (for some m ≤ n)
• WittVector.lift: the unique ring homomorphism into the ring of Witt vectors that is compatible with a family of ring homomorphisms to the truncated Witt vectors: this realizes the ring of Witt vectors as projective limit of the rings of truncated Witt vectors

References

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

def TruncatedWittVector : ℕ → (n : ℕ) → (R : Type u_2) → Type u_2

A truncated Witt vector over R is a vector of elements of R, i.e., the first n coefficients of a Witt vector. We will define operations on this type that are compatible with the (untruncated) Witt vector operations.

TruncatedWittVector p n R takes a parameter p : ℕ that is not used in the definition. In practice, this number p is assumed to be a prime number, and under this assumption we construct a ring structure on TruncatedWittVector p n R. (TruncatedWittVector p₁ n R and TruncatedWittVector p₂ n R are definitionally equal as types but will have different ring operations.)

@[implicit_reducible]

instance instInhabitedTruncatedWittVector (p n : ℕ) (R : Type u_2) [Inhabited R] : Inhabited (TruncatedWittVector p n R)

def TruncatedWittVector.mk (p : ℕ) {n : ℕ} {R : Type u_1} (x : Fin n → R) : TruncatedWittVector p n R

Create a TruncatedWittVector from a vector x.

def TruncatedWittVector.coeff {p n : ℕ} {R : Type u_1} (i : Fin n) (x : TruncatedWittVector p n R) : R

x.coeff i is the ith entry of x.

theorem TruncatedWittVector.ext {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R} (h : ∀ (i : Fin n), coeff i x = coeff i y) : x = y

theorem TruncatedWittVector.ext_iff {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R} : x = y ↔ ∀ (i : Fin n), coeff i x = coeff i y

@[simp]

theorem TruncatedWittVector.coeff_mk {p n : ℕ} {R : Type u_1} (x : Fin n → R) (i : Fin n) : coeff i (mk p x) = x i

@[simp]

theorem TruncatedWittVector.mk_coeff {p n : ℕ} {R : Type u_1} (x : TruncatedWittVector p n R) : (mk p fun (i : Fin n) => coeff i x) = x

def TruncatedWittVector.out {p n : ℕ} {R : Type u_1} [CommRing R] (x : TruncatedWittVector p n R) : WittVector p R

We can turn a truncated Witt vector x into a Witt vector by setting all coefficients after x to be 0.

@[simp]

theorem TruncatedWittVector.coeff_out {p n : ℕ} {R : Type u_1} [CommRing R] (x : TruncatedWittVector p n R) (i : Fin n) : x.out.coeff ↑i = coeff i x

theorem TruncatedWittVector.out_injective {p n : ℕ} {R : Type u_1} [CommRing R] : Function.Injective out

def WittVector.truncateFun {p : ℕ} (n : ℕ) {R : Type u_1} (x : WittVector p R) : TruncatedWittVector p n R

truncateFun n x uses the first n entries of x to construct a TruncatedWittVector, which has the same base p as x. This function is bundled into a ring homomorphism in WittVector.truncate

@[simp]

theorem WittVector.coeff_truncateFun {p n : ℕ} {R : Type u_1} (x : WittVector p R) (i : Fin n) : TruncatedWittVector.coeff i (truncateFun n x) = x.coeff ↑i

@[simp]

theorem WittVector.out_truncateFun {p n : ℕ} {R : Type u_1} [CommRing R] (x : WittVector p R) : (truncateFun n x).out = init n x

@[simp]

theorem TruncatedWittVector.truncateFun_out {p n : ℕ} {R : Type u_1} [CommRing R] (x : TruncatedWittVector p n R) : WittVector.truncateFun n x.out = x

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instZero (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Zero (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instOne (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : One (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instNatCast (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : NatCast (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instIntCast (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : IntCast (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instAdd (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Add (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instMul (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Mul (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instNeg (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Neg (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instSub (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Sub (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.hasNatScalar (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : SMul ℕ (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.hasIntScalar (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : SMul ℤ (TruncatedWittVector p n R)

@[implicit_reducible]

noncomputable instance TruncatedWittVector.hasNatPow (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Pow (TruncatedWittVector p n R) ℕ

@[simp]

theorem TruncatedWittVector.coeff_zero (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] (i : Fin n) : coeff i 0 = 0

def witt_truncateFun_tac : Lean.ParserDescr

A macro tactic used to prove that truncateFun respects ring operations.

theorem WittVector.truncateFun_surjective (p n : ℕ) (R : Type u_1) [CommRing R] : Function.Surjective (truncateFun n)

@[simp]

theorem WittVector.truncateFun_zero (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : truncateFun n 0 = 0

@[simp]

theorem WittVector.truncateFun_one (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : truncateFun n 1 = 1

@[simp]

theorem WittVector.truncateFun_add {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) : truncateFun n (x + y) = truncateFun n x + truncateFun n y

@[simp]

theorem WittVector.truncateFun_mul {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) : truncateFun n (x * y) = truncateFun n x * truncateFun n y

theorem WittVector.truncateFun_neg {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) : truncateFun n (-x) = -truncateFun n x

theorem WittVector.truncateFun_sub {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x y : WittVector p R) : truncateFun n (x - y) = truncateFun n x - truncateFun n y

theorem WittVector.truncateFun_nsmul {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) : truncateFun n (m • x) = m • truncateFun n x

theorem WittVector.truncateFun_zsmul {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℤ) (x : WittVector p R) : truncateFun n (m • x) = m • truncateFun n x

theorem WittVector.truncateFun_pow {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (m : ℕ) : truncateFun n (x ^ m) = truncateFun n x ^ m

theorem WittVector.truncateFun_natCast {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℕ) : truncateFun n ↑m = ↑m

theorem WittVector.truncateFun_intCast {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ℤ) : truncateFun n ↑m = ↑m

@[implicit_reducible]

noncomputable instance TruncatedWittVector.instCommRing (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : CommRing (TruncatedWittVector p n R)

noncomputable def WittVector.truncate {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] : WittVector p R →+* TruncatedWittVector p n R

truncate n is a ring homomorphism that truncates x to its first n entries to obtain a TruncatedWittVector, which has the same base p as x.

theorem WittVector.truncate_surjective (p n : ℕ) (R : Type u_1) [CommRing R] [Fact (Nat.Prime p)] : Function.Surjective ⇑(truncate n)

@[simp]

theorem WittVector.coeff_truncate {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (i : Fin n) : TruncatedWittVector.coeff i ((truncate n) x) = x.coeff ↑i

theorem WittVector.mem_ker_truncate {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) : x ∈ RingHom.ker (truncate n) ↔ ∀ i < n, x.coeff i = 0

@[simp]

theorem WittVector.truncate_mk' (p n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (f : ℕ → R) : (truncate n) { coeff := f } = TruncatedWittVector.mk p fun (k : Fin n) => f ↑k

noncomputable def TruncatedWittVector.truncate {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) : TruncatedWittVector p m R →+* TruncatedWittVector p n R

A ring homomorphism that truncates a truncated Witt vector of length m to a truncated Witt vector of length n, for n ≤ m.

@[simp]

theorem TruncatedWittVector.truncate_comp_wittVector_truncate {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) : (truncate hm).comp (WittVector.truncate m) = WittVector.truncate n

@[simp]

theorem TruncatedWittVector.truncate_wittVector_truncate {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) (x : WittVector p R) : (truncate hm) ((WittVector.truncate m) x) = (WittVector.truncate n) x

@[simp]

theorem TruncatedWittVector.truncate_truncate {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) (x : TruncatedWittVector p n₃ R) : (truncate h1) ((truncate h2) x) = (truncate ⋯) x

@[simp]

theorem TruncatedWittVector.truncate_comp {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) : (truncate h1).comp (truncate h2) = truncate ⋯

theorem TruncatedWittVector.truncate_surjective {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) : Function.Surjective ⇑(truncate hm)

@[simp]

theorem TruncatedWittVector.coeff_truncate {p n : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) (i : Fin n) (x : TruncatedWittVector p m R) : coeff i ((truncate hm) x) = coeff (Fin.castLE hm i) x

@[implicit_reducible]

instance TruncatedWittVector.instFintype {p n : ℕ} {R : Type u_2} [Fintype R] : Fintype (TruncatedWittVector p n R)

theorem TruncatedWittVector.card (p n : ℕ) {R : Type u_2} [Fintype R] : Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n

theorem TruncatedWittVector.iInf_ker_truncate {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] : ⨅ (i : ℕ), RingHom.ker (WittVector.truncate i) = ⊥

noncomputable def WittVector.liftFun {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] (f : (k : ℕ) → S →+* TruncatedWittVector p k R) (s : S) : WittVector p R

Given a family fₖ : S → TruncatedWittVector p k R and s : S, we produce a Witt vector by defining the kth entry to be the final entry of fₖ s.

@[simp]

theorem WittVector.truncate_liftFun {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] {f : (k : ℕ) → S →+* TruncatedWittVector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) (s : S) : (truncate n) (liftFun f s) = (f n) s

noncomputable def WittVector.lift {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] (f : (k : ℕ) → S →+* TruncatedWittVector p k R) (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) : S →+* WittVector p R

Given compatible ring homs from S into TruncatedWittVector n for each n, we can lift these to a ring hom S → 𝕎 R.

lift defines the universal property of 𝕎 R as the inverse limit of TruncatedWittVector n.

@[simp]

theorem WittVector.truncate_lift {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] {f : (k : ℕ) → S →+* TruncatedWittVector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) (s : S) : (truncate n) ((lift f f_compat) s) = (f n) s

@[simp]

theorem WittVector.truncate_comp_lift {p : ℕ} (n : ℕ) {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] {f : (k : ℕ) → S →+* TruncatedWittVector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) : (truncate n).comp (lift f f_compat) = f n

theorem WittVector.lift_unique {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] {f : (k : ℕ) → S →+* TruncatedWittVector p k R} (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) (g : S →+* WittVector p R) (g_compat : ∀ (k : ℕ), (truncate k).comp g = f k) : lift f f_compat = g

The uniqueness part of the universal property of 𝕎 R.

noncomputable def WittVector.liftEquiv {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] : { f : (k : ℕ) → S →+* TruncatedWittVector p k R // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ } ≃ (S →+* WittVector p R)

The universal property of 𝕎 R as projective limit of truncated Witt vector rings.

@[simp]

theorem WittVector.liftEquiv_apply {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] (f : { f : (k : ℕ) → S →+* TruncatedWittVector p k R // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ }) : liftEquiv f = lift ↑f ⋯

@[simp]

theorem WittVector.liftEquiv_symm_apply_coe {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] (g : S →+* WittVector p R) (k : ℕ) : ↑(liftEquiv.symm g) k = (truncate k).comp g

theorem WittVector.hom_ext {p : ℕ} {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] {S : Type u_2} [Semiring S] (g₁ g₂ : S →+* WittVector p R) (h : ∀ (k : ℕ), (truncate k).comp g₁ = (truncate k).comp g₂) : g₁ = g₂