Commit 2019-07-09 20:34 3a7c661a

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 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