refactor(topology/*): define and use dense_inducing #1193

PatrickMassot · 2019-07-08T13:47:31Z

Traditionally, topology extends functions defined on dense subspaces (equipped by the induced topology). In mathlib, this was made type-theory-friendly by rather factoring through dense_embedding maps. A map f : α → β between topological spaces is a dense embedding if its image is dense, it is injective, and it pulls back the topology from β to the topology on α. It turns out
that the injectivity was never used in any serious way. It used not to be used at all until we noticed it could be used to ensure the factorization equation dense_embedding.extend_e_eq could be made to
hold without any assumption on the map to be extended. But of course this formalization trick is mathematically completely irrelevant.

On the other hand, assuming injectivity prevents direct use in uniform spaces completion, because the map from a space to its (separated) completion is injective only when the original space is separated. This is why mathlib ring completion currently assumes a separated topological ring, and the perfectoid spaces project needed a lot of effort to drop that assumption. This commit makes all this completely painless.

Along the way, we improve consistency and readability by turning a couple of conjunctions into structures. Also we introduce a predicate dense_range which was already everywhere, but without a name, and with duplicated proofs.

It also introduces a long overdue fix to function.uncurry (which suffered from abusive pattern
matching, similar to prod.map). Also removes the duplication nhds_induced_eq_comap/nhds_induced.

@sgouezel could you check I didn't harm your metric space completion and Gromov-Hausdorff work? It should be only little simplification, or a bit of help to the elaborator (especially a couple of : _ added with speed).

@rwbarton same question for the Stone-Cech compactification. The main difference should be that the map from a discrete space to ultrafilter on it is first proved to be dense inducing before adding that injectivity also holds. And then injectivity is no longer used anywhere. It means the t2_space assumption needs to be added a bit earlier but this should be totally irrelevant.

See discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/function.20extension and https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/induced.20neighborhoods

jcommelin

Some minor nitpicks. Looks really good!

src/data/prod.lean

src/topology/algebra/uniform_group.lean

src/topology/algebra/uniform_ring.lean

jcommelin · 2019-07-08T18:42:47Z

src/topology/algebra/uniform_ring.lean

    (assume a b,
      by rw [← coe_mul, extension_coe hf, extension_coe hf, extension_coe hf, is_ring_hom.map_mul f]) }

+instance top_ring_compl : topological_ring (completion α) :=


src/topology/constructions.lean

src/topology/uniform_space/completion.lean

src/topology/maps.lean

src/topology/algebra/uniform_ring.lean

src/topology/maps.lean

sgouezel · 2019-07-08T19:18:50Z

src/topology/maps.lean

+  exact hg c
+end
+
+lemma dense_range.inhabited (df : dense_range f) (b : β) : inhabited α :=


Why inhabited instead of nonempty? since there is no canonical element, I think nonempty is more natural -- and if you really need inhabited for some applications, maybe it means that the statements you rely on should also use nonempty instead of inhabited, or otherwise you can easily derive inhabited from nonempty in the application.

inhabited is needed because this is what lim wants.

src/topology/maps.lean

src/topology/metric_space/completion.lean

src/topology/uniform_space/basic.lean

src/topology/uniform_space/uniform_embedding.lean

sgouezel · 2019-07-08T19:35:48Z

Looks very good to me (except for minor nitpicking).

Traditionally, topology extends functions defined on dense subspaces (equipped by the induced topology). In mathlib, this was made type-theory-friendly by rather factoring through `dense_embedding` maps. A map `f : α → β` between topological spaces is a dense embedding if its image is dense, it is injective, and it pulls back the topology from `β` to the topology on `α`. It turns out that the injectivity was never used in any serious way. It used not to be used at all until we noticed it could be used to ensure the factorization equation `dense_embedding.extend_e_eq` could be made to hold without any assumption on the map to be extended. But of course this formalization trick is mathematically completely irrelevant. On the other hand, assuming injectivity prevents direct use in uniform spaces completion, because the map from a space to its (separated) completion is injective only when the original space is separated. This is why mathlib ring completion currently assumes a separated topological ring, and the perfectoid spaces project needed a lot of effort to drop that assumption. This commit makes all this completely painless. Along the way, we improve consistency and readability by turning a couple of conjunctions into structures. It also introduces long overdue fix to `function.uncurry` (which suffered from abusive pattern matching, similar to `prod.map`).

PatrickMassot

Thank you very much @sgouezel and @jcommelin!

PatrickMassot · 2019-07-09T09:13:43Z

src/topology/maps.lean

+  exact hg c
+end
+
+lemma dense_range.inhabited (df : dense_range f) (b : β) : inhabited α :=


inhabited is needed because this is what lim wants.

src/topology/maps.lean

src/topology/uniform_space/completion.lean

Co-Authored-By: Johan Commelin <johan@commelin.net> Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

PatrickMassot

I think I've fixed everything, and this is good to go.

src/topology/algebra/uniform_group.lean

src/topology/maps.lean

jcommelin · 2019-07-09T12:24:01Z

@PatrickMassot The commit title also seems a bit funny. Did you mean to use the word "use"?

sgouezel · 2019-07-09T13:09:17Z

For me, this is good to go. @jcommelin, once you're happy you can mark it as ready to merge.

PatrickMassot · 2019-07-09T13:09:41Z

Indeed the PR title misses the word "use". I'm not sure I can safely change that (I don't think rewriting history would be good for this discussion).

jcommelin · 2019-07-09T14:56:12Z

@sgouezel Great! It's on the merge queue.

semorrison · 2019-07-10T16:40:54Z

You can just click "edit" next to the PR title itself.

…

On Tue, Jul 9, 2019, 3:09 AM Patrick Massot ***@***.***> wrote: Indeed the PR title misses the word "use". I'm not sure I can safely change that (I don't think rewriting history would be good for this discussion). — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1193?email_source=notifications&email_token=AADUWBEXHCMDNDUKALD3TG3P6SEZNA5CNFSM4H634RCKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZQGVTA#issuecomment-509635276>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADUWBD4H2KFQBDVXWMRNNDP6SEZNANCNFSM4H634RCA> .

…nity#1193) * refactor(topology/*): define and dense_inducing Traditionally, topology extends functions defined on dense subspaces (equipped by the induced topology). In mathlib, this was made type-theory-friendly by rather factoring through `dense_embedding` maps. A map `f : α → β` between topological spaces is a dense embedding if its image is dense, it is injective, and it pulls back the topology from `β` to the topology on `α`. It turns out that the injectivity was never used in any serious way. It used not to be used at all until we noticed it could be used to ensure the factorization equation `dense_embedding.extend_e_eq` could be made to hold without any assumption on the map to be extended. But of course this formalization trick is mathematically completely irrelevant. On the other hand, assuming injectivity prevents direct use in uniform spaces completion, because the map from a space to its (separated) completion is injective only when the original space is separated. This is why mathlib ring completion currently assumes a separated topological ring, and the perfectoid spaces project needed a lot of effort to drop that assumption. This commit makes all this completely painless. Along the way, we improve consistency and readability by turning a couple of conjunctions into structures. It also introduces long overdue fix to `function.uncurry` (which suffered from abusive pattern matching, similar to `prod.map`). * Apply suggestions from code review Co-Authored-By: Johan Commelin <johan@commelin.net> Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * minor fixes following review * Some more dot notation, consistent naming and field naming

PatrickMassot requested a review from a team as a code owner July 8, 2019 13:47

jcommelin reviewed Jul 8, 2019

View reviewed changes