[Merged by Bors] - feat(topology/order/lower_topology): Introduce the lower topology on a preorder by mans0954 · Pull Request #17426 · leanprover-community/mathlib3

mans0954 · 2022-11-08T05:10:42Z

This PR introduces the lower topology on a preorder. It is shown that the lower topology on a partial order is T₀ and the non-empty complements of the upper closures of finite subsets form a basis.

It is also shown that the lower topology on the product of two order_bot spaces coincides with the product topology of the lower topologies on the component spaces. This is used to show that the inf map (a,b) → a ⊓ b on a complete lattice is continuous.

The motivation for introducing the lower topology to mathlib is that, along with the Scott Topology (topology.omega_complete_partial_order) it is used to define the Lawson topology (Gierz et al, Chapter III).

depends on: [Merged by Bors] - feat(order/upper_lower): More prod lemmas #17747

YaelDillies · 2023-01-16T09:49:08Z

Since it's been a while,

maintainer merge

github-actions · 2023-01-16T09:49:21Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

sgouezel · 2023-01-16T16:56:03Z

I have two pending comments above (from a few weeks ago). I'd be happy to see them dealt with before the PR is merged.

mans0954 · 2023-01-16T18:53:43Z

I have two pending comments above (from a few weeks ago). I'd be happy to see them dealt with before the PR is merged.

@sgouezel - I think I've expanded everything, but I don't seem to be able to see any comments from you on this PR. Please could you post a direct link to them? Sorry.

All I could find open was this comment #17426 (comment) from @YaelDillies - I'd done this some time ago, but forgot to resolve the thread. I've done that now.

YaelDillies · 2023-01-16T19:02:42Z

Sébastien, I can't find your comments anymore. I think they have been lost to some force-push.

mans0954 · 2023-01-16T21:25:09Z

Sébastien, I can't find your comments anymore. I think they have been lost to some force-push.

I've checked my inbox - if @sgouezel had commented on the PR then I should have received an e-mail notification from GitHub.

sgouezel

Something must have gone wrong somewhere (probably on my side). Here they are again.

sgouezel · 2022-12-29T10:37:19Z

src/topology/order/lower_topology.lean

+This file introduces the lower topology on a preorder. It is shown that the lower topology on a
+partial order is T₀ and the complements of the upper closures of finite subsets form a basis.


Can you explain here what the lower topology here. Ideally, the docstring should be readable by someone who doesn't know the maths. You should also sketch the API here, by explaining that you define a type synonym and giving the main theorems.

@sgouezel is this the sort of thing you had in mind? It's hard to say too much about motivation without straying into concepts which aren't yet in mathlib (as far as I know).

src/topology/order/lower_topology.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/topology/order/lower_topology.lean

sgouezel · 2023-01-21T10:44:15Z

bors r+
Thanks!

…a preorder (#17426) This PR introduces the lower topology on a preorder. It is shown that the lower topology on a partial order is T₀ and the non-empty complements of the upper closures of finite subsets form a basis. It is also shown that the lower topology on the product of two `order_bot` spaces coincides with the product topology of the lower topologies on the component spaces. This is used to show that the inf map `(a,b) → a ⊓ b` on a complete lattice is continuous. The motivation for introducing the lower topology to mathlib is that, along with the Scott Topology (`topology.omega_complete_partial_order`) it is used to define the Lawson topology (Gierz et al, Chapter III).

bors · 2023-01-21T12:48:02Z

Pull request successfully merged into master.

Build succeeded:

… Mathlib (#11710) Introduces the Lawson Topology on a preorder. The Lawson Topology is defined as the meet of the [Lower Topology](leanprover-community/mathlib3#17426) and the [Scott Topology](#2508) previously introduced. A basis for the Lawson Topology is defined and some basic results are established: - An upper set is Lawson open if and only if it is Scott open - A lower set is Lawson closed if and only if it is closed under sups of directed sets - The Lawson topology on a partial order is T₀ Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

mans0954 added 30 commits September 4, 2022 21:18

Define lower topology, state lemma, fail to prove it

5107d59

Progress

582760d

Prove first lemma!

755754b

WIP

d0c3477

ici is closed

731dd5e

One implication

da4bacc

Prove singleton closure

0121f8e

Prime definition

add0b86

Show the lower topology is t0

9085e7d

remove prime for now

6ec9ba9

Shorten proof

bd5e2be

Add a couple of lemmas

f8ee3fe

Open lemma

2ba2c04

Lower topology coincides with product topology (one direction)

3b92ec5

Union of subbasis sets

7d32c1e

Lint

8eb9a77

Add l2 variants

b6278b7

upper_closure formulae

62924ae

upper closure of finite set is lower closed

388b1c0

Finally a formula for intersection of f

00a3746

Make it build with sorry

5fe2de7

Progress

cda4ff9

Show one finite proof

6af093f

Another finite proof

8cd97d6

Complete proof of basis

e2b0a3f

WIP

2c2b3bb

Merge branch 'master' into lower-topology

a81af45

Introduce Lower Topology

fac9a0f

Merge branch 'lower-topology2' into lower-topology

c42a153

Rehabilitate sUnion_Ici_compl

8b93063

Merge branch 'master' into lower-topology

c7c206a

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 16, 2023

sgouezel reviewed Jan 17, 2023

View reviewed changes

mans0954 and others added 2 commits January 17, 2023 07:17

Update src/topology/order/lower_topology.lean

b9ca077

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Improve docs

95605dc

YaelDillies 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 Jan 19, 2023

YaelDillies requested a review from sgouezel January 19, 2023 22:29

alreadydone reviewed Jan 20, 2023

View reviewed changes

src/topology/order/lower_topology.lean Outdated Show resolved Hide resolved

mans0954 added 2 commits January 20, 2023 08:10

namespaces

8287e67

Merge branch 'master' into lower-topology

2db427d

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 Jan 21, 2023

bors bot changed the title ~~feat(topology/order/lower_topology): Introduce the lower topology on a preorder~~ [Merged by Bors] - feat(topology/order/lower_topology): Introduce the lower topology on a preorder Jan 21, 2023

bors bot closed this Jan 21, 2023

bors bot deleted the lower-topology branch January 21, 2023 12:48

mans0954 mentioned this pull request Apr 3, 2024

[Merged by Bors] - feat(Topology/Order/LawsonTopology): Introduce the Lawson Topology to Mathlib leanprover-community/mathlib4#11710

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/order/lower_topology): Introduce the lower topology on a preorder#17426

[Merged by Bors] - feat(topology/order/lower_topology): Introduce the lower topology on a preorder#17426
mans0954 wants to merge 185 commits intomasterfrom
lower-topology

mans0954 commented Nov 8, 2022 •

edited by YaelDillies

Loading

Uh oh!

YaelDillies commented Jan 16, 2023

Uh oh!

github-actions bot commented Jan 16, 2023

Uh oh!

sgouezel commented Jan 16, 2023

Uh oh!

mans0954 commented Jan 16, 2023 •

edited

Loading

Uh oh!

YaelDillies commented Jan 16, 2023

Uh oh!

mans0954 commented Jan 16, 2023

Uh oh!

sgouezel left a comment

Uh oh!

sgouezel Dec 29, 2022

Uh oh!

mans0954 Jan 17, 2023 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Jan 21, 2023

Uh oh!

bors bot commented Jan 21, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

		This file introduces the lower topology on a preorder. It is shown that the lower topology on a
		partial order is T₀ and the complements of the upper closures of finite subsets form a basis.

Conversation

mans0954 commented Nov 8, 2022 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Jan 16, 2023

Uh oh!

github-actions bot commented Jan 16, 2023

Uh oh!

sgouezel commented Jan 16, 2023

Uh oh!

mans0954 commented Jan 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Jan 16, 2023

Uh oh!

mans0954 commented Jan 16, 2023

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

sgouezel Dec 29, 2022

Choose a reason for hiding this comment

Uh oh!

mans0954 Jan 17, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Jan 21, 2023

Uh oh!

bors bot commented Jan 21, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mans0954 commented Nov 8, 2022 •

edited by YaelDillies

Loading

mans0954 commented Jan 16, 2023 •

edited

Loading

mans0954 Jan 17, 2023 •

edited

Loading