Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction

Maria Emilia Maietti, Davide Trotta

TL;DR

The paper introduces an algebraic framework that abstracts localic presheaves and their sheafification through the tripos-to-topos lens, unifying localic and realizability toposes as instances of $ ext{T}_{P^{ ext{∃}}}$ for $ ext{∃}$-supercompactifiable triposes $P$. By defining the abstract presheaf category $E_P := ( ext{G}_P)_{ex/lex}$ and the full existential completion $P^{ ext{∃}}$, it shows $E_P$ is equivalent to the topos $ ext{T}_{P^{ ext{∃}}}$ and characterizes when this yields a topos in terms of $P^{ ext{∃}}$ being a tripos. The authors establish criteria for $ ext{∃}$-supercompactifiability, including a new equivalence with weak dependent products and a generic proof in the category of points, and show that Set-based triposes (under Choice) are all $ ext{∃}$-supercompactifiable with numerous examples. They further demonstrate that, for such triposes, the associated topos can be realized as a sheaf topos $ ext{Sh}_j( ext{T}_{P^{ ext{∃}}})$ for a Lawvere–Tierney topology $j$, thereby providing a generalized localic Comparison Lemma and a flexible framework for fibrational extensions to predicative toposes.

Abstract

Localic and realizability toposes are two central classes of toposes in categorical logic, both arising through the Hyland-Johnstone-Pitts tripos-to-topos construction. We investigate their shared geometric features by providing an algebraic abstraction of the notions of localic presheaves, sheafification and their connection to supercompactification of a locale via an instance of the Comparison Lemma. This can be applied to a broad class of toposes obtained to the tripos-to-topos constructions, including all those generated from a tripos based on the classical category of ZFC-sets. These results provide a unified geometric framework for understanding localic and realizability toposes.

An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction

TL;DR

The paper introduces an algebraic framework that abstracts localic presheaves and their sheafification through the tripos-to-topos lens, unifying localic and realizability toposes as instances of for -supercompactifiable triposes . By defining the abstract presheaf category and the full existential completion , it shows is equivalent to the topos and characterizes when this yields a topos in terms of being a tripos. The authors establish criteria for -supercompactifiability, including a new equivalence with weak dependent products and a generic proof in the category of points, and show that Set-based triposes (under Choice) are all -supercompactifiable with numerous examples. They further demonstrate that, for such triposes, the associated topos can be realized as a sheaf topos for a Lawvere–Tierney topology , thereby providing a generalized localic Comparison Lemma and a flexible framework for fibrational extensions to predicative toposes.

Abstract

Localic and realizability toposes are two central classes of toposes in categorical logic, both arising through the Hyland-Johnstone-Pitts tripos-to-topos construction. We investigate their shared geometric features by providing an algebraic abstraction of the notions of localic presheaves, sheafification and their connection to supercompactification of a locale via an instance of the Comparison Lemma. This can be applied to a broad class of toposes obtained to the tripos-to-topos constructions, including all those generated from a tripos based on the classical category of ZFC-sets. These results provide a unified geometric framework for understanding localic and realizability toposes.

Paper Structure

This paper contains 15 sections, 46 theorems, 38 equations.

Table of Contents

  1. Introduction
  2. Preliminaries on doctrines and triposes
  3. Lex primary and full existential doctrines
  4. Hyperdoctrines and triposes
  5. Tripos-to-topos construction
  6. Abstracting localic presheaves for lex primary doctrines
  7. Abstracting localic supercompactification for lex primary doctrines
  8. Abstracting Localic Comparison Lemma for lex primary doctrines
  9. Preliminaries on the regular and exact completion of a doctrine
  10. Abstracting the localic Comparison Lemma
  11. A charaterization of abstract localic presheaves toposes
  12. A characterization of $\exists$-supercompactifiable triposes
  13. Closure of $\exists$-supercompactifiable triposes under slicing
  14. Abstracting localic sheafification
  15. Conclusion

Key Result

Lemma 2.16

If $P\colon \mathcal{C}^{\operatorname{ op}}\longrightarrow\mathsf{InfSl}$ has a weak predicate classifier and the base category is weakly cartesian closed then, for every object $A$ of $\mathcal{C}$, we can define an object $\mathrm{P}A:=\Omega^A$ and an element $\in_A:=P_{\mathsf{ev}}(\in)$ of $P(

Theorems & Definitions (122)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Example 2.4
  • Example 2.5
  • Definition 2.6
  • Remark 2.7
  • Definition 2.8
  • Example 2.9: subobjects doctrine
  • Example 2.10: weak-subobjects doctrine
  • ...and 112 more