Zulip Chat Archive

Stream: maths

Topic: topology on roption


view this post on Zulip Reid Barton (May 23 2019 at 14:57):

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.

view this post on Zulip Reid Barton (May 23 2019 at 14:59):

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.

view this post on Zulip Johan Commelin (May 23 2019 at 15:01):

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

view this post on Zulip Johan Commelin (May 23 2019 at 15:02):

Which I think corresponds to (b)

view this post on Zulip Reid Barton (May 23 2019 at 15:03):

What do you mean by ++? Disjoint union?

view this post on Zulip Johan Commelin (May 23 2019 at 15:03):

I'll edit the post (-;

view this post on Zulip Reid Barton (May 23 2019 at 15:04):

For YY 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"

view this post on Zulip Johan Commelin (May 23 2019 at 15:06):

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

view this post on Zulip Reid Barton (May 23 2019 at 15:06):

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

view this post on Zulip Chris Hughes (May 23 2019 at 15:45):

Is (a) even possible?

view this post on Zulip Mario Carneiro (May 23 2019 at 22:12):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:14):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:16):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:19):

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)

view this post on Zulip Reid Barton (May 23 2019 at 22:19):

Oh, maybe this doesn't work either?

view this post on Zulip Reid Barton (May 23 2019 at 22:20):

because Mario just said {bot} should not be open

view this post on Zulip Reid Barton (May 23 2019 at 22:20):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:20):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:21):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:23):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:24):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:24):

oh, bot might be open if the space is finite

view this post on Zulip Mario Carneiro (May 23 2019 at 22:24):

I think?

view this post on Zulip Mario Carneiro (May 23 2019 at 22:25):

it's weird turning topological intuitions into a topology

view this post on Zulip Reid Barton (May 23 2019 at 22:25):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:25):

OK, let me sit down and work this out properly

view this post on Zulip Reid Barton (May 23 2019 at 22:27):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:27):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 22:28):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:39):

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

view this post on Zulip Chris Hughes (May 23 2019 at 22:39):

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.

view this post on Zulip Chris Hughes (May 23 2019 at 22:44):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:44):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:47):

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

view this post on Zulip Chris Hughes (May 23 2019 at 22:50):

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.

view this post on Zulip Reid Barton (May 23 2019 at 22:51):

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

view this post on Zulip Reid Barton (May 23 2019 at 22:51):

Er wait

view this post on Zulip Reid Barton (May 23 2019 at 22:52):

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

view this post on Zulip Chris Hughes (May 23 2019 at 22:54):

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.

view this post on Zulip Reid Barton (May 23 2019 at 22:55):

Yeah, that sounds right

view this post on Zulip Mario Carneiro (May 23 2019 at 23:07):

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

view this post on Zulip Mario Carneiro (May 23 2019 at 23:08):

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

view this post on Zulip Mario Carneiro (May 24 2019 at 02:48):

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


Last updated: May 09 2021 at 11:09 UTC