Surjectivity of Frobenius in a π-adically complete ring

Let p be a prime and A a commutative ring that is π-adically complete and separated for an element π with π ^ p ∣ p. Then the following are equivalent (Bhatt–Morrow–Scholze, Integral p-adic Hodge theory, Lemma 3.9):

1. the relative Frobenius A ⧸ π → A ⧸ π ^ p, [x] ↦ [x ^ p], is surjective, that is, every element of A is a p-th power modulo π ^ p;
2. Frobenius on A ⧸ p is surjective;
3. every element of A ⧸ π p is a p-th power.

The implications 3 → 2 → 1 only use π ^ p ∣ p. The implication 1 → 3 is a successive approximation which does not use this divisibility: writing x = y₀ ^ p + π ^ p z₁, z₁ = y₁ ^ p + π ^ p z₂, and so on, the partial sums sₙ = y₀ + π y₁ + ⋯ + π ^ (n - 1) yₙ₋₁ satisfy x = sₙ ^ p + p bₙ + π ^ (p n) zₙ, where p bₙ collects the cross terms of the binomial expansions. These cross terms are divisible by p π, so π ∣ bₙ, and both sₙ and bₙ converge π-adically. In the limit x = s ^ p + p b with π ∣ b.

For a perfectoid Tate ring R this applies to A = R° and a pseudouniformiser ϖ ∈ R° with ϖ ^ p ∣ p, where R° is ϖ-adically complete; it shows that the perfectoid condition can be tested modulo p and that it does not depend on the choice of ϖ. Condition 2 is the hypothesis of Mathlib's WittVector.surjective_fontaineTheta, in the form of TauCeti.surjective_frobenius_modP_iff (in TauCeti.RingTheory.Ideal.Quotient.Frobenius).

Main results

• TauCeti.exists_mul_dvd_sub_pow: in a π-adically complete ring in which every element is a p-th power modulo π ^ p, every element is a p-th power modulo π p.
• TauCeti.tfae_forall_exists_dvd_sub_pow: the equivalence of the three conditions above.

References

• B. Bhatt, M. Morrow, P. Scholze, Integral p-adic Hodge theory, Lemma 3.9.
• P. Scholze, Étale cohomology of diamonds, Remark 3.2.

theorem TauCeti.exists_mul_dvd_sub_pow {A : Type u_1} [CommRing A] {π : A} {p : ℕ} [Fact (Nat.Prime p)] [IsHausdorff (Ideal.span {π}) A] [IsPrecomplete (Ideal.span {π}) A] (h : ∀ (x : A), ∃ (y : A), π ^ p ∣ x - y ^ p) (x : A) : ∃ (y : A), π * ↑p ∣ x - y ^ p

Roots modulo π ^ p give roots modulo π p. In a π-adically complete and separated ring in which every element is a p-th power modulo π ^ p, every element is a p-th power modulo π p (Bhatt–Morrow–Scholze, Integral p-adic Hodge theory, Lemma 3.9).

theorem TauCeti.tfae_forall_exists_dvd_sub_pow {A : Type u_1} [CommRing A] (π : A) {p : ℕ} [Fact (Nat.Prime p)] [IsHausdorff (Ideal.span {π}) A] [IsPrecomplete (Ideal.span {π}) A] (h : π ^ p ∣ ↑p) : [∀ (x : A), ∃ (y : A), π ^ p ∣ x - y ^ p, ∀ (x : A), ∃ (y : A), ↑p ∣ x - y ^ p, ∀ (x : A), ∃ (y : A), π * ↑p ∣ x - y ^ p].TFAE

The Frobenius surjectivity criterion (Bhatt–Morrow–Scholze, Integral p-adic Hodge theory, Lemma 3.9). In a π-adically complete and separated ring A with π ^ p ∣ p, the following are equivalent: every element of A is a p-th power modulo π ^ p, modulo p, and modulo π p.