[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

PatrickMassot · 2020-04-10T15:14:49Z

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).

src/order/filter/bases.lean

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

PatrickMassot · 2020-04-10T17:02:45Z

Oh, I was too quick to accept review suggestions. Gabriel actually broke my code.

src/order/filter/bases.lean

Fix Gabriel's fix

src/order/filter/basic.lean

src/order/filter/bases.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

sgouezel

This is excellent. In particular, congratulations for the documentation! I just have minor comments, see above. I would be happy if @urkud could also have a look, as he has played more with bases than me.

src/topology/sequences.lean

src/order/filter/basic.lean

src/order/filter/bases.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel · 2020-04-13T08:06:01Z

There's a conflict that needs to be solved, which means I can't bors r+ now. You can accept once the conflict is solved.

sgouezel · 2020-04-13T08:07:29Z

In fact the conflict was stupid, so I merged directly with the web editor.

bors r+

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 ```lean 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 ```lean 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: ```lean 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: ```lean 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 ```lean 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).

bors · 2020-04-13T11:19:11Z

Build succeeded

Build mathlib

bors · 2020-04-13T11:19:13Z

Pull request successfully merged into master.

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 ```lean 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 ```lean 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: ```lean 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: ```lean 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 ```lean 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).

…ommunity#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 ```lean 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 ```lean 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: ```lean 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: ```lean 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 ```lean 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).

Refactor filters infi and bases

56cfb29

PatrickMassot requested review from urkud and sgouezel April 10, 2020 15:15

gebner reviewed Apr 10, 2020

View reviewed changes

src/order/filter/bases.lean Outdated Show resolved Hide resolved

src/order/filter/bases.lean Outdated Show resolved Hide resolved

src/order/filter/bases.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

78a1c2e

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

jcommelin changed the title ~~Refactor filters infi and bases~~ refactor(order/filter): refactor filters infi and bases Apr 10, 2020

PatrickMassot commented Apr 10, 2020

View reviewed changes

src/order/filter/bases.lean Outdated Show resolved Hide resolved

Update src/order/filter/bases.lean

2bf68ea

Fix Gabriel's fix

PatrickMassot force-pushed the filter-bases-pr branch from 41d77a6 to 2bf68ea Compare April 10, 2020 17:15

jcommelin reviewed Apr 10, 2020

View reviewed changes

src/order/filter/basic.lean Outdated Show resolved Hide resolved

src/order/filter/bases.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

7dd9ae4

Co-Authored-By: Johan Commelin <johan@commelin.net>

sgouezel reviewed Apr 11, 2020

View reviewed changes

PatrickMassot and others added 4 commits April 11, 2020 14:25

Apply suggestions from code review

ca26894

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Describe the example filter bases

70c71b8

Missing typo fix

49e1525

Remove uneeded prime

d7a8d9e

Merge branch 'master' into filter-bases-pr

6e63ae7

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 13, 2020

bors bot changed the title ~~refactor(order/filter): refactor filters infi and bases~~ [Merged by Bors] - refactor(order/filter): refactor filters infi and bases Apr 13, 2020

bors bot closed this Apr 13, 2020

bors bot deleted the filter-bases-pr branch April 13, 2020 11:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

PatrickMassot commented Apr 10, 2020 •

edited by jcommelin

PatrickMassot commented Apr 10, 2020

sgouezel left a comment

sgouezel commented Apr 13, 2020

sgouezel commented Apr 13, 2020

bors bot commented Apr 13, 2020

bors bot commented Apr 13, 2020

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

Conversation

PatrickMassot commented Apr 10, 2020 • edited by jcommelin

PatrickMassot commented Apr 10, 2020

sgouezel left a comment

Choose a reason for hiding this comment

sgouezel commented Apr 13, 2020

sgouezel commented Apr 13, 2020

bors bot commented Apr 13, 2020

Build succeeded

bors bot commented Apr 13, 2020

Pull request successfully merged into master.

PatrickMassot commented Apr 10, 2020 •

edited by jcommelin