Maximal ideals of ℤ̄ versus valuation subrings of ℚ̄

Let $p$ be a prime, let $\iota : \overline{\mathbb{Q}} \to \mathbb{C}$ be a ring homomorphism from the algebraic closure of $\mathbb{Q}$ to $\mathbb{C}$, and let $\mathfrak{m}$ be a maximal ideal of $\overline{\mathbb{Z}} := \mathrm{integralClosure}\,\mathbb{Z}\,\mathbb{C}$, the ring of elements of $\mathbb{C}$ integral over $\mathbb{Z}$, such that the image of $p$ in $\overline{\mathbb{Z}}$ lies in $\mathfrak{m}$. Then there exists a valuation subring $A$ of $\overline{\mathbb{Q}}$ with the following two properties. First, $A$ lies over $p$ in the sense of the project's predicate LiesOverPrime: the image of $p$ in $\overline{\mathbb{Q}}$ belongs to A.nonunits, the set of elements of $\overline{\mathbb{Q}}$ that are non-units of $A$, i.e. $p$ lies in the maximal ideal of $A$. Second, for every complex number $z$, the following are equivalent: there exist $x, y \in \overline{\mathbb{Z}}$ with $y \notin \mathfrak{m}$ and $x = y z$ in $\mathbb{C}$ (so that $z$ is $\mathfrak{m}$-local, a quotient of algebraic integers with denominator outside $\mathfrak{m}$); and there exists $a \in A$ with $\iota(a) = z$. In particular the image under $\iota$ of $A$ is exactly the localisation of $\overline{\mathbb{Z}}$ at $\mathfrak{m}$ inside $\mathbb{C}$.

This is the comparison of the two ways of expressing $p$-integrality of an algebraic number used in the formalisation: membership in the localisation of the algebraic integers of $\mathbb{C}$ at a maximal ideal above $p$, and membership in a valuation subring of $\overline{\mathbb{Q}}$ whose maximal ideal contains $p$; it rests on the standard theory of extensions of valuations to algebraic extensions. It is used in the analysis of $q$-expansions and Atkin–Lehner/Hecke operators on modular curves, where integrality hypotheses arrive in one spelling and are consumed in the other.