Commit 2019-07-09 20:34 3a7c661a
View on Github →refactor(topology/*): define and use dense_inducing (#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 mapf : α → β
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 equationdense_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 tofunction.uncurry
(which suffered from abusive pattern matching, similar toprod.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