Refactoring algebraic filter bases

Stream: mathlib4

[Anatole Dedecker]

Motivated by #14990, I thought it was probably time to update our good old "algebraic filter bases" API to modern mathlib practices. #18202 (still marked as draft just because it's too big, otherwise I'm happy with it) is an attempt at doing this. Broadly speaking, here's what it does:

1. In a huge majority of cases, Mathlib uses filter bases by the means of the docs#Filter.HasBasis API. Of course this is only suitable when we already "have" the generated filter. When we want to build that filter, we have both docs#FilterBasis and docs#Filter.IsBasis. My point is the latter is much cleaner to use because the translation to HasBasis is seamless (the data is the same, a predicate and an indexed family). So, I changed docs#GroupFilterBasis, docs#RingFilterBasis, ... to predicates docs#Filter.IsGroupBasis, docs#Filter.IsRingBasis, ... using the IsBasis model. For a detailed explanation, read the docstring of https://github.com/leanprover-community/mathlib4/blob/AD_algebra_filter_bases/Mathlib/Topology/Algebra/FilterBasis.lean
2. Now, on top of the general setup, we have extra constructions for bases made of algebraic subobjects, such as docs#RingSubgroupsBasis, docs#RingSubmodulesBasis, ... Apart from the naming which sounds really weird to me, my main concerns about these were (i) these use indexed family but no predicate, so they are inconsistent with everything (ii) this sounds like extra definitions for not much gain. So I changed them to new constructors for the general definitions (adding a bit of SetLike magic to remove some duplication), and I believe everything is now much cleaner. See https://github.com/leanprover-community/mathlib4/blob/AD_algebra_filter_bases/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
3. Since I had to fix a lot of things depending on it, I ended up refactoring some of it slightly along the way. This is what causes the PR to be so big, and of course I want some more eyes to look at what I did in this step.

[Anatole Dedecker]

Now, correct me if I'm wrong, but I don't think anyone will be okay with merging a PR of that size. My plan then is to first add the new versions while keeping the old ones, then refactoring the use places in a few separate PRs, and finally removing the current setup. Does it sound good?

[Anatole Dedecker]

Ping @Patrick Massot @Yury G. Kudryashov @Antoine Chambert-Loir @María Inés de Frutos Fernández @Moritz Doll

[Yaël Dillies]

This looks like a very good idea! I myself tried using the filter bases API a few months ago and basically failed due to all those mismatches between predicates and non-predicates. I ended up stating my result very concretely without using the filter basis machinery.

[Yaël Dillies]

"my result" being docs#exists_mem_interior_convexHull_affineBasis

[Anatole Dedecker]

I'm not sure I understand correctly what you mean by this. If you mean "this should be stated in terms of filter basis" then yes, but the existing docs#Filter.HasBasis works as a charm for that.
The other option is that you were talking about the following alternate proof : start by proving that simplicial neighborhoods form a basis for a T2 vector space topology, and then use something like docs#Basis.equivFunL to get that the topology is the original one ? If so that is quite smart, but I'm not sure how easy that would be in practice.
Am I missing something obvious ?

[Patrick Massot]

I think globally this is a good idea. The old API comes straight from the perfectoid spaces project in 2018 and we learned a lot since then.

[Patrick Massot]

In a context where we try to disentangle the import hierarchy, maybe we should be careful with files doing stuff for all algebraic structures. But this may be a virtual concern in the sense that everything will be already imported anyway.

[Anatole Dedecker]

#18437 adds the new core API without touching any existing files.

[Yury G. Kudryashov]

I have another question about this design. Why do we define predicates on filter bases, not on filters?

[Yury G. Kudryashov]

E.g., we can have

structure GroupFilter (G : Type*) [Group G] extends Filter G where
  pure_le : pure 1 ≤ toFilter
  tendsto_inv : Tendsto Inv.inv toFilter toFilter
  tendsto_mul : Tendsto (· * ·) (l ×ˢ l) l

Then GroupFilters form a CompleteLattice which is equivalent to the lattice of GroupTopologys.

[Yury G. Kudryashov]

Then any basis will be a GroupFilterBasis.

[Kevin Buzzard]

I can't speak for Patrick but I am a consumer of these funny things and in my experience you only really want them as technical intermediate tools along the way to prove that eg a ring with a topology is a topological ring. For example our proof that the finite adeles are a topological ring uses this kind of machinery.

See for example https://github.com/leanprover-community/mathlib4/blob/318cb7184d6e13f32a69869057dab5bcfe652f0d/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean#L398-L399

[Anatole Dedecker]

Hmmmm, so Yury is indeed raising an interesting point. First, let me mention that most of the interesting results do exist in a version that does not mention filter bases, but they don't have fancy bundling (e.g docs#TopologicalGroup.of_nhds_one). But indeed:

1. We don't have the construction of the topology starting from a "group filter" (we do for filter bases)
2. It would make sense to just move bases later (e.g have a theorem characterizing group filters in terms of filter bases directly)

This doesn't make my life easier because it means more refactoring, but I guess that makes sense. I don't think we want to bundle it on top of filter though (I'd prefer a predicate on filters), precisely because I don't want these things to leak outside of the "I'm building up some topology and proving it's compatible with algebra" phase : we want most people to deal with usual docs#Filter and docs#Filter.HasBasis only.

[Anatole Dedecker]

So I guess I need to do that next (no guarantee about the time of completion), unless someone has some objection

[Anatole Dedecker]

/me is realizing the size of that second refactor...

[Anatole Dedecker]

One problem I have (apart from not wanting to spend my weekend on that) is that I won't be able to make the API uniform because of mathematical problems. For example, if I were to modify docs#TopologicalGroup.of_nhds_one to assume IsGroupFilter, it would be natural to do the same for docs#ContinuousInv.of_nhds_one. The problem is, the natural IsContinuousInvFilter definition would not be strong enough to ensure that there exists a topology with continuous inversion and that filter as neighborhoods of one.

[Anatole Dedecker]

So I really don't know what is the best approach anymore

[Antoine Chambert-Loir]

Thinking that maybe one step today is better than two steps in one month, let me ask two questions:
Would Anatole's suggested refactoring prevent a subsequent refactor along the lines indicated by Yuri? Would it be made obsolete?

[Yury G. Kudryashov]

Note: I don't use this part of the library. I've asked a question that looks reasonable to me, but I know nothing about applications (in particular, I can't understand mathematically what @Kevin Buzzard is talking about since I don't know what finite adeles are), so it's possible that in practice it's more convenient to work with filter bases.

[Kevin Buzzard]

I don't care about studying group-filters or group-filter-bases or anything like that. But I do care about things like "given a commutative ring R and an ideal J, put the topological ring structure on R where powers J^n of J are a basis of open neighbourhoods of zero" or "given a commutative ring R and a subring S which has a topology, extend this topology to R by translating S around and this makes R into a topological ring". I think that the only reason we have these funny group-filter-basis things in mathlib is as an auxiliary tool in order for us to make constructions like this easier. The difficulty with doing everything directly is that it's not difficult to write down a formula for the open sets, but then it's very tedious in general to prove that addition and multiplication are continuous if all you have is this formula. The trick with these auxiliary constructions is that they say things like "if you know what the topology looks like near the identity, and the open sets near the identity satisfy some typically easy-to-check axioms, then the topology you get by translating the picture near the identity around automatically makes multiplication/addition/negation/whatever continuous". But maybe it would also be easy with your approach.

[Kevin Buzzard]

Perhaps a more coherent answer is "in practice you tend to be given the basis, not the filter". For example you are given J^n for all n, not "the set of all subsets which happen to contain J^n for some n".

[Patrick Massot]

I agree with Kevin, I don’t see any example where you would give the filter directly here.

[Antoine Chambert-Loir]

in any case, it's probably simpler to define a filter as the one generated by some sets, and if you have been lucky enough to provide all of them, to state it as a theorem.

[Anatole Dedecker]

Okay, I took some time to think about this, and here are my conclusions.

First, I think Yury's suggestion definitely makes sense, and I'm absolutely convinced that one could make a perfectly usable API from it (wether you like filters or filter bases).

The thing that makes me want to stick with my approach (other than "I don't want to redo this refactor again") is that I'm worried about giving too much importance to what is really a technical trick. Arguably my proposal is not perfect in this aspect either (e.g maybe this lemma should just be stated next to docs#TopologicalGroup.of_nhds_one without bundling anything in a fancy structure). The reason I care about this is that all of these tricks become useless as soon as you just want to prove docs#ContinuousMul or docs#ContinuousSMul in isolation of any extra algebraic structures, and making these kind of generalizations painful (e.g because the APIs are completely distinct) would be very annoying. To take a concrete example, I think I would be against Yury's proposal to use the lattice isomorphism between group topologies and group filters, because this approach completely breaks down for monoid topologies.

So my point is that we should focus on making these things easy to use, rather than trying to make them more general.

If everyone is convinced by this argument, I'm going to move forward with my proposal.

[Kevin Buzzard]

Here's a test case which I'll need soon! If $A_i$ are a family of topological groups and $H_i$ are a family of open subgroups, then I want to make the restricted product of the $A_i$ over the $H_i$ to be a topological group, with a basis for the topology on the restricted product being $\prod_i U_i$ with $U_i\subseteq A_i$ open for all $i$ and $U_i=H_i$ for all but finitely many $i$.