τ-Adele Ring

τ-adele ring 𝔸_τ = restricted product of local fields ℤ_p^τ with respect to unit groups. Almost all components integral. τ-internal construction, not imported from algebraic number theory.

τ-Adele Ring

Summary

τ-adele ring 𝔸_τ = restricted product of local fields ℤ_p^τ with respect to unit groups. Almost all components integral. τ-internal construction, not imported from algebraic number theory.

Statement

%
\label{def:tau-adele-ring}
The \textbf{$\tau$-adele ring} is the restricted product
\begin{equation}\label{eq:ch17-adele-ring}
    \mathbb{A}_\tau
    \;=\;
    {\prod_{p}}' \;\Z_p^\tau
    \;=\;
    \Bigl\{\,
        (x_p)_p \in \prod_{p} \Z_p^\tau
        \;\Big|\;
        x_p \in (\Z_p^\tau)^\times
        \text{ for almost all } p
    \,\Bigr\},
\end{equation}
equipped with componentwise addition and multiplication.
The restricted-product notation
$\prod'_p$
indicates that the product is taken
with respect to the compact open subgroups
$(\Z_p^\tau)^\times \subset \Z_p^\tau$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 47
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch17-the-adelic-embedding.tex lines 142-164

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.Adeles
• Name: AdeleElement

Dependencies

• Canonical: III.D21, III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.