Zulip Chat Archive

Stream: maths

Topic: (uniform) inducing vs embedding


view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 01:29):

Hi, when a uniform_inducing map is not uniform_embedding? I see that uniform_embedding is uniform_inducing + injective but I don't see examples of uniform_inducing non-injective maps in mathlib. Is it possible, e.g., in a t2_space? Or this is all about some strange topologies with glued points?

view this post on Zulip Reid Barton (Mar 02 2020 at 02:26):

If an inducing map sends two points to the same thing then I think the two points have the same neighborhoods. Right Patrick?

view this post on Zulip Reid Barton (Mar 02 2020 at 02:27):

I think the examples are things like premetric spaces before you form the quotient by zero distance, eg, Cauchy sequences

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 02:31):

I think this deserves to be mentioned in the docstring, and maybe a theorem (inducing + some separation ⇒ injective, thus embedding).

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 02:31):

And probably we don't need injective in emetric.uniform_embedding_iff.

view this post on Zulip Reid Barton (Mar 02 2020 at 02:47):

Even T_0 is enough.

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:42):

If an inducing map sends two points to the same thing then I think the two points have the same neighborhoods. Right Patrick?

Sure, it's almost the definition (and should be called something like inducing.nhds_eq_comap).

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:44):

Yury, the main application of uniform_inducing is the map from a uniform space to its separated completion. You can read the perfectoid formalization paper if you'd like to know more about this.

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:44):

And this is not an injective map if the original uniform space is not separated.


Last updated: May 06 2021 at 18:20 UTC