Zulip Chat Archive

Stream: maths

Topic: open_embedding


view this post on Zulip Kevin Buzzard (Apr 23 2019 at 17:38):

Should open_embedding (an open map which is an embedding) be a class? I want to prove ten things about open embeddings and define some comap stuff (pulling back a bunch of structures along open embeddings). Currently I have this:

import topology.maps

class open_embedding {α : Type*} {β : Type*} [topological_space α] [topological_space β]
  (f : α  β) : Prop :=
(Hopen : is_open_map f)
(Hembedding : embedding f)

But then I remember that in core Lean things like bijective f is not defined as a class at all, it's just injective f \and surjective f. Which is the best approach? What will make things easier later on?

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 17:41):

I think this is the Stricklandization of the inclusion of an open subset of alpha into alpha

view this post on Zulip Johan Commelin (Apr 23 2019 at 18:15):

Note that you could also have other hypotheses, like

  • is_open (set.range f) and embedding f, or
  • is_open_map f and injective f and continuous f
    So we will likely want several constructors

Last updated: May 18 2021 at 08:14 UTC