τ-Native Local Field

ℤ_p^τ = lim← ℤ/p^n ℤ as inverse limit within τ. The p-adic integers are a τ-object with NF address. p-adic valuation v_p = D-coordinate restricted to p-primary component.

τ-Native Local Field

Summary

ℤ_p^τ = lim← ℤ/p^n ℤ as inverse limit within τ. The p-adic integers are a τ-object with NF address. p-adic valuation v_p = D-coordinate restricted to p-primary component.

Statement

%
\label{def:tau-native-local-field}
The \textbf{$\tau$-native $p$-adic integers} are the inverse limit
\begin{equation}\label{eq:ch16-p-adic-integers}
    \Z_p^\tau
    \;=\;
    \varprojlim_{n} \Z / p^n \Z
    \;=\;
    \Bigl\{
        (a_1, a_2, a_3, \ldots)
        \;\Big|\;
        a_n \in \Z / p^n \Z,\;
        \pi_{n+1,n}(a_{n+1}) = a_n
        \;\text{for all } n \geq 1
    \Bigr\}.
\end{equation}
An element of $\Z_p^\tau$ is called a \textbf{$p$-adic $\tau$-integer}.
The ring operations are defined componentwise:
\begin{align}
    (a_n)_n + (b_n)_n &\;=\; (a_n + b_n \bmod p^n)_n,
    \label{eq:ch16-p-adic-add} \\
    (a_n)_n \cdot (b_n)_n &\;=\; (a_n \cdot b_n \bmod p^n)_n.
    \label{eq:ch16-p-adic-mult}
\end{align}
These are well defined because the reduction maps
are ring homomorphisms:
if $a_{n+1} \equiv a_n$ and $b_{n+1} \equiv b_n$ modulo~$p^n$,
then $(a_{n+1} + b_{n+1}) \equiv (a_n + b_n)$
and $(a_{n+1} \cdot b_{n+1}) \equiv (a_n \cdot b_n)$ modulo~$p^n$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 45
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch16-hensel-lifting-and-local-fields.tex lines 346-376

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.LocalFields
• Name: LocalFieldElt

Dependencies

• Canonical: III.T11, III.D19

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.