Characteristic Morphism

The characteristic morphism chi_S: X -> Omega_tau assigns a Truth4 value based on B-sector and C-sector membership. T = both confirm, F = both deny, B = overdetermined, N = underdetermined. Pullback of true along chi recovers the subobject.

Characteristic Morphism

Summary

The characteristic morphism chi_S: X -> Omega_tau assigns a Truth4 value based on B-sector and C-sector membership. T = both confirm, F = both deny, B = overdetermined, N = underdetermined. Pullback of true along chi recovers the subobject.

Statement

%
\label{def:characteristic-morphism}
Let $m : S \hookrightarrow X$ be a monomorphism
in $\mathrm{PSh}(\mathrm{Cat}_\tau)$.
The \textbf{characteristic morphism} of $S$ in $X$ is the
unique natural transformation
\[
    \boxed{%
    \chi_S : X \to \Omega_\tau}
\]
from Theorem~\ref{thm:omega-tau-classifier}:
for each object $c$ and element $x \in X(c)$,
\[
    \chi_S(x) :=
    \mathrm{membership}_S(x, c)
    \in \{\mathsf{T}, \mathsf{F}, \mathsf{B}, \mathsf{N}\}.
\]
The defining property is the pullback square:
$S = \chi_S^{-1}(\mathsf{T})
= \{x \in X : \chi_S(x) = \mathsf{T}\}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 136
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch56-earned-topos.tex lines 277-298

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.EarnedTopos
• Name: Tau.Topos.characteristic_morphism

Dependencies

• Canonical: I.T25

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.