Generation of Grothendieck topologies, provability and operations on subtoposes

TL;DR

This paper explores the duality between Grothendieck topologies and subtoposes, introduces geometric operations on subtoposes, and provides formulas for generating topologies, thereby linking logic and geometry in topos theory.

Contribution

It presents a new formulation of the duality between Grothendieck topologies and subtoposes, along with formulas for topology generation and analysis of geometric operations.

Findings

Formulas for generating Grothendieck topologies from families of sieves.

Refined procedures translating logical provability into topology generation.

Proved that pullback operations preserve intersections and unions of subtoposes.

Abstract

After reviewing the multiple roles of toposes - as generalized topological spaces, as universal invariants, as categorical analogues of the set-theoretic universe, and as semantic environments for first-order theories - we recall the notion of subtopos and its dual expression: both in terms of Grothendieck topologies and in terms of first-order logic. We emphasize the significance of this duality, which enables the translation of provability problems in first-order logic into problems concerning the generation of Grothendieck topologies. We also introduce the natural geometric operations, both inner and outer, on subtoposes. Building on these foundations, we present a new formulation of the duality between Grothendieck topologies and subtoposes, as well as the duality between topologies and closedness properties of subpresheaves. This presentation relies on general categorical principles and aims to clarify the structural relationships involved. We then provide two general formulas for the Grothendieck topology generated by an arbitrary family of sieves or covering families of morphisms. In addition, we refine the constructive procedures that translate logical provability into topology generation, highlighting their role in bridging logic and geometry within the topos-theoretic framework. Finally, we study the inner geometric operations on subtoposes: union, intersection, and difference, along with the outer adjoint operations of pushforward and pullback along topos morphisms. We prove that pullback operations preserve not only arbitrary intersections but also finite unions of subtoposes, and that pullbacks along locally connected morphisms even preserve arbitrary unions.