open_embedding

Stream: maths

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Johan Commelin]

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