Skip to main content
61 votes
Accepted

How to rewrite mathematics constructively?

If you want a "general method" that "always works" to turn a classical theorem into a constructive one, there are double-negation translations: if you add enough $\neg\neg$s to a ...
Mike Shulman's user avatar
  • 65.4k
54 votes
Accepted

Constructive algebraic geometry

Let me wrote a quick introduction to this idea: 1) Locales I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk: They are a small variation on ...
Simon Henry's user avatar
  • 40.4k
20 votes
Accepted

Locales as geometric objects

First, if you haven't already you should have a look at this introductory paper by P.T. Johnstone The Art of pointless thinking which gives a lot of insight on how locale theory works. Here are some ...
Simon Henry's user avatar
  • 40.4k
16 votes
Accepted

Locales as spaces of ideal/imaginary points

I can only answer some of your questions. Yes, the Zariski locale is extensively studied. It's one of the ways of setting up scheme theory in a constructive context: Don't define schemes as locally ...
Ingo Blechschmidt's user avatar
15 votes
Accepted

Is it possible to completely embed complete Heyting Algebras into upsets of a poset?

No, not in general: for instance, the real interval $([0,1],{\le})$, or any non-atomic complete Boolean algebra, do not have such an embedding. This follows from the following characterization: ...
Emil Jeřábek's user avatar
15 votes
Accepted

Combination topological space and locale?

The proper term is topological system as found in Vickers' book Topology via Logic. Vickers actually uses precisely your expanded definition. What you call "topological" Vickers calls "spatial" and ...
Tomáš Jakl's user avatar
14 votes
Accepted

Is there a good theory of 2-locales?

A standard answer is in fact that Grothendieck toposes are categorified locales, with the argument that a Grothendieck topos that lacks enough points is not a tight generalization of a topological ...
Kevin Carlson's user avatar
14 votes

Localic or topos-theoretic definition of $\operatorname{Spec}$

The Zariski spectrum is essentially the classifying topos for prime ideal of $A$, or to be more precise, the classifying topos for subsets of $A$ that are "complement of prime ideals of $A$"....
Simon Henry's user avatar
  • 40.4k
13 votes
Accepted

Locales in constructive mathematics

For this type of question the first reference that comes to my mind is P.T.Johnstone Sketches of an elephant, part C. Most of the results in this book are constructively valid: If a result is proved ...
Simon Henry's user avatar
  • 40.4k
13 votes

Another notion of exactness: how to refine it, and where does it fit?

I'd like to argue that the current definition is too minimal to allow for much theory development, since the only substantial axiom is the pasting condition. In particular, it would be possible to ...
Tobias Fritz's user avatar
  • 5,795
12 votes

What are the 'wonderful consequences' following from the existence of a minimal dense subspace?

An example of an application of this appeared in Alex Simpson's paper called "Measure, Randomness and Sublocales" where Alex used this fact to resolve the Banach-Tarski paradox. Recall that $\mathbb ...
Tomáš Jakl's user avatar
12 votes

Locales as spaces of ideal/imaginary points

Here is a very brief sketches of the connection between this and forcing. I'll describe you how I understand forcing, this is quite different from how it is generally described by logician, but this ...
Simon Henry's user avatar
  • 40.4k
12 votes
Accepted

What are projective locales / injective frames?

So the short answer is that there is no non-empty projective locales for essentially any reasonable class of epimorphisms you can think of (except maybe proper maps). The problem is that there exists ...
Simon Henry's user avatar
  • 40.4k
12 votes

Every Grothendieck topos can be built from localic topoi

They are (it is?) the same theorem, but emphasising different aspects. We can exploit the object classifier to get from the formulation in terms of (pseudo)colimits to the "elementary" ...
Zhen Lin's user avatar
  • 14.9k
12 votes

Localic or topos-theoretic definition of $\operatorname{Spec}$

This is ultimately the same construction as the one Simon Henry describes, but you might like the different perspective. Definition. Let $A$ be a commutative rig and let $L$ be a distributive lattice. ...
Zhen Lin's user avatar
  • 14.9k
11 votes
Accepted

Which topological manifolds do not correspond to strongly Hausdorff locales?

Let me expand a bit my comment as this is a rather subtle property. As I said any locally compact Hausdorff topological space is a strongly hausdroff locally compact locales. (and under the axiom of ...
Simon Henry's user avatar
  • 40.4k
11 votes
Accepted

"Scott completion" of dcpo

I believe the paper by Johnstone linked to in the question contains the answer, and it is negative. In that paper, Johnstone constructs a Scott topology that is not sober as a byproduct of answering ...
მამუკა ჯიბლაძე's user avatar
11 votes
Accepted

What's the localic reflection of a presheaf topos?

I'm writing $\mathcal{O}(X)$ for the frame corresponding to $X$. Opens of $Y$ are sieves on $X$, i.e. the collection of open subsets $V \subset \mathcal{O}(X)$ such that $v \in V$ and $u \leqslant v \...
Simon Henry's user avatar
  • 40.4k
11 votes
Accepted

Every Grothendieck topos can be built from localic topoi

The groupoid representation of Joyal and Tierney may be identified with the truncated simplicial diagram appearing in the statement of Theorem 2 of the Lurie notes mentioned in the question. That is, ...
Tim Campion's user avatar
  • 61.9k
10 votes

What are the 'wonderful consequences' following from the existence of a minimal dense subspace?

I like to call this result the localic Baire category theorem, and it plays essentially the same role as Baire category theorem: it lets you "construct" object by showing that some spaces are non-...
Simon Henry's user avatar
  • 40.4k
10 votes

Localic or topos-theoretic definition of $\operatorname{Spec}$

Is there a construction of the spectrum of a ring, where it is defined as a locale or Grothendieck site generated by the D(f), and where the relation that D(fk)=D(f) is definitional? Yes, the Zariski ...
Dmitri Pavlov's user avatar
9 votes

Locales as geometric objects

While Simon's answer is very good, I think one can also say something a little more along the lines of what you may be thinking. I haven't seen this written out in this way before, so I may have made ...
Mike Shulman's user avatar
  • 65.4k
9 votes
Accepted

Does the functor $\mathrm{Sh}\colon\mathbf{Top}\to\mathbf{Topos}$ have an adjoint?

In this answer, Topos is interpreted as a 2-category. (As a side remark, the 1-category of toposes does not make sense until one picks a specific model for toposes and geometric morphisms, and ...
Dmitri Pavlov's user avatar
8 votes
Accepted

Product of topological spaces and product of corresponding locales

Your map $f$ is known to be an injective dense localic map. See, for example, Proposition 4.2.2 in [1]. In general, it isn't an isomorphism. The reason for this is that $\Omega(X \times_t Y)$ is ...
Tomáš Jakl's user avatar
8 votes
Accepted

Connections between $0$-toposes and $1$-toposes (Grothendieck and elementary)

Yes and no. As Jonas Frey pointed out on MSE, you can take the category of finite sheaves on any Heyting algebra $H$ to get an elementary topos. However, unlike in the case of frames and ...
Mike Shulman's user avatar
  • 65.4k
7 votes

Is it possible to completely embed complete Heyting Algebras into upsets of a poset?

Emil Jeřábek gave more complete answer than mine, so I have initially deleted it. On the afterthought, I decided to turn it into an addendum to Emil's answer. It is a generalization of sorts: if an ...
მამუკა ჯიბლაძე's user avatar
7 votes
Accepted

Best introductory texts on pointless topology

Topology via Logic - theoretical computer scientist Stone Spaces - pure mathematician Both are really good. Topology via logic as it gives a good account of domain theory, including power domains. ...
Christopher Townsend's user avatar
7 votes

How to rewrite mathematics constructively?

Are you aware that the (semantic) completeness theorem for countable first-order languages is equivalent over RCA0 (a weak subsystem of second-order arithmetic) to WKL0? Essentially the non-...
user21820's user avatar
  • 2,731
6 votes

Another notion of exactness: how to refine it, and where does it fit?

If you were willing to allow a generalization where "being exact" is structure on a square rather than a property of it, then there would be an example in the homotopy category of a stable $\infty$-...
Mike Shulman's user avatar
  • 65.4k

Only top scored, non community-wiki answers of a minimum length are eligible