[Merged by Bors] - feat(order/topology/filter): define topology on `filter X` #17219

urkud · 2022-10-28T01:46:26Z

depends on: [Merged by Bors] - feat(order/filter): add several trivial lemmas #17215

PatrickMassot

It would be nice to refactor stone_cech.lean to avoid code duplication with the new file, but this can be left to a future PR.
bors d+

src/topology/filter.lean

bors · 2022-10-28T12:36:37Z

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-dependent-issues-bot · 2022-10-28T14:48:08Z

This PR/issue depends on:

~~[Merged by Bors] - feat(order/filter): add several trivial lemmas #17215~~
By Dependent Issues (🤖). Happy coding!

Co-authored-by: Patrick Massot <patrickmassot@free.fr>

urkud · 2022-10-28T17:45:48Z

@PatrickMassot According to github, you've delegated this PR, then removed the delegated label. Was it intentional?

src/topology/filter.lean

alreadydone · 2022-10-29T19:08:23Z

src/topology/filter.lean

+
+This topology has the following important properties.
+
+* If `X` is a topological space, then the map `𝓝 : X → filter X` is a topology inducing map.


I wonder what relationship this topology has to Cauchy.uniform_space; we have Cauchy.dense_inducing_pure_cauchy but that's for the pure filter, not neighborhood filter.

I don't know. IMHO, we can look at this after merging this PR.

Sounds good!

Even though the relationship with Cauchy.uniform_space is still unclear, ultrafilter.topological_space is just the subspace topology inherited from the topology in this PR.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

alreadydone · 2022-10-29T22:35:55Z

src/topology/filter.lean

+
+This topology has the following important properties.
+
+* If `X` is a topological space, then the map `𝓝 : X → filter X` is a topology inducing map.


Sounds good!

alreadydone · 2022-10-29T22:46:36Z

src/topology/order.lean

+lemma is_open_generate_from_inter_closed {g : set (set α)} (hg : ∀ s t ∈ g, s ∩ t ∈ g)
+  (hU : (⋃₀ g) = univ) {s} :
+  @is_open _ (generate_from g) s ↔ ∃ S ⊆ g, s = ⋃₀ S :=


The assumption hU is topological_space.is_topological_basis.sUnion_eq and hg is stronger than exists_subset_inter, and the conclusion still holds if you replace hg by exists_subset_inter: we have topological_space.is_topological_basis.open_eq_sUnion. Maybe you could use that or we should do some refactor?

(BTW hg is also satisfied by basic opens in the prime spectrum of a commutative ring with the Zariski topology: we have prime_spectrum.basic_open_mul and prime_spectrum.is_topological_basis_basic_opens.)

I guess if you do letI := generate_from g then you can prove this lemma using topological_space.is_topological_basis.open_eq_sUnion easily. In your use case (is_open_iff) you don't even need letI. So I think you can just delete this lemma and use that in is_open_iff.

I added is_topological_basis.open_iff_eq_sUnion and deleted my lemma. Thanks!

Thanks! I have no more suggestions or objections, and you already got the delegation, so feel free to merge. But could you add the reference(s) you use, maybe in a future PR, because for example I'm curious to learn more about this topology but couldn't find anything relevant from a brief web search.

I didn't use any reference. My goal was to have a topology such that nhds is continuous and tendsto nhds at_top (nhds at_top). AFAIR, I asked on Zulip and someone suggested to generate the topology by {l | s ∈ l}.

PatrickMassot · 2022-10-30T21:11:34Z

@PatrickMassot According to github, you've delegated this PR, then removed the delegated label. Was it intentional?

No it wasn't. I guess there was a race condition between me and bors.

urkud · 2022-11-02T17:43:42Z

bors merge

bors · 2022-11-02T23:27:15Z

Pull request successfully merged into master.

Build succeeded:

urkud added 30 commits May 12, 2022 16:06

Snapshot

bea5916

Fix

9e727f0

Snapshot

3b23cd6

Update

bf10132

Merge branch 'master' into YK-filter-topology

ba07e98

Snapshot

596c860

Snapshot

59aa288

Merge branch 'YK-filter-lift-infi' into YK-filter-topology

0b0e5d0

Snapshot

4a5315c

Merge branch 'master' into YK-filter-topology

4a7da04

Merge branch 'master' into YK-filter-topology

3c63dd5

Snapshot

0b316a6

Snapshot

311a074

Merge branch 'master' into YK-filter-topology

614eae9

Snapshot

3bd583f

Missing file

6d47529

Revert parts that went to another PR

eb6ddf3

Revert parts that went to another PR

0edc962

Merge branch 'master' into YK-ultrafilter-atom

eeaf262

add is_atom_pure

5484494

Merge branch 'master' into YK-filter-pure

53a13b9

Merge branch 'YK-ultrafilter-atom' into YK-filter-pure

11ac14f

Update

b095070

Merge branch 'YK-filter-pure' into YK-filter-topology

748b46e

Snapshot

28b79d7

Fix

335768a

Merge branch 'YK-filter-pure' into YK-filter-topology

89e3f9c

Merge branch 'master' into YK-filter-pure

57d1d06

Revert

b30cbe4

Merge branch 'YK-filter-pure' into YK-filter-topology

dca31f8

mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 28, 2022

PatrickMassot reviewed Oct 28, 2022

View reviewed changes

src/topology/filter.lean Outdated Show resolved Hide resolved

src/topology/filter.lean Show resolved Hide resolved

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 28, 2022

PatrickMassot added awaiting-author A reviewer has asked the author a question or requested changes and removed delegated The PR author may merge after reviewing final suggestions. labels Oct 28, 2022

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 28, 2022

Update src/topology/filter.lean

80e377d

Co-authored-by: Patrick Massot <patrickmassot@free.fr>

urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 28, 2022

alreadydone reviewed Oct 29, 2022

View reviewed changes

Update src/topology/filter.lean

e02fd25

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

alreadydone reviewed Oct 29, 2022

View reviewed changes

urkud added 2 commits October 31, 2022 17:11

Merge branch 'master' into YK-filter-topology

01e23de

Snapshot

e6e0c1f

urkud added the delegated The PR author may merge after reviewing final suggestions. label Oct 31, 2022

+2 lemmas

ddf3cf5

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 2, 2022

bors bot pushed a commit that referenced this pull request Nov 2, 2022

feat(order/topology/filter): define topology on filter X (#17219)

78e50d8

bors bot changed the title ~~feat(order/topology/filter): define topology on filter X~~ [Merged by Bors] - feat(order/topology/filter): define topology on filter X Nov 2, 2022

bors bot closed this Nov 2, 2022

bors bot deleted the YK-filter-topology branch November 2, 2022 23:27

eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Nov 5, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(order/topology/filter): define topology on `filter X` #17219

[Merged by Bors] - feat(order/topology/filter): define topology on `filter X` #17219

urkud commented Oct 28, 2022 •

edited

PatrickMassot left a comment

bors bot commented Oct 28, 2022

mathlib-dependent-issues-bot commented Oct 28, 2022

urkud commented Oct 28, 2022

alreadydone Oct 29, 2022

urkud Oct 29, 2022

alreadydone Oct 29, 2022

alreadydone Nov 1, 2022

alreadydone Oct 29, 2022

alreadydone Oct 29, 2022 •

edited

alreadydone Oct 31, 2022

urkud Oct 31, 2022

alreadydone Nov 1, 2022

urkud Nov 1, 2022 •

edited

PatrickMassot commented Oct 30, 2022

urkud commented Nov 2, 2022

bors bot commented Nov 2, 2022


		This topology has the following important properties.

		* If `X` is a topological space, then the map `𝓝 : X → filter X` is a topology inducing map.

[Merged by Bors] - feat(order/topology/filter): define topology on filter X #17219

[Merged by Bors] - feat(order/topology/filter): define topology on filter X #17219

Conversation

urkud commented Oct 28, 2022 • edited

PatrickMassot left a comment

Choose a reason for hiding this comment

bors bot commented Oct 28, 2022

mathlib-dependent-issues-bot commented Oct 28, 2022

urkud commented Oct 28, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone Oct 29, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

urkud Nov 1, 2022 • edited

Choose a reason for hiding this comment

PatrickMassot commented Oct 30, 2022

urkud commented Nov 2, 2022

bors bot commented Nov 2, 2022

[Merged by Bors] - feat(order/topology/filter): define topology on `filter X` #17219

[Merged by Bors] - feat(order/topology/filter): define topology on `filter X` #17219

urkud commented Oct 28, 2022 •

edited

alreadydone Oct 29, 2022 •

edited

urkud Nov 1, 2022 •

edited