# Zulip Chat Archive

## 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