Identity-Faithful Reception

Identity-faithful reception: a VM system S can receive tau ontically only if there exists an interpretation functor P: C_tau -> C_S that is faithful on identity — reflects equality/isomorphism back to tau-identity, preserves identity morphisms, and maps distinct tau-objects to distinct S-objects.

Identity-Faithful Reception

Summary

Identity-faithful reception: a VM system S can receive tau ontically only if there exists an interpretation functor P: C_tau -> C_S that is faithful on identity — reflects equality/isomorphism back to tau-identity, preserves identity morphisms, and maps distinct tau-objects to distinct S-objects.

Statement

%
\label{def:identity-faithful-reception}
A virtual machine system $\mathsf{S}$
can \textbf{receive $\tau$ ontically}
only if there exists an interpretation functor
$P : \mathcal{C}_\tau \to \mathcal{C}_{\mathsf{S}}$
satisfying three conditions:
\begin{enumerate}[\normalfont(i)]
    \item \textbf{Object distinctness.}
          $P$ maps distinct $\tau$-objects to distinct $\mathsf{S}$-objects:
          if $X \neq Y$ in $\mathcal{C}_\tau$,
          then $P(X) \neq P(Y)$ in $\mathcal{C}_{\mathsf{S}}$.
    \item \textbf{Identity preservation.}
          $P$ preserves identity morphisms:
          $P(\mathrm{id}_X) = \mathrm{id}_{P(X)}$
          for every object $X$ of $\mathcal{C}_\tau$.
    \item \textbf{Isomorphism reflection.}
          $P$ reflects isomorphism:
          if $P(X) \cong P(Y)$ in $\mathcal{C}_{\mathsf{S}}$,
          then $X \cong Y$ in $\mathcal{C}_\tau$.
\end{enumerate}
Such a functor is called
\textbf{identity-faithful}.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 207
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part18/ch82-reception-criterion.tex lines 115-139

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.MetaLogic.ReceptionCriterion
• Name: Tau.MetaLogic.IdentityFaithfulReception

Dependencies

• Canonical: I.D89, I.D90, I.T46

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.