Number Tower

N_tau subset Z_tau subset Q_tau subset R_tau subset C_tau. Integers via Grothendieck group, rationals via field of fractions, reals via Cauchy completion, complexes via R_tau[i].

Number Tower

Summary

N_tau subset Z_tau subset Q_tau subset R_tau subset C_tau. Integers via Grothendieck group, rationals via field of fractions, reals via Cauchy completion, complexes via R_tau[i].

Statement

%
\label{def:number-tower}
The \textbf{number tower} of Category $\tau$ is the hierarchy:
\[
    \boxed{\mathbb{N}_\tau \subseteq \mathbb{Z}_\tau \subseteq \mathbb{Q}_\tau
    \subseteq \mathbb{R}_\tau \subseteq \mathbb{C}_\tau.}
\]
Each level is a completion of the previous level
via a standard universal construction:
\begin{itemize}
    \item $\mathbb{N}_\tau \to \mathbb{Z}_\tau$: Grothendieck group completion (adjoining negatives).
    \item $\mathbb{Z}_\tau \to \mathbb{Q}_\tau$: Field of fractions (adjoining reciprocals).
    \item $\mathbb{Q}_\tau \to \mathbb{R}_\tau$: Cauchy completion (adjoining limits).
    \item $\mathbb{R}_\tau \to \mathbb{C}_\tau$: Algebraic extension (adjoining $\sqrt{-1}$).
\end{itemize}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 85
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part10/ch42-number-tower.tex lines 482-498

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.NumberTower
• Name: Tau.Boundary.TauInt

Dependencies

• Canonical: I.D07, I.D19, I.D10, I.D11

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.