12
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • 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$
    – Bas Spitters
    Commented 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$
    – Simon Henry
    Commented 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$
    – Matthias Hutzler
    Commented Oct 5, 2020 at 18:45

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .