Teichmuller Series

Let R be a characteristic p perfect ring. In this file, we show that every element x of the Witt vectors 𝕎 R can be written as the (p-adic) summation of Teichmuller series, namely ∑ i, (teichmuller p (((frobeniusEquiv R p).symm ^ i) (x.coeff i)) * p ^ i)

Main theorems

• WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff : p ^ (n + 1) divides x minus the summation of the first n + 1 terms of the Teichmuller series.
• WittVector.eq_of_apply_teichmuller_eq : Given a ring S such that p is nilpotent in S and two ring maps f g : 𝕎 R →+* S, if they coincide on the teichmuller representatives, then they are equal.

TODO

Show that the Teichmuller series is unique.

theorem WittVector.sum_coeff_eq_coeff_sum {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] {α : Type u_2} {S : Finset α} (x : α → WittVector p R) (h : ∀ (n : ℕ), Subsingleton ↑{r : α | r ∈ S ∧ (x r).coeff n ≠ 0}) (n : ℕ) : (∑ s ∈ S, x s).coeff n = ∑ s ∈ S, (x s).coeff n

@[simp]

theorem WittVector.teichmuller_mul_pow_coeff {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] (n : ℕ) (x : R) : ((teichmuller p) x * ↑p ^ n).coeff n = x ^ p ^ n

theorem WittVector.teichmuller_mul_pow_coeff_of_ne {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] (x : R) {m n : ℕ} (h : m ≠ n) : ((teichmuller p) x * ↑p ^ n).coeff m = 0

theorem WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff {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) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i

p ^ (n + 1) divides x minus the summation of the first n + 1 terms of the Teichmuller series.

theorem WittVector.eq_of_apply_teichmuller_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] {S : Type u_2} [CommRing S] (f g : WittVector p R →+* S) : IsNilpotent ↑p → ∀ (h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)), f = g

Given a ring S such that p is nilpotent in S and two ring maps f g : 𝕎 R →+* S, if they coincide on the teichmuller representatives, then they are equal.