Table of Contents
Fetching ...

Solution to Lawvere's first problem: a Grothendieck topos that has proper class many quotient topoi

Yuhi Kamio, Ryuya Hora

TL;DR

The paper resolves Lawvere's first open problem by constructing a Grothendieck topos with a proper class of quotient topoi, exemplified by the presheaf topos $\mathbf{PSh}(M_{\omega})$ on the countably generated free monoid. The strategy introduces the encoding topos $\mathcal{E}_{\mathcal{L}}$ and the classifying topos of inhabited objects $\mathbb{A}^{\circ}$, then reduces quotient-topoi considerations to rigidity phenomena via inhabited-topos-rigid objects and a pairing mechanism. A key component is the development of a length/minimal-expression theory for objects in the classifying topos $\textbf{A}$ and its inhabited subtopos $\textbf{A}^{\circ}$, enabling precise control over endomorphisms and projections. The main technical achievements are: (i) showing the existence of proper class many inhabited-topos-rigid objects in the encoding topos through a Relational-Structure framework, (ii) constructing a countable relational language $\mathcal{L}$ yielding proper class many non-isomorphic inhabited-lex-rigid $\mathcal{L}$-structures, and (iii) establishing a presheaf-encoding bridge in which $\mathcal{E}_{\mathcal{L}}$ is a quotient topos of $\mathbf{PSh}(M_{\omega})$ (and vice versa), thereby solving Lawvere's problem in a concrete setting with explicit encodings.

Abstract

This paper solves the first of the open problems in topos theory posted by William Lawvere, concerning the existence of a Grothendieck topos that has proper class many quotient topoi. This paper concretely constructs such Grothendieck topoi, including the presheaf topos on the free monoid generated by countably infinitely many elements PSh(M_ω). Utilizing the combinatorics of the classifying topos of the theory of inhabited objects and with the help of a system of pairing functions, the problem is reduced to a theorem of Vopenka, Pultr, and Hedrlin, which states that any set admits a rigid relational structure.

Solution to Lawvere's first problem: a Grothendieck topos that has proper class many quotient topoi

TL;DR

The paper resolves Lawvere's first open problem by constructing a Grothendieck topos with a proper class of quotient topoi, exemplified by the presheaf topos on the countably generated free monoid. The strategy introduces the encoding topos and the classifying topos of inhabited objects , then reduces quotient-topoi considerations to rigidity phenomena via inhabited-topos-rigid objects and a pairing mechanism. A key component is the development of a length/minimal-expression theory for objects in the classifying topos and its inhabited subtopos , enabling precise control over endomorphisms and projections. The main technical achievements are: (i) showing the existence of proper class many inhabited-topos-rigid objects in the encoding topos through a Relational-Structure framework, (ii) constructing a countable relational language yielding proper class many non-isomorphic inhabited-lex-rigid -structures, and (iii) establishing a presheaf-encoding bridge in which is a quotient topos of (and vice versa), thereby solving Lawvere's problem in a concrete setting with explicit encodings.

Abstract

This paper solves the first of the open problems in topos theory posted by William Lawvere, concerning the existence of a Grothendieck topos that has proper class many quotient topoi. This paper concretely constructs such Grothendieck topoi, including the presheaf topos on the free monoid generated by countably infinitely many elements PSh(M_ω). Utilizing the combinatorics of the classifying topos of the theory of inhabited objects and with the help of a system of pairing functions, the problem is reduced to a theorem of Vopenka, Pultr, and Hedrlin, which states that any set admits a rigid relational structure.
Paper Structure (17 sections, 30 theorems, 39 equations)

This paper contains 17 sections, 30 theorems, 39 equations.

Key Result

Proposition 3.5

For a Grothendieck topos $\mathcal{E}$, an object $X \in \mathrm{ob}(\mathcal{E})$, and an object $F\in \mathrm{ob}(\mathbb{A})$, the object $X\otimes F$ is given by the following coend: where the object $X^A$ is the $A$-times product of the object $X$ and $X^A \times FA$ is its $FA$-times coproduct. In particular, if the topos $\mathcal{E}$ is the category of sets $\mathbf{Set}$ and the object $

Theorems & Definitions (81)

  • Definition 2.1
  • Definition 2.2
  • Remark 2.3: Equivalence of quotient topoi
  • Remark 3.4: As a left Kan extension
  • Proposition 3.5
  • Lemma 3.8
  • proof
  • Lemma 3.9
  • Proposition 3.10
  • proof
  • ...and 71 more