Relative open sets

Stream: mathlib4

[Violeta Hernández]

Is a definition IsOpenIn s t = IsOpen (s ↓∩ t) desirable?

[Violeta Hernández]

Arguably, this is quite a common notion in topology, and so it makes sense to provide a specialized API for it.

[Violeta Hernández]

But on the other hand, most theorems about this new API are one-liners reducing to theorems about IsOpen, see #17854.

[Violeta Hernández]

@Floris van Doorn

[Johan Commelin]

In the areas of maths that I move around in, I don't think I encounter this notion very often. But I agree that it appears at least in courses on point set topology.

[Patrick Massot]

I think this would only lead to either frustration or huge duplication. What precisely are you trying to formalize and lead you to feel this is missing?

[Yaël Dillies]

The original motivation is #16710, where a bunch of topological predicates are introduced for the order topology of o where o : Ordinal

[Violeta Hernández]

Patrick Massot said:

I think this would only lead to either frustration or huge duplication. What precisely are you trying to formalize and lead you to feel this is missing?

Yeah, I think you're right.

[Violeta Hernández]

The topological API is just way too vast to try and build something in parallel to it

[Violeta Hernández]

Why does #16710 need relative closed sets to begin with? I don't remember what the motivation for not just working with closed sets of ordinals was

[Anatole Dedecker]

This is something I've had in mind for some time : we have a lot of "within" variants of things in Mathlib, should that apply to open sets ? I haven't fully made my opinion, but the fact that we haven't been in desperate need for it yet is good evidence that maybe it's not as crucial as one would expect at first.

[Floris van Doorn]

Patrick Massot said:

I think this would only lead to either frustration or huge duplication. What precisely are you trying to formalize and lead you to feel this is missing?

@Hannah Scholz has a formalization of the proposition "(C : Set X) is a CW-complex", and has to deal a lot with the statements "A is closed in C" or "A is closed in the n-skeleton of C". In this thread I explain some more about the definition of CW complex we use.

I completely forgot we can now write IsClosed (s ↓∩ t). Instead, she has often been writing statements of the form ∃ B, IsClosed B ∧ B ∩ C = A ∩ C, which are very cumbersome to work with. Therefore I was already planning to suggest defining IsOpenIn/IsClosedIn myself. The fact that this turns out to be useful in a completely different field (ordinal numbers) given an indication we need good API for it.

As I mentioned in a comment of #17854, it is possible that we can already achieve this with IsClosed (s ↓∩ t).

[Anatole Dedecker]

Just noting that, even before we had the shiny s ↓∩ t notation, the easier way to do this was to talk about the preimage under the inclusion. This has the huge advantage of working for "inclusions" which are not actually inclusions (e.g we can express that a subset of $\mathbb{C}$ is open in $\mathbb{R}$).

[Nir Paz]

Violeta Hernández said:

Why does #16710 need relative closed sets to begin with? I don't remember what the motivation for not just working with closed sets of ordinals was

Mainly that the set of ordinals can be unbounded below o, so to talk about being closed in Ordinal you would have to manually add it: IsClosed ((S ∩ Iio o) ∪ {o}) means S is closed below o.

[Violeta Hernández]

My question was more, what are the mathematics that motivate this?

[Violeta Hernández]

(I don't doubt they exist, I'm just curious)

[Nir Paz]

Violeta Hernández said:

My question was more, what are the mathematics that motivate this?

Oh, you mean only work with universal clubs? A lot of results would really be the same, just a little less convenient, for example the intersection of k many clubs that have k as an accumulation point would be a club that has k as an accumulation point.

But I don't see an easy way to talk about stationary sets below an ordinal for example, since a stationary set with an accumulation point k isn't "stationary below k". But regressive functions are ubiquitous in infinite combinatorics, so you'd be missing that.

I guess more generally: the definition of clubs happens to transfer nicely from universal to local (by intersecting at a limit point), but when dealing with properties that apply to any filter and don't have to do with the specifics of clubs, like stationary sets, you don't get much information about what happens at cardinals below univ.

[Floris van Doorn]

This conversation seem to have stalled. The two options are:
(1) define predicate IsOpenIn and API for it
(2) use IsOpen (s ↓∩ t) consistently instead (and maybe some scattered lemmas about it).

I think both options are fine. Let's do a quick poll, and decide to go with the majority in (say) 2 days, even if it is a slim majority.

[Floris van Doorn]

/poll What to do with relative open (and closed) sets
define predicate IsOpenIn s t and API for it
use IsOpen (t ↓∩ s)

[Patrick Massot]

Why don’t you include the option “keep using the inverse image under inclusion”?

[Violeta Hernández]

If we do define the predicate, what other topological notions have to be relativized?

[Violeta Hernández]

Is it just IsOpen and IsClosed?

[Floris van Doorn]

Patrick Massot said:

Why don’t you include the option “keep using the inverse image under inclusion”?

Polls always allow you to add options, please add that option if you think that is the best solution.

[Floris van Doorn]

However, _ ↓∩ _ is just notation for that, so it will be syntactically the same, and is a lot shorter to write (but perhaps more confusing when you're new to it).

[Violeta Hernández]

yeah, I find it a bit silly to write down the preimage explicitly when we have notation that does exactly that