Commit 2020-04-13 08:52 17b2d065

refactor(order/filter): refactor filters infi and bases (#2384) This PR expands what Yury wrote about filter bases, and takes the opportunity to bring long overdue clarification to our treatment of infimums of filters (and also improve documentation and ordering in filter.basic). I'm sorry it mixes reorganization and some new content, but this was hard to avoid (I do keep what motivated all this for a later PR). The fundamental problem is that the infimum construction remained mysterious in filter.basic. All lemmas about it assume a directed family of filters. Yet there are many uses of infimums without this condition, notatably things like ⨅ i, principal (s i) without condition on the indexed family of sets s. Related to this, filter.generate stayed mysterious. It was used only as a technical device to lift the complete lattice structure from set (set a). However it has a perfectly valid mathematical existence, as explained by the lemma

lemma sets_iff_generate {s : set (set α)} {f : filter α} : f ≤ filter.generate s ↔ s ⊆ f.sets

which justifies the docstring of generate: generate g is the smallest filter containing the sets g. As an example of the mess this created, consider: https://github.com/leanprover-community/mathlib/blob/e758263/src/topology/bases.lean#L25

def has_countable_basis (f : filter α) : Prop :=
∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t

As it stands, this definition is not clearly related to asking for the existence of a countable s such that f = generate s. Here the main mathematical content this PR adds in this direction:

lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔
∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U
lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s
i).sets) 
lemma mem_infi_iff {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔
  ∃ I : set ι, finite I ∧ ∃ V : {i | i ∈ I} → set α, (∀ i, V i ∈ s i) ∧
  (⋂ i, V i) ⊆ U

All the other changes in filter.basic are either:

• moving out stuff that should have been in other files (such as the lemmas that used to be at the very top of this file)
• reordering lemmas so that we can have section headers and things are easier to find,
• adding to the module docstring. This module docstring contains more mathematical explanation than our usual ones. I feel this is needed because many people think filters are exotic (whereas I'm more and more convinced we should teach filters). The reordering stuff makes it clear we could split this file into a linear chain of files, like we did with topology, but this is open for discussion. Next I added a lot to filter.bases. Here the issue is filter bases are used in two different ways. If you already have a filter, but you want to point out it suffices to use certain sets in it. Here you want to use Yury's has_basis. Or you can start with a (small) family of sets having nice properties, and build a filter out of it. Currently we don't have this in mathlib, but this is crucial for incoming PRs from the perfectoid project. For instance, in order to define the I-adic topology, you start with powers of I, make a filter and then make a topology. This also reduces the gap with Bourbaki which uses filter bases everywhere. I turned has_basis into a single field structure. It makes it very slightly less convenient to prove (you need an extra pair of angle brackets) but much easier to extend when you want to record more properties of the basis, like being countable or decreasing. Also I proved the fundamental property that f.has_basis p s implies that s (filtered by p) actually is a filter basis. This is of course easy but crucial to connect with real world maths. At the end of this file, I moved the countable filter basis stuff that is currently in topology.bases (aiming for first countable topologies) except that I used the foundational work on filter.basic to clearly prove all different formulations. In particular:

lemma generate_eq_generate_inter (s : set (set α)) : generate s = generate (sInter '' { t | finite t ∧ t ⊆ s})

clarifies things because the right-hand colleciton is countable if s is, and has the nice directedness condition. I also took the opportunity to simplify a proof in topology.sequences, showcasing the power of the newly introduced

lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l :
filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s)
{φ : ι → α} (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l

(I will add more to that sequences file in the next PR).