One point compactification

Stream: Is there code for X?

[Yourong Zang]

The canonical topology of roption is very unclear to me. It seems that the topology can be constructed by either inducing on some map with specific preimages or with filters of complements of compact + closed sets. But I couldn't really find the names/definitions of these filters or maps in Zulip or mathlib. I apologize if this is a stupid question. Any help will be appreciated.

[Yury G. Kudryashov]

I see no instances for topological_space (roption X) or topological_space (option X) in mathlib. Do you want to define it as the one point compactification or you see this definition somewhere and can't understand it?

[Yury G. Kudryashov]

We have docs#filter.cocompact. Will it help you?

[Yourong Zang]

Yury G. Kudryashov said:

I see no instances for topological_space (roption X) or topological_space (option X) in mathlib. Do you want to define it as the one point compactification or you see this definition somewhere and can't understand it?

Thank you for the information! I saw this thread and this one, but I've never seen an actual instance in the forms mentioned in those posts. It seems that people agree that the construction in the first post is not done in the correct generality.

I want to define the one-point compactification as a topological structure on roption rather than a quotient of sum X X.

We have docs#filter.cocompact. Will it help you?

I'm sure this would do the job for the compactification of roption on a Hausdorff space. Thanks a lot!

[Yaël Dillies]

Are you sure you want use roption and not option? roption is intended for computability results and mostly necessary to get around decidability issues.

[Eric Wieser]

I've seen comments that say "roption and option have a different topology", but don't have the background to understand what is meant by that.

[Yaël Dillies]

Oh, are people using them as type synonyms or something?

[Yourong Zang]

Eric Wieser said:

I've seen comments that say "roption and option have a different topology", but don't have the background to understand what is meant by that.

I also saw a similar comment. This one

[Yourong Zang]

Yaël Dillies said:

Are you sure you want use roption and not option? roption is intended for computability results and mostly necessary to get around decidability issues.

I can use option if there is no huge difference in the topological construction :).

[Mario Carneiro]

They "morally" have a topology based on their intuitionistic structure, but the topology is not literally implemented as an instance of topological_space in mathlib because these types are usually too generic to be used directly for their topologies. The topologies in question are:

• option A has the disjoint sum topology, the same as A + 1: sets in A are open and {none} is also open.
• roption A has the one point compactification topology: sets in A are open and sets containing none and also cocompact are also open.

[Kevin Buzzard]

I would strongly recommend option. It's much easier to use.

[Kevin Buzzard]

The "topology" which people are talking about is something to do with constructive mathematics and you can imagine it as unrelated to the topology questions you're thinking about.

[Mario Carneiro]

If you want these types for their topologies, I recommend adding a type synonym that implements the topology. In practice I think you would want to use option A as the base type for both topologies anyway

[Kevin Buzzard]

e.g. when Mario says "roption A has the one point compactification topology" he doesn't actually mean "if A has a topology then roption A will get one too and it will be the one point compactification", he is just explaining the way constructivists think topologically about things.

[Yaël Dillies]

Mario Carneiro said:

• option A has the disjoint sum topology, the same as A + 1: sets in A are open and {none} is also open.
• roption A has the one point compactification topology: sets in A are open and sets containing none and also cocompact are also open.

This feels like a type job's synonym.

[Yaël Dillies]

*A type synonym's job!

[Eric Wieser]

I assume the moral claim is something like "if you swap the topologies around you'd need choice to define at leats one of them"?

[Mario Carneiro]

it's actually somewhat hard to write the moral claim formally, because constructivist's "continuous" means "definable without choice"

[Mario Carneiro]

so the literal implementations using topological_space don't and can't capture this

[Mario Carneiro]

it's similar to the distinction between computable functions meaning things without noncomputable marker in lean, vs computable meaning having a proof of computable f using the computability library

[Kevin Buzzard]

In particular Yourong, as a classical mathematician you have no interest in the statements that Mario and Eric are making about "topology" -- all they are doing is confusing the issue.

[Mario Carneiro]

If you want the one point compactification, just define it using filter.cocompact and pretend you never saw roption :)

[Mario Carneiro]

I agree we should have type synonyms for this

[Mario Carneiro]

I think there is a reasonable argument for giving option A itself the disjoint sum topology (rather than a type synonym), since I think sum A B also has a topology

[Kevin Buzzard]

Right, so def one_point_compactification (X : Type*) [topological_space X] := option X should be fine, and then put a topology on it.

[Yourong Zang]

Kevin Buzzard said:

Right, so def one_point_compactification (X : Type*) [topological_space X] := option X should be fine, and then put a topology on it.

Great! Thank you for the comments.