Restriction Map

The restriction map: restrict a StageFun to inputs NOT in a given subset K. Returns 0 for deleted inputs. Agrees with original outside K.

Restriction Map

Summary

The restriction map: restrict a StageFun to inputs NOT in a given subset K. Returns 0 for deleted inputs. Agrees with original outside K.

Statement

%
\label{def:restriction-map}
Let $K \subseteq \mathbb{L}$.
The \textbf{restriction map} is:
\[
    \boxed{%
    \mathrm{res}_K : \mathrm{Hol}(\mathbb{L})
    \to \mathrm{Fun}(\mathbb{L} \setminus K),
    \quad
    \mathrm{res}_K(f) := f|_{\mathbb{L} \setminus K},}
\]
sending $f$ to its restriction
to the complement $\mathbb{L} \setminus K$.
The map $\mathrm{res}_K$ is a ring homomorphism:
$\mathrm{res}_K(f + g) = \mathrm{res}_K(f) + \mathrm{res}_K(g)$
and $\mathrm{res}_K(f \cdot g) = \mathrm{res}_K(f) \cdot \mathrm{res}_K(g)$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 149
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part16/ch60-spectral-coefficients.tex lines 137-154

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.SpectralCoefficients
• Name: Tau.Holomorphy.restriction

Dependencies

• Canonical: I.D47

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.