Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: real manifolds are locally path-connected #7877

Open
wants to merge 26 commits into
base: master
Choose a base branch
from
Open

feat: real manifolds are locally path-connected #7877

wants to merge 26 commits into from
+188 −15

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Oct 23, 2023 •
edited
Loading

The proper way to prove this is showing that a charted space is locally path-connected iff its model space is.
(For connectedness, this is in mathlib.)

Note that #7822 and this PR used to have almost the same proof; I wonder if this can be refactored. (Both proofs basically argue that

  • given the hypotheses, my local models satisfy topological property P (local compactness resp. local path-connectedness)
  • property P is invariant under continuous maps
  • charts are local homeomorphisms.
    I don't know if mathlib has such meta-reasoning currently.)

grunweg and others added 16 commits October 21, 2023 08:59
@grunweg
Preliminary lemmas, part 1.
206658e 
Proving image_congr' is a bit unwieldy as image_id as not be proven yet.
@grunweg
Fix double namespace; more helper lemmas.
f0097d8
@grunweg
Add final result, over any locally compact field.
f02fbee
@grunweg
Fix linter errors.
57cfe33
@grunweg
chore: remove extreneous Set. qualifiers.
7fa60a1 
It's proposed that a code formatter remove those automatically,
so we might as well remove them as we see them.
@digama0
chore: bump lean toolchain
eb102af
@grunweg
Move material to a new file.
676c420
@grunweg
Expand docstring slightly.
e2ff7d8
@grunweg
Show sigma-compactness.
df48927
@grunweg
WIP, mostly just the scaffolding
bbd1042
@grunweg
Outline implication path-connected => connected.
7fe98f0 
Have one sizable gap in mathlib: is missing definitions of and API around
locally (path-)connected sets. The remaining scaffolding is done.
@grunweg
Show real mathfolds are locally path-connected:
89126ef 
except for another missing lemma from mathlib.
@grunweg
IsPathConnected.image is already in mathlib.
d691cb5
@grunweg
Further tweaks.
501f639
@grunweg
Remove local connectivity.
b29c544
@grunweg
Last tweak.
b998d8a
@grunweg grunweg added blocked-by-other-PR This PR depends on another PR to Mathlib awaiting-review The author would like community review of the PR t-differential-geometry Manifolds etc t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 23, 2023
@grunweg grunweg mentioned this pull request Oct 23, 2023
Open
@grunweg grunweg 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 Oct 31, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Nov 3, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Nov 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. t-differential-geometry Manifolds etc 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.

None yet
3 participants
@grunweg @leanprover-community-mathlib4-bot @digama0