Adelic Euler Product

τ-holomorphic function on 𝔸_τ decomposes into local factors at each prime. Adelic form of Euler product: CRT lifted to holomorphic level.

Adelic Euler Product

Summary

τ-holomorphic function on 𝔸_τ decomposes into local factors at each prime. Adelic form of Euler product: CRT lifted to holomorphic level.

Statement

%
\label{prop:adelic-euler-product}
Let $F \in \mathrm{Hol}(\mathbb{A}_\tau)$
be a $\tau$-holomorphic function on the adele ring.
Then $F$ admits a unique decomposition
\begin{equation}\label{eq:ch17-euler-product}
    F
    \;=\;
    \prod_{p} f_p,
    \qquad
    f_p \in \mathrm{Hol}_p(\Z_p^\tau),
\end{equation}
with $f_p = 1$ for almost all~$p$.
The decomposition is functorial:
if $\Phi : F \to G$
is a morphism of adelic holomorphic functions,
then $\Phi$ decomposes as $\Phi = \prod_p \phi_p$
with $\phi_p : f_p \to g_p$
a morphism of local holomorphic functions
at each prime.

Proof / Justification

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

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: III.D22, III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.