Countable Topos

PSh(Cat_tau) is a countable topos: Cat_tau has countable objects and at most one morphism between each pair (thin). Presheaves are countably generated by functions TauIdx -> Bool.

Countable Topos

Summary

PSh(Cat_tau) is a countable topos: Cat_tau has countable objects and at most one morphism between each pair (thin). Presheaves are countably generated by functions TauIdx -> Bool.

Statement

%
\label{prop:countable-topos}
$\mathrm{PSh}(\mathrm{Cat}_\tau)$
has a \textbf{countable} generating set.
Specifically:
\begin{enumerate}
    \item $|\Obj(\mathrm{Cat}_\tau)| = \aleph_0$.
    \item $|\mathrm{Mor}(\mathrm{Cat}_\tau)| = \aleph_0$.
    \item The representable presheaves
          $\{y(X)\}_{X \in \mathrm{Cat}_\tau}$
          form a countable generating set.
\end{enumerate}

Proof / Justification

\textbf{(1)} The objects of $\mathrm{Cat}_\tau$
are the elements of $\tau$-Idx $\cong \mathbb{N}$
(Proposition~\ref{prop:set-countable}, I.P12).

\textbf{(2)} The morphisms are pairs $(X, Y)$ with $X \mid Y$,
a subset of $\mathbb{N} \times \mathbb{N}$,
hence countable.

\textbf{(3)} The set $\{y(X)\}$
is indexed by $\tau$-Idx, hence countable.
By the Yoneda Lemma,
every presheaf is a colimit of representables,
so the representables generate.

Source Context

• Registry source: book-01.jsonl line 134
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch55-limits-sites.tex lines 497-510

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.LimitsSites
• Name: Tau.Topos.psh_countable_objects

Dependencies

• Canonical: I.D57, I.P25

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.