## Stream: maths

### Topic: (uniform) inducing vs embedding

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

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

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

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

#### Yury G. Kudryashov (Mar 02 2020 at 02:31):

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

#### Reid Barton (Mar 02 2020 at 02:47):

Even T_0 is enough.

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

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

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