Papers With

← All papers
First page of Non-liftability of the field of norms of the $p$-adic false Tate curve extension

Non-liftability of the field of norms of the $p$-adic false Tate curve extension

Yijun Yuan

math.NT Oct 26, 2026 · v1
formalization mathlib number-theory
Read PDF arXiv abstract Code
TL;DR
All results and their dependencies are formalized sorry-free in Lean 4 with mathlib4, with LLM assistance in producing the formalization.
Abstract
Let $p\geq3$ be a prime number. We prove that the action of the Galois group on the field of norms of the $p$-adic false Tate curve extension $\mathbf{Q}_p\left(ζ_{p^\infty},p^{1/p^\infty}\right)$ of $\mathbf{Q}_p$ is not liftable to its Cohen ring with respect to any admissible coefficient field.
Problem

For p ≥ 3, the question is whether the Galois action on the field of norms of the p-adic false Tate curve extension Q_p(ζ_{p^∞}, p^{1/p^∞}) can be lifted to its Cohen ring together with a commuting Frobenius. Such a lift would give a theory of (φ,Γ)-modules beyond the cyclotomic case, as asked by Berger.

Approach

The argument works with finite-precision lifts modulo ϖ_F^{e+1} and introduces a normalized derivative h_P of a Frobenius lift P. In the case s(P)=e, normal forms of commuting automorphisms give valuation bounds on h_P. In the case s(P)<e, invariant exact differentials lead to an integrality constraint. Arithmetic input comes from the ramification numbers of Kummer iterates, computed from Viviani's description of the ramification filtration.

Results

The Galois action is not liftable with respect to any admissible coefficient field, because the ramification numbers d_k = (2p^{2k+2}+p−1)/(p+1) tend to infinity and converge p-adically to a non-integer. The whole development is formalized in Lean 4 using mathlib4 and depends only on the standard axioms.