Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Every theory is eventually of presheaf type

Christian Espíndola, Kristóf Kanalas

TL;DR

The paper develops a robust κ-site/κ-topos framework to analyze when a theory’s classifying topos is of presheaf type. It proves a completeness theorem for κ-lex categories, extends to classifying toposes via κ-toposes, and shows that, under enough $\lambda$-points and suitable cardinal arithmetic, the classifying $\lambda$-topos of a κ-site is equivalent to a presheaf topos. A key innovation is the use of locally covering cotrees to control extremal epimorphic coverings in a way compatible with $<\kappa$-limits, enabling a precise passage from theories to presheaf representations. The results yield practical criteria for when complex toposes can be treated as presheaf toposes, with downstream consequences for accessibility, model theory, and logical completeness in a categorical setting. The work also clarifies the role of $\lambda$-points and shows how λ-separability implies enough $\lambda$-points, reinforcing the presheaf-type conclusion under broad set-theoretic assumptions.

Abstract

We give a detailed and self-contained introduction to the theory of $λ$-toposes and prove the following: 1) A $λ$-separable $λ$-topos has enough $λ$-points. 2) The classifying $λ$-topos of a $κ$-site $(\mathcal{C},E)$ is a presheaf topos (assuming $κ\vartriangleleft λ=λ^{<λ}$, $|\mathcal{C}|,|E|<λ$).

Every theory is eventually of presheaf type

TL;DR

The paper develops a robust κ-site/κ-topos framework to analyze when a theory’s classifying topos is of presheaf type. It proves a completeness theorem for κ-lex categories, extends to classifying toposes via κ-toposes, and shows that, under enough -points and suitable cardinal arithmetic, the classifying -topos of a κ-site is equivalent to a presheaf topos. A key innovation is the use of locally covering cotrees to control extremal epimorphic coverings in a way compatible with -limits, enabling a precise passage from theories to presheaf representations. The results yield practical criteria for when complex toposes can be treated as presheaf toposes, with downstream consequences for accessibility, model theory, and logical completeness in a categorical setting. The work also clarifies the role of -points and shows how λ-separability implies enough -points, reinforcing the presheaf-type conclusion under broad set-theoretic assumptions.

Abstract

We give a detailed and self-contained introduction to the theory of -toposes and prove the following: 1) A -separable -topos has enough -points. 2) The classifying -topos of a -site is a presheaf topos (assuming , ).
Paper Structure (5 sections, 19 theorems)

This paper contains 5 sections, 19 theorems.

Table of Contents

  1. Introduction
  2. A completeness theorem
  3. Classifying toposes
  4. Eventually: enough points $\Rightarrow$ presheaf type
  5. A $\lambda$-separable $\lambda$-topos has enough $\lambda$-points

Key Result

theorem 1

$\mathcal{C}$ is $\kappa$-lex of local size $\leq \kappa$, and it has a strict initial object $\emptyset$. Let $E$ be a set of extremal epimorphic families, such that $|E|\leq \kappa$ and $E$ is compatible with $<\kappa$-limits. Then given any object $u_0\in \mathcal{C}$ there is a continuous cofina

Theorems & Definitions (58)

  • remark 1
  • definition 1
  • definition 2
  • definition 3
  • theorem 1
  • proof
  • theorem 2
  • proof
  • definition 4
  • remark 2
  • ...and 48 more