Composition of Holomorphic Maps

Composition of Holomorphic Maps

Composition of Holomorphic Maps

Summary

Composition of Holomorphic Maps

Statement

%
\label{def:composition}
Let $f = \{f_k\}_{k \geq 1}$
and $g = \{g_k\}_{k \geq 1}$
be $\omega$-germ transformers.
Their \textbf{composition} is the family
\[
    \boxed{%
    (g \circ f)_k
    \;:=\;
    g_k \circ f_k
    \qquad \text{for all } k \geq 1.}
\]
The composition is taken
in the split-complex codomain $H_\tau$:
at each stage~$k$,
$f_k$ maps $\mathbb{Z}/P_k\mathbb{Z} \to H_\tau$,
and $g_k$ acts on the image
via the $H_\tau$-valued germ structure.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D49, I.D20, I.T18, II.T26

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.