embeddings and hook arrow notation: (regular) monomorphisms

Stream: maths

[Kyle Miller]

I was wondering about notation for monomorphisms vs regular monomorphisms. This is motivated by graph theory formalization, but it applies to smooth manifolds, too, where needing both is more immediately believable to me, so I'll state it in terms of topology. A monomorphism in the category of smooth manifolds is an injective smooth map, and a regular monomorphism in the category is an injective smooth map that induces a diffeomorphism onto the image with the induced smooth structure. Are these notions already in mathlib for smooth manifolds? Is there a recommendation for bundling or not bundling these sorts of morphisms?

I would be tempted to have ↪ for monomorphisms (like function.embedding already) and maybe ↪r for regular monomorphisms (like function.rel_embedding which incidentally is a regular monomorphism in a suitable category), but there seem to be lots of other options, too, for how to set things up. (One ergonomic complexity: saying a monomorphism is a homomorphism that's injective on vertices is ok for simple graphs, but for multigraphs you need injectivity on the edge set, too.)

Ok, so what does this have to do with graphs? Thinking of graphs as being 1D simplicial complexes, there is some use in considering both of these kinds of monomorphisms. Monomorphisms are just injective maps, with images ranging over all subgraphs (subcomplexes), but regular monomorphisms are injective maps whose image has the induced simplicial structure (i.e., is an induced subgraph). The image of a regular monomorphism has a regular neighborhood (an open neighborhood from including the interiors of some edges), which is the simplicial complex version of a tubular neighborhood.

I've been told that regular monomorphisms for graphs are useful to model theorists (hi @Aaron Anderson!), and so they'd like some specific notation for it.

[Scott Morrison]

src#category_theory.regular_mono

[Scott Morrison]

Notation is overrated, in my view. :-)

[Kyle Miller]

Oh, cool, morphism properties are all done with typeclasses.

It would be nice in certain contexts to be able to have hookarrow be an abbreviation for "this is a map that has a mono instance." For notation, sometimes I'm very pro-Lisp, where of course you can do everything with s-expressions and the regularity helps you reason about code, but other times I'm feeling more pro-APL or J, where density can help you see larger-scale patterns. They both seem useful in different contexts. (I am very thankful that Lean lets you go to the definition for custom notation -- this would be a nightmare without editor support!)

[Heather Macbeth]

Well, or affine spaces.