DEF0090canonicalv1Primorial Presheaf
The primorial presheaf F : Prim^op -> Ring sends d to Z/M_dZ with reduction maps. Its split-complex extension F_j sends d to Z/M_dZ[j]. The spectral presheaf pair (F_B, F_C) is the sector decomposition.
Payload
Primorial Presheaf
The primorial presheaf F : Prim^op -> Ring sends d to Z/M_dZ with reduction maps. Its split-complex extension F_j sends d to Z/M_dZ[j]. The spectral presheaf pair (F_B, F_C) is the sector decomposition.
Primorial Presheaf
Summary
The primorial presheaf F : Prim^op -> Ring sends d to Z/M_dZ with reduction maps. Its split-complex extension F_j sends d to Z/M_dZ[j]. The spectral presheaf pair (F_B, F_C) is the sector decomposition.
Statement
%
\label{def:primorial-presheaf}
The \textbf{primorial category} $\mathbf{Prim}$
(sketched in Remark~\ref{rem:naturality}) is the category:
\begin{enumerate}
\item \textbf{Objects}: natural numbers $d \geq 1$
(primorial depths).
\item \textbf{Morphisms}: for each $k \leq \ell$,
a unique morphism $\pi_{\ell \to k} : \ell \to k$
(the primorial reduction map,
reduction modulo $M_k$).
\item \textbf{Composition}:
$\pi_{\ell \to k} \circ \pi_{m \to \ell}
= \pi_{m \to k}$.
\end{enumerate}
$\mathbf{Prim}$ is a subcategory of $\mathrm{Cat}_\tau$
(Definition~\ref{def:cat-tau}, I.D51).
Three presheaves on $\mathbf{Prim}$:
\begin{enumerate}
\item The \textbf{source presheaf}
$\mathcal{F} : \mathbf{Prim}^{\mathrm{op}} \to \mathbf{Ring}$,
sending $d \mapsto \mathbb{Z}/M_d\mathbb{Z}$
with restriction maps $\pi_{\ell \to k}$.
\item The \textbf{split-complex presheaf}
$\mathcal{F}_{\jj} : \mathbf{Prim}^{\mathrm{op}} \to \mathbf{Ring}$,
sending $d \mapsto \mathbb{Z}/M_d\mathbb{Z}[\jj]$
with restriction maps extended $\mathbb{Z}[\jj]$-linearly.
\item The \textbf{spectral presheaf pair}
$(\mathcal{F}_B, \mathcal{F}_C)$:
both copies of $\mathcal{F}$
(as set-valued presheaves),
obtained from $\mathcal{F}_{\jj}$
via the characters $\chi_+$ and $\chi_-$
(Definition~\ref{def:lemniscate-characters}, I.D37).
\end{enumerate}
Proof / Justification
This item is definitional. No manuscript proof is required.
Source Context
- Registry source:
book-01.jsonlline 184 - Manuscript source:
2nd-edition/book-i-categorical-foundations/02_mainmatter/part19/ch74-holomorphy-as-naturality.texlines 88-125
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookI.Holomorphy.PresheafEssence - Name:
PrimorialPresheaf
Dependencies
- Canonical: I.D51, I.D54, I.D46, I.D19, I.D20
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
I.D83primorial-presheafdef:primorial-presheafRelease lines
corpus_v3_workingcorpus_v2Relations
Appears in (1)
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.