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 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
  • Apply suggestions from code review Co-Authored-By: Johan Commelin Co-Authored-By: sgouezel
  • minor fixes following review
  • Some more dot notation, consistent naming and field naming

Estimated changes

added theorem closed_embedding.comp
deleted theorem closed_embedding_compose
deleted theorem dense_embedding.extend_eq
modified theorem dense_embedding.inj_iff
modified structure dense_embedding
added theorem'
added structure dense_inducing
added theorem dense_range.comp
added theorem dense_range.inhabited
added def dense_range
added theorem embedding.comp
added def'
added theorem embedding.prod_mk
added structure embedding
deleted def embedding
deleted theorem embedding_compose
deleted theorem embedding_prod_mk
added theorem inducing.comp
added theorem inducing.continuous
added theorem inducing.map_nhds_eq
added theorem inducing.nhds_eq_comap
added theorem inducing.prod_mk
added structure inducing
added theorem inducing_id
added theorem inducing_is_closed
added theorem inducing_open