Witt-vector Frobenius on Teichmüller representatives and the (p, [ϖ])-adic topology

Let R be a ring of characteristic p. The Witt-vector Frobenius φ of 𝕎 R sends the Teichmüller representative [r] to [r ^ p] = [r] ^ p, and when R is perfect its inverse sends [r] to [r ^ (1 / p)]. Consequently φ carries the ideal (p, [ϖ]) into itself, and φ⁻¹ carries it into its radical, so both are continuous for the (p, [ϖ])-adic topology. For a perfect ring of integers 𝒪_F this is the continuity of Frobenius on A_inf = W(𝒪_F), which lets Frobenius act on its adic spectrum.

Main results

• WittVector.frobenius_teichmuller : φ [r] = [r] ^ p in characteristic p.
• WittVector.frobeniusEquiv_symm_teichmuller : φ⁻¹ [r] = [r ^ (1 / p)] for perfect R.
• TauCeti.WittVector.continuous_frobenius : φ is continuous for the (p, [ϖ])-adic topology.
• TauCeti.WittVector.continuous_frobeniusEquiv_symm : so is φ⁻¹, for perfect R.

References

• K. S. Kedlaya, Sheaves, stacks, and shtukas, lecture notes, Arizona Winter School 2017, §3.1.

@[simp]

theorem WittVector.frobenius_teichmuller {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] (r : R) : frobenius ((teichmuller p) r) = (teichmuller p) r ^ p

In characteristic p, the Witt-vector Frobenius sends a Teichmüller representative [r] to its p-th power [r ^ p].

@[simp]

theorem WittVector.frobeniusEquiv_symm_teichmuller {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] (r : R) : (frobeniusEquiv p R).symm ((teichmuller p) r) = (teichmuller p) ((_root_.frobeniusEquiv R p).symm r)

For a perfect ring of characteristic p, the inverse of the Witt-vector Frobenius sends a Teichmüller representative [r] to the Teichmüller representative of the p-th root of r.

theorem TauCeti.WittVector.continuous_frobenius {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [TopologicalSpace (WittVector p R)] {ϖ : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ})) : Continuous ⇑WittVector.frobenius

The Witt-vector Frobenius is continuous for the (p, [ϖ])-adic topology: it fixes p and sends [ϖ] to [ϖ] ^ p, so it carries the ideal (p, [ϖ]) into itself.

theorem TauCeti.WittVector.continuous_frobeniusEquiv_symm {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [TopologicalSpace (WittVector p R)] {ϖ : R} [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ})) : Continuous ⇑(WittVector.frobeniusEquiv p R).symm

For a perfect ring of characteristic p, the inverse of the Witt-vector Frobenius is continuous for the (p, [ϖ])-adic topology: it fixes p and sends [ϖ] to a p-th root [ϖ ^ (1 / p)] of [ϖ], so it carries the ideal (p, [ϖ]) into its radical.