RFC: open immersion / embedding

Stream: maths

[Kevin Buzzard]

I've asked here several times about whether Lean has open immersions a.k.a open embeddings a.k.a. injections X -> Y of topological spaces which are isomorphic to the inclusion of an open subset. I don't think we do, and I feel confident enough nowadays to be able to PR them myself. I attempted to make a start and immediately ran into questions of (a) name (b) bundle/unbundle (c) notation. Does anyone have any comments on the below code?

import topology.order

-- An open immersion is a continuous injection of topological spaces which is also an open map.
-- Or is it called open embedding?

open function set

structure open_immersion (α : Type*) (β : Type*) [topological_space α] [topological_space β] :=
(to_fun : α → β)
(cts : continuous to_fun)
(inj : injective to_fun)
(is_open : _root_.is_open (range to_fun))

def is_open_immersion (α : Type*) (β : Type*)
[tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
function.injective f ∧ tα = tβ.induced f ∧ _root_.is_open (range f)

infixr ` ↪₀ `:25 := open_immersion

I think algebraic geometers call them open immersions, and differential geometers call them open embeddings (what do I know, I'm a number theorist). I see from topology/maps.lean that we have things like

def embedding [tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
function.injective f ∧ tα = tβ.induced f

but that might have been written before we came round to a "bundle morphisms" philosophy.

[Kevin Buzzard]

https://mathoverflow.net/questions/48527/why-open-immersion-rather-than-open-embedding for example, to see a debate about the naming issue.

[Mario Carneiro]

I think we should leave topological functions unbundled for now. Unlike linear maps, it's not like open immersions have a nice algebraic structure of their own

[Reid Barton]

#1059 adds open embeddings but now I remember it got caught up in some minor issue.

[Sebastien Gouezel]

As to the bundled/unbundled question, the vague opinion I have formed over time is the following: if a property is the essential feature of an object, it should be bundled. If it is some additional property that might be satisfied by some of the objects you want to play with, but not all of them, then it should be unbundled. In some situations, both make sense, and then I am happy to have both.

Examples:

• the derivative of a map is a linear map by essence, so it should be bundled (using linear_map).
• The composition of two linear maps is well defined, and it turns out that the left-composition (or right-composition) by a fixed linear map is a linear operation on the space of linear maps. But that's not the essence of what I want to do, I really want to think of it as composition. Here, unbundled is better (using is_linear_map).