Zulip Chat Archive

Stream: new members

Topic: Proving that a continuous map is inducing (topology)

Ruth Plümer (Feb 09 2025 at 15:21):

Hello everyone,
I'm currently trying to prove that a certain continuous map

f : ContinuousMap X Y

is an embedding and I decided to prove it by using embedding_iff and proving that it is both injective and inducing, but I am currently a little stuck when trying to prove that it is inducing. I know how to prove that a set is open in X iff its image is open in Y, but I can't find a lemma in mathlib that shows that a map is inducing if it has this property.

The only characterizations of inducing maps all yield that f is inducing if and only if

TopologicalSpace X = induced f (TopologicalSpace Y)

but I don't know how to prove induced f (TopologicalSpace Y) with what I've proven either. I've tried loogle, but I haven't found any lemma that seems useful.
Could someone please give me a hint on how to prove that f is inducing? I am not looking for code for the lemma I'm looking for, just maybe a hint on how to proceed.

Aaron Liu (Feb 09 2025 at 15:23):

You will have more luck searching for docs#Topology.IsInducing, docs#Topology.Inducing is deprecated.

Aaron Liu (Feb 09 2025 at 15:25):

I found docs#Topology.isInducing_iff_nhds, does this work for you?

Ruth Plümer (Feb 09 2025 at 15:57):

Yes, this seems to be what I was looking for, thank you!

Michael Rothgang (Feb 10 2025 at 14:21):

Another strategy: prove that IsOpenMap f (i.e., f maps open sets map to open sets), and then use a lemma that f is an embedding iff it is continuous, injective and an open map.