## Stream: maths

### Topic: topology on roption

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

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

#### Johan Commelin (May 23 2019 at 15:01):

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

#### Johan Commelin (May 23 2019 at 15:02):

Which I think corresponds to (b)

#### Reid Barton (May 23 2019 at 15:03):

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

#### Johan Commelin (May 23 2019 at 15:03):

I'll edit the post (-;

#### Reid Barton (May 23 2019 at 15:04):

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 (May 23 2019 at 15:06):

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

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

#### Chris Hughes (May 23 2019 at 15:45):

Is (a) even possible?

#### Mario Carneiro (May 23 2019 at 22:12):

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

#### 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\} \cup \{1/n\mid n\in\mathbb{N}\}$

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

#### 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)

#### Reid Barton (May 23 2019 at 22:19):

Oh, maybe this doesn't work either?

#### Reid Barton (May 23 2019 at 22:20):

because Mario just said {bot} should not be open

#### Reid Barton (May 23 2019 at 22:20):

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

#### Mario Carneiro (May 23 2019 at 22:20):

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

#### Mario Carneiro (May 23 2019 at 22:21):

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

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

#### Reid Barton (May 23 2019 at 22:24):

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

#### Mario Carneiro (May 23 2019 at 22:24):

oh, bot might be open if the space is finite

I think?

#### Mario Carneiro (May 23 2019 at 22:25):

it's weird turning topological intuitions into a topology

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

#### Reid Barton (May 23 2019 at 22:25):

OK, let me sit down and work this out properly

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

#### 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)

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

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

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

#### Chris Hughes (May 23 2019 at 22:44):

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

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

#### Reid Barton (May 23 2019 at 22:47):

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

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

#### 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)

Er wait

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

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

#### Reid Barton (May 23 2019 at 22:55):

Yeah, that sounds right

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

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

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