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 ...

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 ...

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 ...

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 ...

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:
...

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 ...

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 ...

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$"....

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 ...

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 ...

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 ...

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 ...

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 ...

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" ...

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.
...

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 ...

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 ...

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 \...

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, ...

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-...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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.
...

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-...

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$-...

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

#### Related Tags

locales × 83ct.category-theory × 35

gn.general-topology × 28

topos-theory × 21

constructive-mathematics × 14

reference-request × 7

lattice-theory × 6

lo.logic × 5

measure-theory × 5

order-theory × 4

boolean-algebras × 4

ag.algebraic-geometry × 3

pr.probability × 3

real-analysis × 3

soft-question × 3

lattices × 3

infinity-topos-theory × 3

frames-and-locales × 3

higher-category-theory × 2

sheaf-theory × 2

limits-and-convergence × 2

von-neumann-algebras × 2

manifolds × 2

infinity-categories × 2

categorical-logic × 2