Skip to content

feat(Topology/Order): topological basis of scott topology on Complete…#31662

Open
edwin1729 wants to merge 8 commits intoleanprover-community:masterfrom
edwin1729:scott-topology
Open

feat(Topology/Order): topological basis of scott topology on Complete…#31662
edwin1729 wants to merge 8 commits intoleanprover-community:masterfrom
edwin1729:scott-topology

Conversation

@edwin1729
Copy link
Copy Markdown
Contributor

@edwin1729 edwin1729 commented Nov 15, 2025 •
edited
Loading

…PartialOrder

Zulip discussion for this PR.
(1/2) PRs in domain theory, proving that scott topologies over Algebraic DCPOs (CompletePartialOrder) are sober.
The main reference is Renata, Duality in Domain Theory. But the statements can also be found in the canonical text Abramsky and Jung
This first PR proves two prerequisites, namely:

The next PR is here: #31670

Open in Gitpod

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters labels Nov 15, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 15, 2025 •
edited
Loading

PR summary d4d96de5f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.Order.ScottTopologyDCPO (new file) 727

Declarations diff

+ AlgebraicDCPO
+ CompactElement
+ CompactElement.toOpen
+ IsCompactElement.toOpen
+ exists_basis_mem_basis
+ isCompactElement_iff_le_of_directed_sSup_le
+ isOpen_of_basis
+ isTopologicalBasis_Ici_image_compactSet
+ specialization_iff_ge

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@edwin1729 edwin1729 force-pushed the scott-topology branch 6 times, most recently from 6a5f829 to b9b6f96 Compare November 15, 2025 18:32
@edwin1729 edwin1729 mentioned this pull request Nov 15, 2025
Open
1 task
@edwin1729 edwin1729 marked this pull request as ready for review November 15, 2025 19:07
plp127
plp127 requested changes Nov 18, 2025
View reviewed changes
@edwin1729 edwin1729 requested a review from plp127 November 18, 2025 17:11
plp127
plp127 requested changes Nov 18, 2025
View reviewed changes
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Nov 20, 2025

@plp127 I wonder if you know something about this
I'm having some trouble building my fork since I rebased my branch yesterday. Wonder if it might have anything to do with the introduction of this new toolchain leanprover/lean4:v4.26.0-rc1. I rebased again today hoping the problem would just go away but it didn't. Am I forgetting some step? I show here how I

  1. update Mathlib.Lean
  2. Attempt to build all of Mathlib which fails
  3. But building just my file still succeeds
edwin@fury ~/c/mathlib4 (scott-topology) [1]> ~/.elan/bin/lake exe mk_all
No update necessary

edwin@fury ~/c/mathlib4 (scott-topology)> ~/.elan/bin/lake build
⡿ [5260/6849] Running Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (+ 22 ⣷ [6811/7547] Running Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (+ 22 ⣷ [7295/7579] Running Mathlib.Probability.Kernel.Composition.IntegralCompProd (+ 23 more⣯ [7327/7579] Running Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable✖ [7578/7579] Building Mathlib
trace: .> LEAN_PATH=/home/edwin/code/mathlib4/.lake/packages/Cli/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/batteries/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/Qq/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/aesop/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/importGraph/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/packages/plausible/.lake/build/lib/lean:/home/edwin/code/mathlib4/.lake/build/lib/lean /home/edwin/.elan/toolchains/leanprover--lean4---v4.26.0-rc1/bin/lean /home/edwin/code/mathlib4/Mathlib.lean -o /home/edwin/code/mathlib4/.lake/build/lib/lean/Mathlib.olean -i /home/edwin/code/mathlib4/.lake/build/lib/lean/Mathlib.ilean -c /home/edwin/code/mathlib4/.lake/build/ir/Mathlib.c --setup /home/edwin/code/mathlib4/.lake/build/ir/Mathlib.setup.json --json
error: Mathlib.lean:1:0: cannot import non`-module` Mathlib.Topology.Order.ScottTopologyDCPO from `module`
error: Lean exited with code 1
Some required targets logged failures:
- Mathlib
error: build failed

edwin@fury ~/c/mathlib4 (scott-topology) [1]> ~/.elan/bin/lake build Mathlib.Topology.Order.ScottTopologyDCPO
Build completed successfully (893 jobs).
edwin@fury ~/c/mathlib4 (scott-topology)>

@plp127
Copy link
Copy Markdown
Contributor

plp127 commented Nov 20, 2025

@edwin1729 see Zulip

@edwin1729 edwin1729 force-pushed the scott-topology branch 2 times, most recently from a9e2a87 to e66a006 Compare November 23, 2025 19:06
@edwin1729 edwin1729 requested a review from plp127 November 23, 2025 20:40
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Nov 26, 2025

@plp127 I didn't realize CI was failing. This is ready for review again now.

@b-mehta b-mehta assigned b-mehta and unassigned PatrickMassot Nov 27, 2025
b-mehta
b-mehta reviewed Nov 27, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here are some preliminary comments; we discussed more in person.

@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 13, 2026

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 6, 2026
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Mar 6, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 6, 2026
@edwin1729 edwin1729 requested a review from b-mehta March 6, 2026 16:05
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Mar 6, 2026 •
edited
Loading

@Vierkantor as co-author of Topology.Order.Category.FrameAdjunction, I thought this and (especially the next #31670) might be interesting to you. This PR does some initial setup while the next proves the main result, of showing Scott Topologies are Sober given conditions. It establishes the condition for equivalence of the above adjunction on one side

b-mehta
b-mehta reviewed Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've left a few comments.
In general, public definitions in mathlib are somewhat expensive, so ensure that you only make definitions you actually need.
Also, I think lots of the docstrings could be improved for mathlib.

@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 6, 2026
@edwin1729
Copy link
Copy Markdown
Contributor Author

edwin1729 commented Mar 7, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 7, 2026
@edwin1729 edwin1729 requested a review from b-mehta March 7, 2026 13:37
b-mehta
b-mehta reviewed Mar 8, 2026
View reviewed changes
edwin1729
edwin1729 commented Mar 8, 2026
View reviewed changes
@edwin1729 edwin1729 requested a review from b-mehta March 10, 2026 23:01
@edwin1729 edwin1729 force-pushed the scott-topology branch 2 times, most recently from 405fa10 to 95a8b18 Compare March 28, 2026 13:54
@mathlib-triage mathlib-triage bot assigned urkud and unassigned b-mehta Mar 29, 2026
@edwin1729 edwin1729 mentioned this pull request Mar 31, 2026
Open
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@plp127 plp127 Awaiting requested review from plp127

@b-mehta b-mehta Awaiting requested review from b-mehta

Assignees

@urkud urkud

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@edwin1729 @mathlib4-merge-conflict-bot @plp127 @mathlib4-dependent-issues-bot @b-mehta @urkud @jcommelin @PatrickMassot