Identity Map

The identity omega-germ transformer on a tau-admissible point x, defined by the identity map at each stage. The unit morphism in HolEnd(tau).

Identity Map

Summary

The identity omega-germ transformer on a tau-admissible point x, defined by the identity map at each stage. The unit morphism in HolEnd(tau).

Statement

%
\label{def:identity-map}
The \textbf{identity map}
on a $\tau$-admissible point~$x$
is the $\omega$-germ transformer
$\mathrm{id}_x = \{\mathrm{id}_k\}_{k \geq 1}$
defined by
\[
    \boxed{%
    (\mathrm{id}_x)_k
    \;:=\;
    \mathrm{id}_{\mathbb{Z}/P_k\mathbb{Z}}
    \qquad \text{for all } k \geq 1,}
\]
the identity function
on the finite stage $\mathbb{Z}/P_k\mathbb{Z}$.
This is the \textbf{constant family}:
the identity germ at every stage.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 94
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part06/ch33-composition-structure.tex lines 225-244

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Hartogs.CategoryStructure
• Name: hol_identity

Dependencies

• Canonical: I.D49, II.D39

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.