open embeddings

Stream: maths

[Patrick Massot]

We bumped mathlib in the perfectoid project and got https://github.com/leanprover-community/mathlib/commit/10cb0d125d1d02d0ea68e478456c522bd1920d29 which conflicts with our own implementation of open_embedding https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/open_embeddings.lean. We should decide whether we adapt our code to use mathlib open embeddings or PR something. @Reid Barton there are a couple of things to decide here. First we put open_embedding in the topological_space namespace whereas you put it in root. I think we are clearly right, what will we do when the algebraic geometry gang will claim we have the wrong definition?

With slightly more mathematical content, we have a definition which looks stronger but is equivalent. We ask that an open embedding is an embedding which is open. You only ask is has open range. Also we use a structure, in order to have meaningful names for each condition, h.is_open_map and h.embedding rather that h.1 and h.2. Do you have any a priori objection to merge our efforts using our definition (and namespace)?

[Reid Barton]

I noticed that embedding changed to a structure so it makes sense for open_embedding to change to one as well. I just ask you make corresponding changes to closed_embedding too

[Patrick Massot]

What about putting the (seemingly) stronger condition in the definition, are you ok with that?

[Reid Barton]

For propositions the exact definition usually doesn't matter much. Normally I think we try to make the definition something easy to check, since the constructor has special support. You can emulate extracting the is_open_map field by defining a function open_embedding.is_open_map.

[Reid Barton]

Normally it should be easier to check that the range is open than that the image of an open set is open (maybe not in open_embedding.comp though)

[Patrick Massot]

I guess we also want mathematicians not to be surprised by the definition. But maybe this case is unclear

[Johan Commelin]

logic.embedding has the following:

structure embedding (α : Sort*) (β : Sort*) :=
(to_fun : α → β)
(inj    : injective to_fun)

[Johan Commelin]

Do we want topological embeddings to extend those?

[Johan Commelin]

In other words, should topological embeddings be bundled maps, or a predicate on a function?

[Patrick Massot]

I settled for a minimal change, simply making open_embedding and closed_embedding structures extending embedding: https://github.com/leanprover-community/mathlib/pull/1459