nLab Schanuel topos

Idea

The Schanuel topos (also called the Myhill-Schanuel topos) is the Grothendieck topos of “combinatorial functors” whose “typical objects are natural combinatorial constructions such as binomial coefficients”¹. 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 category-theoretic variant of the Fraenkel-Mostowski model of set theory.

Definition

The Schanuel topos is the sheaf topos $Sh(FinSet^{op}_{mono},J)$ where $FinSet^{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\}\quad.$

Properties

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

• Since monos are precisely the morphisms that pull back along themselves to isomorphisms, any pullback preserving functor preserves monos. This affords another description as the category of intersection preserving functors from $FinSet_{mono}\to Set_{mono}$, a special case of combinatorial functors.

• The Schanuel topos $Sh(FinSet^{op}_{mono},J)$ is atomic over $Set$ (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.

• The Schanuel topos $Sh(FinSet^{op}_{mono},J)$ is locally finitely presentable since its category of atoms is co-well-founded? (cf. Marquès 2024).

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

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

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

• $Sh(FinSet^{op}_{mono},J)$ is contractible in the sense of natural homotopy (cf. Joyal-Wraith 1984).

Remark

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

Related Concepts

• nominal set

• locally decidable topos

• theory of decidable objects

• Fraenkel-Mostowski model

• combinatorial functor

• permutation model

• atomic topos

• species

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)

• André Joyal, Gavin Wraith, Eilenberg-Mac Lane Toposes and Cohomology , pp.117-131 in Cont. Math. 92 AMS 1984.

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

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

• Jérémie Marquès?, Atomic Toposes with Co-Well-Founded Categories of Atoms , arXiv:2406.14346 (2024). (abstract)

• 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)

• John Myhill, Recursive equivalence types and combinatorial functions , Bull. Amer. Math. Soc. 64 (1958) pp.373-376.

• Andrew M. Pitts, Nominal Sets - Names and Symmetry in Computer Science , Cambridge UP 2013. (Section 6.3)

• Alex Simpson, Equivalence and Conditional Independence in Atomic Sheaf Logic, arXiv:2405.11073 (2024). (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)

---

1. Lawvere 1989, p.299. ↩