Nowhere dense and meagre sets

Stream: Is there code for X?

[Michael Rothgang]

These are necessary to formalize Sard's theorem: the conceptual statement of Sard's theorem is that the set of critical values is meagre --- its complement is comeagre (residual in mathlib), it contains the intersection of countably many open dense sets. This is also the correct generalisation to Banach manifolds.

While residual sets are nicer than meagre ones (e.g., the former form a filter), writing the proof only in terms of residual sets would be awkward: decomposing the critical set into disjoint subsets naturally yields a union of subsets.

Would a PR adding nowhere dense and meagre sets to mathlib be welcomed? (I'd prove their API using the analogous results for open dense resp. residual sets.)

[Yaël Dillies]

@Yury G. Kudryashov, haven't you defined meagre sets already?

[Pedro Sánchez Terraf]

Also @Felix Weilacher was into this

[Felix Weilacher]

I have a very old lean3 write up of some basics of Baire category ending in a proof of Kuratowski Ulam here. (There are a few trivial sorry's) I took a break from working on this b/c of the port but I did plan to fix it up and PR it to mathlib4 soon.

Does mathlib have a function which takes in a Filter f on a Boolean algebra and outputs the Order.Ideal consisting of all complements of elements of f? Defining this first, let's call it dual f, and then defining meager X := dual (residual X) would probably be the way to go.

For whatever reason, the API for Filters is a lot more developed than the API for Ideals. For example there is not even a notion of a sigma-Ideal (see CountableInterFilter) which is the Type you'd want meager X to have. There is also a lot of nice infrastructure for working what I would call mod an ideal that uses the dual filter. E.g. docs#Filter.Eventually and docs#Filter.EventuallyEq. I have always wondered whether this was intentional and analogous to e.g. the convention that we should prefer lt to gt. Anyways with all this, it might be better to try and stick with using residual over meager as much as possible.

[Johan Commelin]

Felix Weilacher said:

I have a very old lean3 write up of some basics of Baire category ending in a proof of Kuratowski Ulam here. (There are a few trivial sorry's) I took a break from working on this b/c of the port but I did plan to fix it up and PR it to mathlib4 soon.

Cool!

[Felix Weilacher]

Thanks!

[Felix Weilacher]

All that being said, I think nowhere denseness itself would be a very nice addition

[Michael Rothgang]

So I'll prepare a short PR adding just the elementary API for this - and you can refactor this later to your liking?

[Felix Weilacher]

That sounds ideal! (no pun intended)

[Yaël Dillies]

Felix, I've been revamping the Ideal API, but it's complicated by the fact that docs#Order.PFilter also exists and is not used to define Filter.

[Yaël Dillies]

I'm currently adding the "apply compl everywhere" to docs#UpperSet, which is a prerequisite to what you want.

[Felix Weilacher]

Oh I didn't even realize Filter wasn't a special case of the order theoretic version in mathlib.

[Yaël Dillies]

Yeah... it's an annoying historical accident

[Yury G. Kudryashov]

@Yaël Dillies We have docs#residual

[Michael Rothgang]

PR at #7180

[Antoine Chambert-Loir]

Yaël Dillies said:

Yeah... it's an annoying historical accident

Why should you keep the two terminologies in Mathlib? This will force you to maintain by hand two parallel architectures of lemmas, which will quickly by unfeasible.

[Ruben Van de Velde]

Presumably because unifying is also work

[Yaël Dillies]

Especially given how widespread the use of Filter is.

[Anatole Dedecker]

Yes, I think there's a bit more to it than just an "historical accident". The real reason we haven't fixed that yet is that filters of sets are everywhere in topology in Mathlib. So when the general definition was added (file#Mathlib/Order/PFilter says in 2020, 3 years after file#Mathlib/Order/Filter/Basic), there was already a lot of APIs about this special case, and no one was sufficiently interested in the general case to really develop its API (I don't even think there was a consensus that unifying was the right thing to do). I'm now convinced that we should do it at some point because a few people have already complained for the lack of API in the general case, but I'm not even sure how much actually generalizes. For sure the lattice structure does, but what about docs#FIlter.map and docs#Filter.comap ?

[Yaël Dillies]

I don't know about Filter.map, but Filter.comap generalises verbatim.

[Anatole Dedecker]

The story is a bit similar for set and order ideals : the need for them and the definition came later than the super-crucial filters on sets, and in the meantime we realized that in a lot of cases where you'd think we need them, we can just use filters instead. A great example of that is docs#MeasureTheory.Measure.ae, which works so well that I'm now convinced that working with this filter is more natural than working with the ideal of null-sets. I don't know what kind of arguments are usually done with meagre sets, but if a lot of them are reasoning "modulo meagre sets" then almost-surely working with docs#residual will be more convenient. A not-so-great example in my opinion is docs#Bornology, which really should be defined in terms of ideal rather than the current trick to go back to filters.

[Patrick Massot]

We have always said that a refactor that has no impact at all on the use of filters in topology and analysis would be welcome. But I fear this isn't so easy.

[Anatole Dedecker]

Yaël Dillies said:

I don't know about Filter.map, but Filter.comap generalises verbatim.

Oh in my mind docs#Filter.map would have been the easiest one to generalize (except it now goes in the opposite direction): if you have $\phi : B\to A$ a morphism of lattices (you probably need way less but whatever) then you can define a map $\mathrm{Filter}(A)\to\mathrm{Filter}(B)$ by taking the preimage by $\phi$. docs#Filter.map is the special case where $\phi$ is the inverse image under a function.

Anyways, this shows that I haven't thought a lot about it, so maybe forget that last sentence about generalizations.

[Anatole Dedecker]

Another thing to note is that a bunch of people here have developped a very good intuition of how filter works and what they represent, and to me at least it's not obvious at all that any of this applies to the general case. This is still not an argument against unification of course, just a justification for why we haven't done it already.

[Yaël Dillies]

Patrick Massot said:

We have always said that a refactor that has no impact at all on the use of filters in topology and analysis would be welcome. But I fear this isn't so easy.

I thought so too but, come to think of it, filters are a place where defeq is rarely used, so there's potential for deep rewrites to actually be quite innocuous.

[Anatole Dedecker]

I agree with Yael, I was scared of it but in the end I don't think it will break that many things. The thing I'm still wondering about is what the naming should be

[Antoine Chambert-Loir]

I believe docs#Filter has to stay.
Since it duplicates docs#Order.Ideal, my (possibly too radical) suggestion would be to simply remove docs#Order.PFilter. If Mathlib really needs something duplicate because the order is reversed, I'd suggest to introduce something such as Order.Coideal and to have the lemmas written automatically when needed.

[Anatole Dedecker]

Note that we already have a bunch of definitions that are order duals of each other (docs#Monotone vs docs#Antitone for example). we don't have @[to_additive]-style automation for dualising for reasons (*), but we already do a lot of proof by dualizing, so nothing unusual here.

(*) IIRC the reason is that what you want to do is less obvious: do you want to reverse all order relations at once, or do you want to state the 2^n variations where n is the number of ordered sets appearing in your lemmas?

[Anatole Dedecker]

Also, people definitely want filters on general lattices in order to do point-free topology (ping @Sam van G), so I don't think we should get rid of it.

[Anatole Dedecker]

I agree that we do not want to replace all Filter X by Filter (Set X). One possibility is to have Set.Filter and Order.Filter. I don't think that would cause too many clashes because we don't usually open Order in topology files, but maybe that would increase the risk of confusion.

[Yaël Dillies]

What we should do is make Filter X an abbreviation of PFilter (Set X), slowly move Filter API to PFilter, then dualise everything that we want to Order.Ideal.

[Anatole Dedecker]

I agree with the strategy, but I claim that we should change the name of PFilter.

[Yaël Dillies]

To what? Order.Filter?

[Anatole Dedecker]

For example

[Anatole Dedecker]

We also have to think about what happens to lemmas that are generalized to PFilter: do we keep the Filter version as a special case, or do we expect people using Filter to go search for lemmas about PFilter?

[Yaël Dillies]

So you want to change the name from Order.PFilter to Order.Filter? (just making sure you know it's already in the Order namespace) Do you want it to be protected so that it doesn't conflict with Filter?

[Anatole Dedecker]

I don’t think protecting it is needed, since no one opens Order

[Anatole Dedecker]

But I think one thing we could do is change the current Filter to Set.Filter so that it’s easier to disambiguate if needed

[Anatole Dedecker]

Ah but that could mess up linking in docs

[Yaël Dillies]

or Topology.Filter. In general, a bunch of topological material deserves to be put under a namespace, eg docs#LocallyFinite.

[Pedro Sánchez Terraf]

I believe that leaving Filter as such and something else for order filters (either protecting or some other name) is the way to go. In any case, the P in PFilter is somewhat misleading. An O would be more appropriate.