ayberkt
commented
2 months ago The possibility of adding a definition of spectral locale that is naturally propositional (i.e. not requiring truncation) was previously discussed in this pull request (in a review).
When I tried to do this, however, I came to the conclusion that this will actually not be that easy, which I have discussed with @martinescardo yesterday. Accordingly, we have decided not to do this for now. I will briefly document this discussion for future reference.
The current definition we have that expresses being isomorphic to the frame of ideals of a distributive lattice is the following:
is-spectral· : (X : Locale (𝓤 ⁺) 𝓤 𝓤) → Ω (𝓤 ⁺)
is-spectral· {𝓤} X = Ǝ L ꞉ DistributiveLattice 𝓤 , X ≅c≅ spec LThe distributive lattice whose existence is asserted by this definition is uniquely determined by the stipulation that its spectrum be isomorphic to X. The problem, however, is that the isomorphism itself might not be unique. Accordingly, we used Ǝ in the definition instead of Σ.
In univalent mathematics, the usual approach to this kind of problem is to specify the equivalence of interest. In this case, the equivalence is the map $𝒪(X) → \mathsf{Idl}(\mathcal{K}(X))$ sending an open of X to the ideal of compact opens below it.
However, there is a problem here, namely that the distributive lattice $\mathcal{K}(X)$ is not a priori small. This is problematic because our notion of ideal is defined on a distributive lattice, meaning this equivalence does not even typecheck in general.
Requiring $\mathcal{K}(X)$ to be small is a requirement we have in one notion of spectrality (is-spectral-with-small-basis), equivalent to 6 others.
One might think this definition might be possible for spectral locales with a small type of compact opens, but that also does not quite work (in our current setting). The reason is that the type $\mathcal{K}(X)$ being small will not allow us to resize down the distributive lattice of compact opens as to allow us to can speak its type of ideals. We also need the compact opens to be closed under binary meets for this purpose.
The condition that will allow us to speak of this equivalence (using distributive lattices) is very close to the definition of spectral locale itself, so this seems kind of silly.
One could instead generalize the notion of ideal as to be defined a join-semilattice, and not a distributive lattice (which is defined to be a join and meet lattice). Because compact opens are always closed under binary joins, they are always a join-semilattice. The smallness of $\mathcal{K}(X)$ will allow us to resize down the join-semi-lattice of compact opens and then speak of this equivalence. But as mentioned before, there is no reason for us to do this at the moment so we leave it for further work.
tomdjong
martinescardo
Fixes #268.