Functoriality Theorem

For every sector morphism f: S₁→S₂, the induced map on boundary characters commutes with spectral decomposition

Functoriality Theorem

Summary

For every sector morphism f: S₁→S₂, the induced map on boundary characters commutes with spectral decomposition

Statement

\label{thm:functoriality-theorem}
Let $S_1, S_2 \in \{A, B, C, D\}$ be primitive sectors and let $f\colon S_1 \to S_2$ be a tower-coherent sector morphism in $\operatorname{Cat}_{\T}(\Elayer{1})$.  Then the diagram
\begin{equation}
\begin{tikzcd}
\operatorname{Bdy}_{S_1} \arrow[r, "f^{\mathrm{bdy}}"] \arrow[d, "\operatorname{AG}_{S_1}"'] & \operatorname{Bdy}_{S_2} \arrow[d, "\operatorname{AG}_{S_2}"] \\
\operatorname{Spec}_{S_1} \arrow[r, "f^{\mathrm{spec}}"'] & \operatorname{Spec}_{S_2}
\end{tikzcd}
\label{eq:ch49-functoriality-theorem-diagram}
\end{equation}
commutes.  That is, for every boundary character $\beta \in \operatorname{Bdy}_{S_1}$,
\begin{equation}
\operatorname{AG}_{S_2}\bigl(f^{\mathrm{bdy}}(\beta)\bigr) \;=\; f^{\mathrm{spec}}\bigl(\operatorname{AG}_{S_1}(\beta)\bigr).
\label{eq:ch49-functoriality-equation}
\end{equation}

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 134
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part06/ch49-functoriality-as-diagram-commutativity.tex lines 93-109

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Arithmetic.Langlands
• Name: functoriality_check

Dependencies

• Canonical: III.D57, III.D63, III.D64, III.P28

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.