# Zulip Chat Archive

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

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

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)

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

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