nLab
Schanuel topos

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

The Schanuel topos (also called the Myhill-Schanuel topos) is the Grothendieck topos of combinatorial functors. It plays an important role in computer science in the theory of name-binding calculi and in William Lawvere‘s approach to petit toposes. It can be viewed as a categorical variant of the Fraenkel-Mostowski model of set theory.

Definition

The Schanuel topos is the sheaf topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) where FinSet mono opFinSet^{op}_{mono} is the opposite of the category of finite sets and monomorphisms and the coverage is the collection of all sieves generated by singletons {f}.\{f\}\quad.

Properties

  • The objects of the Schanuel topos are called nominal sets and correspond precisely to the pullback preserving functors FinSet monoSetFinSet_{mono}\to Set.

  • The Schanuel topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is atomic over SetSet (S. Schanuel, cf. (Wraith 1978), p.335) hence Boolean. This fact can be viewed as a reflex of the urelements in Fraenkel-Mostowski set theory.

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the classifying topos Set[D ]Set[D_\infty] for the theory of infinite decidable objects D D_\infty i.e. for a Grothendieck topos \mathcal{E} geometric morphisms Sh(FinSet mono op,J)\mathcal{E}\to Sh(FinSet^{op}_{mono},J) correspond to infinite decidable objects in \mathcal{E}. Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is equivalent to Sh ¬¬([FinSet mono,Set])Sh_{\neg\neg}([FinSet_mono,Set]).

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the category of continuous actions for the group of bijections of NN equipped with the topology derived from the product topology for NN.\prod_{N}N\quad .

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the Kleisli category of the monad on the topos of species Set FinSet isoSet^{FinSet_{iso}} induced by the inclusion of finite sets and bijections FinSet isoFinSet monoFinSet_{iso}\hookrightarrow FinSet_{mono} (cf. Fiore-Menni 2004).

Remark

For some information on the history of the Schanuel topos see section 10 of Menni (2009, pp.529f).

References

  • M. Fiore, M. Menni, Reflective Kleisli Subcategories of the Category of Eilenberg-Moore Algebras for Factorization Monads , TAC 15 no. 2 (2004) pp.40-65. (pdf)

  • M. J. Gabbay, A. M. Pitts, A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13 (2002) pp.341-363. (draft)

  • Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002. (pp.79f, 691, 925)

  • F. William Lawvere, Qualitative Distinctions between some Toposes of Generalized Graphs , Cont. Math. 92 (1989). (pp.298f)

  • S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994. (pp.155, 158)

  • Matías Menni, About N-quantifiers , Appl. Cat. Struc. 11 (2003) pp.421-445. (preprint)

  • Matías Menni, Algebraic categories whose projectives are explicitly free , TAC 22 no.20 (2009) pp.509-541. (abstract)

  • Sam Staton, Name-passing process calculi: operational models and structural operational semantics, Technical Report 688 CL University Cambridge 2007. (pdf)

  • G. Wraith, Intuitionistic Algebra: Some Recent Developments of Topos Theory , Proc. ICM Helsinki (1978) pp.331-337. (pdf)

Last revised on August 5, 2016 at 10:07:44. See the history of this page for a list of all contributions to it.