Character Group

The set of all characters on L with pointwise multiplication. Every character traces back to the bipolar partition of primes.

Character Group

Summary

The set of all characters on L with pointwise multiplication. Every character traces back to the bipolar partition of primes.

Statement

%
\label{def:character-group}
The \textbf{character group} of $\mathbb{L}$ is the set
\[
    \boxed{%
    \mathrm{Char}(\mathbb{L})
    := \{ \chi : H_\tau \to \hat{\mathbb{Z}}_\tau[j]
    \mid \chi \text{ is a lemniscate character} \}}
\]
equipped with \textbf{pointwise multiplication}:
for characters $\chi_1, \chi_2 \in \mathrm{Char}(\mathbb{L})$,
\[
    (\chi_1 \cdot \chi_2)(x)
    := \chi_1(x) \cdot \chi_2(x)
    \quad \text{for all } x \in H_\tau.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 88
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part11/ch43-lemniscate-characters.tex lines 372-389

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.Characters
• Name: Tau.Boundary.chi_complete

Dependencies

• Canonical: I.D37

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.