Let $\mathbb{T}$ be a geometric theory. Let $\mathrm{Set}[\mathbb{T}]$ be its classifying topos, such that geometric morphisms from any (cocomplete) topos $\mathcal{E}$ into $\mathrm{Set}[\mathbb{T}]$ are in canonical one-to-one correspondence with models of $\mathbb{T}$ in $\mathcal{E}$.

As with any topos, associated to $\mathrm{Set}[\mathbb{T}]$ is its localic reflection $L(\mathrm{Set}[\mathbb{T}])$, the locale which has the partially ordered set $\mathrm{Sub}_{\mathrm{Set}[\mathbb{T}]}(1)$ as frame of opens. Like any locale, this locale is the classifying locale of some propositional geometric theory $\mathbb{T}'$.

Question: Can the theory $\mathbb{T}'$ be described in terms of $\mathbb{T}$?

For instance, let $\mathbb{T}$ the theory of an object, containing a single sort and no axioms. Then $\mathrm{Set}[\mathbb{T}]$ is the object classifier, the copresheaf topos $[\mathrm{FinSet}, \mathrm{Set}]$. Its localic reflection is the one-point locale, so $\mathbb{T}'$ is the empty theory.

My motivation is that I want to find out whether a certain geometric $\mathcal{F} \to \mathcal{E}$ morphism is open. For this, I have to check whether its localic reflection is open (as a locale internal to $\mathcal{E}$); if I knew which theory the localic reflection classifies, I'd have a handle on this.

An obvious place to look for an answer would be Olivia Caramello's beautiful paper on lattices of theories. However, there she discusses only subtoposes, not the localic reflection.

  • 3
    $\begingroup$ We computed the localic reflection using geometric methods in Thm 24 here: arxiv.org/abs/1310.0705 The methods are more general, and you will find more information in the work by Steve Vickers. Unfortunately, I don't have time to find the precise references now. $\endgroup$ Jun 1, 2017 at 11:20
  • $\begingroup$ In general, I think one can only say the obvious thing: T' is the " theory of geometric formula without free variables of T ". (i.e. a propositional theory which has one proposition for each geometric proposition of T without free variables and which proves exactly the same implication between these propositions as T does.) $\endgroup$ Feb 27, 2018 at 18:16
  • 2
    $\begingroup$ I think the object classifier example isn't correct. The localic reflection of the object classifier is the Sierpinski space (classifying the theory with one proposition symbol); the nontrivial geometric formula without free variables in the one sort theory is "the sort is inhabited". $\endgroup$ Oct 5, 2020 at 18:45


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.