nLab
realizability topos

Contents

Idea

A realizability topos is a topos which embodies the realizability interpretation of intuitionistic number theory (due to Kleene) as part of its internal logic. Realizability toposes form an important class of toposes that are not Grothendieck toposes, and don’t even have a geometric morphism to Set.

The input datum for forming a realizability topos is a partial combinatory algebra, or PCA.

Constructions

There are a number of approaches toward constructing realizability toposes. One is through tripos theory, and another is through assemblies.

Via tripos theory

…

Via assemblies

Definition

Let AA be a PCA. An (AA-)partitioned assembly XX consists of a set |X|{|X|} and a function [βˆ’] X:|X|β†’A[-]_X \colon {|X|} \to A. A morphism Xβ†’YX \to Y between partitioned assemblies is a function f:|X|β†’|Y|f \colon {|X|} \to {|Y|} for which there exists a∈Aa \in A such that a[x] Xa[x]_X is defined for all x∈Xx \in X and a[x] X=[f(x)] Ya[x]_X = [f(x)]_Y. The category of partitioned assemblies is denoted Pass APass_A.

Proposition

Pass APass_A is lextensive.

Theorem

The ex/lex completion of Pass APass_A is a topos, called the realizability topos of AA.

Remark

A general result about the ex/lex completion C ex/lexC_{ex/lex} of a left exact category CC is that it has enough regular projectives, meaning objects PP such that hom(P,βˆ’):C ex/lexβ†’Set\hom(P, -) \colon C_{ex/lex} \to Set preserves regular epis. In fact, the regular projective objects coincide with the objects of CC (as a subcategory of C ex/lexC_{ex/lex}). Of course, when C ex/lexC_{ex/lex} is a topos, where every epi is regular, this means C ex/lexC_{ex/lex} has enough projectives, or satisfies (external) COSHEP. It also satisfies internal COSHEP, since binary products of projectives, i.e., products of objects of CC, are again objects of CC (see this result).

Properties

Axiomatic characterization

The following is a statement characterizing realizability toposes which is analogous to the Giraud axioms characterizing Grothendieck toposes.

Theorem

A locally small category β„°\mathcal{E} is (equivalent to) a realizability topos precisely if

  1. β„°\mathcal{E} is exact and locally cartesian closed;

  2. β„°\mathcal{E} has enough projectives and the full subcategory Proj(β„°)β†ͺβ„°Proj(\mathcal{E}) \hookrightarrow \mathcal{E} has all finite limits;

  3. the global section functor Γ≔ℰ(*,βˆ’):β„°βŸΆ\Gamma \coloneqq \mathcal{E}(\ast,-) \colon \mathcal{E}\longrightarrow Set

    1. has a right adjoint βˆ‡:Setβ†ͺβ„°\nabla \colon Set \hookrightarrow \mathcal{E} (which is necessarily a reflective inclusion making βˆ‡Ξ“\nabla \Gamma a finite-limit preserving idempotent monad/closure operator);

    2. βˆ‡\nabla factors through Proj(β„°)Proj(\mathcal{E});

  4. there exists an object D∈Proj(β„°)D \in Proj(\mathcal{E}) such that

    1. DD is βˆ‡Ξ“\nabla\Gamma-separated (in that its (Ξ“βŠ£βˆ‡)(\Gamma \dashv \nabla)-unit is a monomorphism);

    2. all βˆ‡Ξ“\nabla \Gamma-closed regular epimorphisms have the left lifting property against Dβ†’*D\to \ast;

    3. for every projective object PP there is a βˆ‡Ξ“\nabla \Gamma-closed morphism Pβ†’DP \to D.

This is due to (Frey 14)

References

  • Stijn Vermeeren, Realizability Toposes, 2009 (pdf)

  • MatΓ­as Menni, Exact completions and toposes. Ph.D. Thesis, University of Edinburgh (2000). (web)

A characterization of realizability toposes analogous to the Giraud axioms for Grothendieck toposes is given in

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

\,

Revised on June 27, 2014 06:27:22 by Anonymous Coward (134.157.86.121)