Kyle Miller (Aug 31 2020 at 18:20):
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 (Aug 31 2020 at 22:41):
Scott Morrison (Aug 31 2020 at 22:42):
Notation is overrated, in my view. :-)
Kyle Miller (Aug 31 2020 at 22:55):
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 (Aug 31 2020 at 22:56):
Well, or affine spaces.
Last updated: May 19 2021 at 03:22 UTC