topology on roption

Stream: maths

[Reid Barton]

A good way to set up this question of the topology on roption X is to ask what universal property it should have/what functor it should represent. We already that an arbitrary function f : X -> roption Y corresponds to a S : set X and a function g : S -> Y. Then we could choose one of several conditions for f to be continuous, for example:
(a) f is continuous iff g is continuous;
(b) f is continuous iff s is open and g is continuous;
((c) f is continuous iff s is closed and g is continuous; I don't think this is at all useful for the application of defining manifolds, but the point is the list of options is open-ended...)
For each of these options, there is at most one topology on roption Y making it hold (by the Yoneda lemma). Then we have a little exercise to determine whether the topology really exists and if so what it looks like.
The point is that we're really going to use the fact (a)/(b) to work with this topology anyways--the exact construction of the topology is less important.

[Reid Barton]

If Y is a point, then a function X -> roption Y corresponds to just a subset S of X and in this case I happen to know that the answers are
(a) the indiscrete topology (\bot) on roption Y,
(b) the Sierpinski topology on roption Y ~ Prop,
((c) the Sierpinski topology on roption Y ~ Prop but with the roles of the points reversed via not).
So I guess that there are probably solutions for general Y as well.

[Johan Commelin]

I guess you just want $\text{roption}\ Y = Y \sqcup \{*\}$

[Johan Commelin]

Which I think corresponds to (b)

[Reid Barton]

What do you mean by $+$? Disjoint union?

[Johan Commelin]

I'll edit the post (-;

[Reid Barton]

For $Y$ a point none of these options are the disjoint union with a separate point. That would correspond to (d) "s is both closed and open and g is continuous"

[Johan Commelin]

Aah, you are right... I'm being to quick. I'll think while walking to the train station.

[Reid Barton]

In the original correspondence between maps to roption and partial functions, the domain s of the partial function is the inverse image of the subset some _, so if this latter subset of roption Y is open/closed then s has to be too

[Chris Hughes]

Is (a) even possible?

[Mario Carneiro]

I would like (a), but I think it is impossible

[Mario Carneiro]

Also {bot} should not be open. Here's another special case: when Y = nat it should be homeomorphic to $\{0\} \cup \{1/n\mid n\in\mathbb{N}\}$

[Mario Carneiro]

by contrast, {none} is open in the topology on option A, so that makes the difference between them a bit clearer

[Reid Barton]

What happens if I take: a set in roption Y is open if it's either empty or the union of {bot} and the image of an open subset of Y. (This is working classically for now)

[Reid Barton]

Oh, maybe this doesn't work either?

[Reid Barton]

because Mario just said {bot} should not be open

[Reid Barton]

OK, so I guess the existence of choice (a) for Y a point is a coincidence

[Mario Carneiro]

I don't think bot should be in every open set

[Mario Carneiro]

And the subspace of non-bot should be homeo to Y

[Mario Carneiro]

What about a set is open if it is open in Y, or it contains bot and another point and the restriction to Y is open in Y

[Reid Barton]

I wanted to do that but it's not closed under intersection.

[Mario Carneiro]

oh, bot might be open if the space is finite

[Mario Carneiro]

I think?

[Mario Carneiro]

it's weird turning topological intuitions into a topology

[Reid Barton]

That's appealing because we know for Y a point, roption Y is supposed to have just two open sets and yet Y already has two open sets and they should somehow correspond to each other

[Reid Barton]

OK, let me sit down and work this out properly

[Reid Barton]

What's tricky about this is that open sets in roption Y correspond to maps out of it to the Sierpinski space, but we only have direct information about maps into roption Y

[Mario Carneiro]

I think roption unit should be {bot, unit}, {unit}, (/) which is the Sierpinski space (I always forget the orientation)

[Mario Carneiro]

There is a canonical map from roption Y to Prop with the sierpinski topology, that's dom

[Reid Barton]

Okay, I have a somewhat hackish case analysis proof that it can't be done for Y a two-point discrete space

[Chris Hughes]

I think you need none to not be contained in any open set other than univ, Take s = (0, 3) and f =subtype.val, then g^-1((1,2)union{none}) is not open.

[Chris Hughes]

Maybe there's a different topology that works when s is closed as well.

[Reid Barton]

(Here's the argument. We may as well work classically, so write Y = {a,b} and roption Y = {a, b, bot}. Neither {a, b} nor {bot} can be open because that would force the domain of any partial map to be open/closed. If {a} is open then {b} has to be too, by uniqueness, contradicting {a, b} not open. Similarly {a, bot} cannot be open because then {bot} would be the intersection of the opens {a, bot} and {b, bot}. But then none of the open sets distinguish a from b, so the topology cannot possibly detect whether or not a total map is continuous.)

[Reid Barton]

I feel like the original option (b) has better chances, I'm less sure about (c)

[Chris Hughes]

I think the best you can do is s is open implies f continuous iff g continuous, which would just be the topology generated by the open sets in Y.

[Reid Barton]

I can also force s to be open by making the complement of {bot} open (at least classically)

[Reid Barton]

Er wait

[Reid Barton]

That's also one of the open sets in Y of course. So I think that topology works.

[Chris Hughes]

You could have a version that works for closed s as well, by generating the closed sets in roption Y from the closed sets in Y.

[Reid Barton]

Yeah, that sounds right

[Mario Carneiro]

I think this is right. From a computation point of view, if you haven't eliminated none yet, then the computation is still under way and so every answer is possible. So this corresponds to the open set univ

[Mario Carneiro]

I guess enat is a bit different since you think of computations as eliminating nats successively until you have only top remaining, so you get the one point compactification

[Mario Carneiro]

I was expecting this to be a special case of one of our existing general topological constructions, but it doesn't look like this is the case. It's not topological_space.coinduced roption.some because that topology is too fine. The generalization here is, given a function f : A -> B (probably injective), define a topology on B to be generated by the images of open sets in A. This is the coarsest topology that makes f an open map