Reconstruction Functor

CRT defines a functor R_k from ∏(ℤ/pᵢℤ-Mod) to ℤ/Prim(k)ℤ-Mod. This functor is an equivalence (inverse = restriction S_k). All Part IV-VI arguments decompose through it.

Reconstruction Functor

Summary

CRT defines a functor R_k from ∏(ℤ/pᵢℤ-Mod) to ℤ/Prim(k)ℤ-Mod. This functor is an equivalence (inverse = restriction S_k). All Part IV-VI arguments decompose through it.

Statement

%
\label{def:reconstruction-functor}
The \textbf{Reconstruction Functor}
at primorial depth~$k$ is
\begin{equation}\label{eq:ch15-recon-functor}
    \mathcal{R}_k
    \;:\;
    \prod_{i=1}^{k} (R_i\text{-Mod})
    \;\longrightarrow\;
    R\text{-Mod},
    \qquad
    \mathcal{R}_k(M_1, \ldots, M_k)
    \;=\;
    \bigoplus_{i=1}^{k} M_i,
\end{equation}
where $r \in R$ acts on $M_i$
via $r_i = r \bmod p_i$.
On morphisms: $\mathcal{R}_k(f_1, \ldots, f_k)
= f_1 \oplus \cdots \oplus f_k$.
The \textbf{Restriction Functor}
$\mathcal{S}_k : R\text{-Mod}
\to \prod (R_i\text{-Mod})$
maps $M \mapsto (e_1 \cdot M, \ldots, e_k \cdot M)$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 42
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch15-the-crt-decomposition-theorem.tex lines 520-544

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.CRT
• Name: reconstruction_functor_check

Dependencies

• Canonical: III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.