## Stream: maths

### Topic: open embeddings

#### Patrick Massot (Sep 16 2019 at 11:44):

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 (Sep 16 2019 at 11:49):

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 (Sep 16 2019 at 12:03):

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

#### Reid Barton (Sep 16 2019 at 12:06):

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 (Sep 16 2019 at 12:07):

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 (Sep 16 2019 at 12:09):

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

#### Johan Commelin (Sep 18 2019 at 11:43):

logic.embedding has the following:

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


#### Johan Commelin (Sep 18 2019 at 11:43):

Do we want topological embeddings to extend those?

#### Johan Commelin (Sep 18 2019 at 11:44):

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

#### Patrick Massot (Sep 18 2019 at 14:18):

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

Last updated: May 19 2021 at 02:10 UTC