Table of Contents
Fetching ...

Sketches and Classifying Logoi

Ivan Di Liberti, Gabriele Lobbia

TL;DR

It is shown that every rounded sketch has an associated classifying logos, having similar properties to the classifying topos of a geometric theory.

Abstract

Inspired by the theory of classifying topoi for geometric theories, we define rounded sketches and logoi and provide the notion of classifying logos for a rounded sketch. Rounded sketches can be used to axiomatise all the known fragments of infinitary first order logic in $\mathbf{L}_{\infty,\infty}$, in a spectrum ranging from weaker than finitary algebraic to stronger than $λ$-geometric for $λ$ a regular cardinal. We show that every rounded sketch has an associated classifying logos, having similar properties to the classifying topos of a geometric theory. This amounts to a Diaconescu-type result for rounded sketches and (Morita small) logoi, which generalises the one for classifying topoi.

Sketches and Classifying Logoi

TL;DR

It is shown that every rounded sketch has an associated classifying logos, having similar properties to the classifying topos of a geometric theory.

Abstract

Inspired by the theory of classifying topoi for geometric theories, we define rounded sketches and logoi and provide the notion of classifying logos for a rounded sketch. Rounded sketches can be used to axiomatise all the known fragments of infinitary first order logic in , in a spectrum ranging from weaker than finitary algebraic to stronger than -geometric for a regular cardinal. We show that every rounded sketch has an associated classifying logos, having similar properties to the classifying topos of a geometric theory. This amounts to a Diaconescu-type result for rounded sketches and (Morita small) logoi, which generalises the one for classifying topoi.
Paper Structure (30 sections, 29 theorems, 43 equations, 3 tables)

This paper contains 30 sections, 29 theorems, 43 equations, 3 tables.

Key Result

Theorem 1

The $2$-category $\mathsf{Log}^\mathsf{M}$ of Morita small logoi is (bi)reflective in the $2$-category $r\mathsf{Skt}^\mathsf{M}$, of Morita small rounded sketches. \begin{tikzcd}[ampersand replacement=\&] {\roundSkt^\moritaM} \& {\Log^\moritaM} \arrow[""{name=0, anchor=center, inner sep=0}, "U"',

Theorems & Definitions (107)

  • Theorem : Diaconescu for Logoi, \ref{['diaconescu']}
  • Definition 1.1.2: Notions of sketch
  • Definition 1.1.3: Morphism of Sketches
  • Remark 1.1.4: On the strictness of the notion of morphism
  • Definition 1.1.5: $2$-category of Sketches
  • Remark 1.1.6
  • Example 1.1.8: First order doctrines
  • Remark 1.1.9: Sketches are presentations!
  • Example 1.1.10: (Lex) sites
  • Theorem 1.1.12: Diaconescu
  • ...and 97 more