[Merged by Bors] - feat(topology/covering): Define covering spaces #16087

tb65536 · 2022-08-17T03:20:45Z

This PR adds a definition of covering spaces.

We don't want to have to specify a constant index set I, and we don't want to say "there exists an index set I : Type u such that f ⁻¹' U is homeomorphic to I × U" (annoying universe issues). Instead, we can use the preimage of any point as our index set.

Supersedes #15276, where @alreadydone suggested that I drop the surjectivity assumption.

depends on: [Merged by Bors] - feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber #16079
depends on: [Merged by Bors] - feat(topology/separation): embedding.discrete_topology #16092

mathlib-dependent-issues-bot · 2022-09-02T13:39:22Z

This PR/issue depends on:

~~[Merged by Bors] - feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber #16079~~
~~[Merged by Bors] - feat(topology/separation): embedding.discrete_topology #16092~~
By Dependent Issues (🤖). Happy coding!

merge

src/topology/covering.lean

ocfnash

Thanks!

Aside from a trivial comment about code style, my two thoughts are:

Since branched coverings are important, I'd be tempted to include a subset of the base as part of the data and do everything relative to that. In other words, we could define is_covering_map_on instead (and presumably as a convenience have is_covering_map, specializing this to set.univ) and hopefully thus avoid some subtype pain in future work.
I'd be tempted to include the monodromy group as part of the data. I don't see a way to use the definitions here to make the statement that "the map f : E → X admits a set of trivializations with monodromy group G". In other words, it looks to me like we'll have to refactor or duplicate code when this day comes.

What do you think?

Feel free to push back, I think we could go with this for now at least.

src/topology/covering.lean

tb65536 · 2022-10-21T17:20:37Z

Thanks!

Aside from a trivial comment about code style, my two thoughts are:

Since branched coverings are important, I'd be tempted to include a subset of the base as part of the data and do everything relative to that. In other words, we could define is_covering_map_on instead (and presumably as a convenience have is_covering_map, specializing this to set.univ) and hopefully thus avoid some subtype pain in future work.

I'd be tempted to include the monodromy group as part of the data. I don't see a way to use the definitions here to make the statement that "the map f : E → X admits a set of trivializations with monodromy group G". In other words, it looks to me like we'll have to refactor or duplicate code when this day comes.

What do you think?

Feel free to push back, I think we could go with this for now at least.

Thanks! I hadn't though about branched covers. I've added is_covering_map_on.

I'm not so sure about including the monodromy group as part of the data. It seems like it would make the definition more clunky (e.g., path connectedness) and would make it more painful to prove that a given map is a covering map. Wouldn't it make more sense to just have the monodromy data be constructed from is_covering_map?

ocfnash

Thanks!

On reflection I think it's probably best not to make the monodromy group explicit for now, especially as we do not have a theory of principal bundles.

One style suggestion, and one optional task but otherwise this LGTM. Thanks again.

bors d+

src/topology/covering.lean

ocfnash · 2022-10-21T18:21:55Z

src/topology/covering.lean

+lemma continuous (hf : is_covering_map f) : continuous f :=
+continuous_iff_continuous_at.mpr (λ x, (hf (f x)).continuous_at)
+
+lemma is_locally_homeomorph (hf : is_covering_map f) : is_locally_homeomorph f :=


Optionally: I think it would be nice to generalise this to is_covering_map_on (in the case when s is open).

I'll have to think about this. It's a tad bit tricker than it looks, since you don't know that f ⁻¹' s is open.

you don't know that f ⁻¹' s is open.

I don't understand: f is continuous and s is open so this is trivial, right?

Thinking about this a bit more, I suppose you'll also need that s is non-empty but otherwise this should be easy.

Oh, are you talking about is_locally_homeomorph? I was talking about continuous.

Is this along the lines of what you were thinking of? #17114

bors · 2022-10-21T18:23:33Z

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

tb65536 · 2022-10-21T20:30:53Z

bors r+

@alreadydone

This PR adds a definition of covering spaces. We don't want to have to specify a constant index set `I`, and we don't want to say "there exists an index set `I : Type u` such that `f ⁻¹' U` is homeomorphic to `I × U`" (annoying universe issues). Instead, we can use the preimage of any point as our index set. Supersedes #15276, where @alreadydone suggested that I drop the surjectivity assumption.

bors · 2022-10-21T21:24:47Z

Pull request successfully merged into master.

Build succeeded:

new file

d6c1598

tb65536 added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters and removed awaiting-review The author would like community review of the PR labels Aug 17, 2022

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 Aug 17, 2022

YaelDillies changed the title ~~feat(src/topology/covering): Define covering spaces~~ feat(topology/covering): Define covering spaces Aug 17, 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 Sep 2, 2022

tb65536 added 2 commits September 2, 2022 06:58

Merge branch 'master' into covering_spaces2

8f723cf

merge

merge

4ff2fba

tb65536 added the awaiting-review The author would like community review of the PR label Sep 2, 2022

tb65536 added 4 commits September 8, 2022 16:21

surjective

9e7d0e4

reorder

41cb068

revert surjective for now

24a0c94

year

bb77572

sgouezel reviewed Sep 30, 2022

View reviewed changes

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

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 Sep 30, 2022

module docstring review

745da4b

tb65536 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 Sep 30, 2022

ocfnash reviewed Oct 21, 2022

View reviewed changes

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

review

fe25806

ocfnash approved these changes Oct 21, 2022

View reviewed changes

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 21, 2022

tb65536 added 2 commits October 21, 2022 11:59

review

e280a80

review

14de02a

bors bot changed the title ~~feat(topology/covering): Define covering spaces~~ [Merged by Bors] - feat(topology/covering): Define covering spaces Oct 21, 2022

bors bot closed this Oct 21, 2022

bors bot deleted the covering_spaces2 branch October 21, 2022 21:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/covering): Define covering spaces #16087

[Merged by Bors] - feat(topology/covering): Define covering spaces #16087

tb65536 commented Aug 17, 2022 •

edited

Loading

mathlib-dependent-issues-bot commented Sep 2, 2022

ocfnash left a comment

tb65536 commented Oct 21, 2022 •

edited

Loading

ocfnash left a comment •

edited

Loading

ocfnash Oct 21, 2022

tb65536 Oct 21, 2022

ocfnash Oct 22, 2022

tb65536 Oct 22, 2022

tb65536 Oct 22, 2022

bors bot commented Oct 21, 2022

tb65536 commented Oct 21, 2022

bors bot commented Oct 21, 2022

[Merged by Bors] - feat(topology/covering): Define covering spaces #16087

[Merged by Bors] - feat(topology/covering): Define covering spaces #16087

Conversation

tb65536 commented Aug 17, 2022 • edited Loading

mathlib-dependent-issues-bot commented Sep 2, 2022

ocfnash left a comment

Choose a reason for hiding this comment

tb65536 commented Oct 21, 2022 • edited Loading

ocfnash left a comment • edited Loading

Choose a reason for hiding this comment

ocfnash Oct 21, 2022

Choose a reason for hiding this comment

tb65536 Oct 21, 2022

Choose a reason for hiding this comment

ocfnash Oct 22, 2022

Choose a reason for hiding this comment

tb65536 Oct 22, 2022

Choose a reason for hiding this comment

tb65536 Oct 22, 2022

Choose a reason for hiding this comment

bors bot commented Oct 21, 2022

tb65536 commented Oct 21, 2022

bors bot commented Oct 21, 2022

tb65536 commented Aug 17, 2022 •

edited

Loading

tb65536 commented Oct 21, 2022 •

edited

Loading

ocfnash left a comment •

edited

Loading