(uniform) inducing vs embedding

Stream: maths

[Yury G. Kudryashov]

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?

[Reid Barton]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Reid Barton]

Even T_0 is enough.

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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