Teichmüller coordinates of Witt vectors over a perfect ring

Let R be a perfect ring of characteristic p. Every Witt vector x : 𝕎 R is the p-adic sum x = ∑ₙ [xₙ] pⁿ of Teichmüller representatives, where xₙ is the p ^ n-th root of the n-th Witt coordinate of x (WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff). This file names xₙ the n-th Teichmüller coordinate x.teichmullerCoeff n and records how it behaves: it is determined by x modulo p ^ (n + 1), it reads off the coefficients of a finite Teichmüller sum, and multiplication by [c] multiplies every Teichmüller coordinate by c, while multiplication by p shifts them. The coordinates determine x, so divisibility by [c] and regularity of [c] can be read off coordinatewise. These coordinates are the input to the Gauss valuations on A_inf = W(𝒪_F).

Main definitions

• WittVector.teichmullerCoeff : the Teichmüller coordinates of a Witt vector.

Main results

• WittVector.pow_dvd_sub_sum_teichmullerCoeff : the Teichmüller expansion modulo p ^ (n + 1).
• WittVector.exists_eq_sum_teichmullerCoeff_add_pow_mul : the splitting x = ∑_{i < m} [xᵢ] pⁱ + pᵐ b of the Teichmüller expansion.
• WittVector.teichmullerCoeff_sum_teichmuller_mul_pow : the Teichmüller coordinates of a finite Teichmüller sum ∑_{j ∈ s} [aⱼ] pʲ are the aᵢ for i ∈ s, and vanish off s.
• WittVector.pow_dvd_sub_iff_forall_teichmullerCoeff_eq : two Witt vectors are congruent modulo p ^ (n + 1) exactly when their first n + 1 Teichmüller coordinates agree.
• WittVector.teichmullerCoeff_teichmuller_mul : [c] x has Teichmüller coordinates c xₙ.
• WittVector.teichmullerCoeff_injective : a Witt vector is determined by its Teichmüller coordinates.
• WittVector.teichmullerCoeff_mul_natCast_pow_add : x pᵐ has Teichmüller coordinates xₙ in position n + m, and 0 below m (WittVector.teichmullerCoeff_mul_natCast_pow_of_lt).
• WittVector.teichmuller_dvd_iff : [c] divides x iff c divides every xₙ; hence [c] divides x pᵐ only if it divides x (WittVector.teichmuller_dvd_mul_natCast_pow_iff).
• WittVector.teichmuller_mem_nonZeroDivisors_iff : [c] is a nonzerodivisor iff c is.

References

• L. Fargues and J.-M. Fontaine, Courbes et fibrés vectoriels en théorie de Hodge p-adique, Astérisque 406 (2018), Chapter 1.

theorem WittVector.teichmuller_ne_zero (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {a : R} (ha : a ≠ 0) : (teichmuller p) a ≠ 0

The Teichmüller representative [a] of a ≠ 0 is nonzero, as its 0-th coordinate is a.

noncomputable def WittVector.teichmullerCoeff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) (n : ℕ) : R

The n-th Teichmüller coordinate of a Witt vector x over a perfect ring of characteristic p: the p ^ n-th root of the n-th Witt coordinate of x. These are the coefficients of the Teichmüller expansion x = ∑ₙ [xₙ] pⁿ.

@[simp]

theorem WittVector.teichmullerCoeff_pow {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) (n : ℕ) : x.teichmullerCoeff n ^ p ^ n = x.coeff n

The n-th Teichmüller coordinate is a p ^ n-th root of the n-th Witt coordinate.

theorem WittVector.teichmullerCoeff_eq_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {x : WittVector p R} {n : ℕ} {a : R} : x.teichmullerCoeff n = a ↔ x.coeff n = a ^ p ^ n

The Teichmüller coordinate is characterised by its p ^ n-th power.

@[simp]

theorem WittVector.teichmullerCoeff_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) : x.teichmullerCoeff 0 = x.coeff 0

The 0-th Teichmüller coordinate is the 0-th Witt coordinate.

@[simp]

theorem WittVector.zero_teichmullerCoeff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (n : ℕ) : teichmullerCoeff 0 n = 0

The Teichmüller coordinates of 0 vanish.

@[simp]

theorem WittVector.teichmullerCoeff_sum_teichmuller_mul_pow {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (a : ℕ → R) (s : Finset ℕ) (i : ℕ) : (∑ j ∈ s, (teichmuller p) (a j) * ↑p ^ j).teichmullerCoeff i = if i ∈ s then a i else 0

The Teichmüller coordinates of a finite Teichmüller sum ∑_{j ∈ s} [aⱼ] pʲ are the aᵢ for i ∈ s, and vanish off s.

@[simp]

theorem WittVector.teichmullerCoeff_natCast_pow {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (m n : ℕ) : (↑p ^ m).teichmullerCoeff n = if n = m then 1 else 0

The Teichmüller coordinates of p ^ m: 1 in position m and 0 elsewhere.

@[simp]

theorem WittVector.teichmullerCoeff_teichmuller {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (a : R) (n : ℕ) : ((teichmuller p) a).teichmullerCoeff n = if n = 0 then a else 0

The Teichmüller coordinates of [a]: a in position 0 and 0 elsewhere.

theorem WittVector.pow_dvd_sub_sum_teichmullerCoeff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) (n : ℕ) : ↑p ^ (n + 1) ∣ x - ∑ i ≤ n, (teichmuller p) (x.teichmullerCoeff i) * ↑p ^ i

The Teichmüller expansion: x is congruent to ∑_{i ≤ n} [xᵢ] pⁱ modulo p ^ (n + 1).

theorem WittVector.exists_eq_sum_teichmullerCoeff_add_pow_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) (m : ℕ) : ∃ (b : WittVector p R), x = ∑ i ∈ Finset.range m, (teichmuller p) (x.teichmullerCoeff i) * ↑p ^ i + ↑p ^ m * b

Splitting the Teichmüller expansion of x after m terms: x = ∑_{i < m} [xᵢ] pⁱ + pᵐ b.

theorem WittVector.pow_dvd_sub_iff_forall_teichmullerCoeff_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {x y : WittVector p R} {n : ℕ} : ↑p ^ (n + 1) ∣ x - y ↔ ∀ i ≤ n, x.teichmullerCoeff i = y.teichmullerCoeff i

Two Witt vectors are congruent modulo p ^ (n + 1) exactly when their first n + 1 Teichmüller coordinates agree.

@[simp]

theorem WittVector.teichmullerCoeff_teichmuller_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (c : R) (x : WittVector p R) (n : ℕ) : ((teichmuller p) c * x).teichmullerCoeff n = c * x.teichmullerCoeff n

Multiplication by a Teichmüller representative [c] multiplies every Teichmüller coordinate by c.

theorem WittVector.teichmullerCoeff_injective {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] : Function.Injective teichmullerCoeff

A Witt vector over a perfect ring is determined by its Teichmüller coordinates.

@[simp]

theorem WittVector.teichmullerCoeff_mul_natCast_pow_add {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) (m n : ℕ) : (x * ↑p ^ m).teichmullerCoeff (n + m) = x.teichmullerCoeff n

Multiplication by p ^ m shifts the Teichmüller coordinates up by m.

theorem WittVector.teichmullerCoeff_mul_natCast_pow_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (x : WittVector p R) {m n : ℕ} (h : n < m) : (x * ↑p ^ m).teichmullerCoeff n = 0

The first m Teichmüller coordinates of x * p ^ m vanish.

theorem WittVector.teichmuller_dvd_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {c : R} {x : WittVector p R} : (teichmuller p) c ∣ x ↔ ∀ (n : ℕ), c ∣ x.teichmullerCoeff n

The Teichmüller representative [c] divides x exactly when c divides every Teichmüller coordinate of x.

@[simp]

theorem WittVector.teichmuller_dvd_mul_natCast_pow_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {c : R} {x : WittVector p R} {m : ℕ} : (teichmuller p) c ∣ x * ↑p ^ m ↔ (teichmuller p) c ∣ x

Over a perfect ring, [c] divides x * p ^ m only if it divides x: the factor p ^ m merely shifts the Teichmüller coordinates.

@[simp]

theorem WittVector.teichmuller_mem_nonZeroDivisors_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {c : R} : (teichmuller p) c ∈ nonZeroDivisors (WittVector p R) ↔ c ∈ nonZeroDivisors R

The Teichmüller representative [c] is a nonzerodivisor of 𝕎 R exactly when c is a nonzerodivisor of R.