Questions about particular design decisions

Stream: sphere eversion

[Michael Rothgang]

Looking closely at the ToMathlib folder, I noticed a few design decision I don't find obvious. Can you help me understand Chesterton's fence here, i.e. describe why you decided this way?

1. Smooth germs
   Right now, smooth germs (of smooth functions $f : M \to \mathbb{R}$ are defined as the image of a particular ring homomorphism (RingHom.germOfContMDiffMap). Is there a reason why you didn't choose, say, ofFun '' { smooth functions $$M \to R$$ } instead? (Is this some detail about coercions I don't know yet?)

(Side note: the mathlib-ready definition should clearly generalise beyond the real numbers. The current defintion generalises virtually unchanged to any smooth ring, but I'd like a definition for smooth maps $M \to N$ into any smooth manifold.)

2. In several places, you're using a definition instead of a structure: for instance, in ToMathlib/Analysis/CutOff or in Global/SmoothEmbedding. Is there a particular reason why? In mathlib, the topological embeddings are a structure... (In fact, I also wrote a definition of smooth embeddings (on branch#MR-submersions-embeddings-advanced) with the same design.)
   Put differently: what would you think of adding/upstreaming structure versions and (eventually) switching to it?

[Anatole Dedecker]

Re: 2. I think you mean def/structure rather than unbundled/bundled. Bundled maps are things like docs#LinearMap, where the map and the property are bundled together, so in your code both Immersion and Immersion' are unbundled.

[Michael Rothgang]

Indeed, thanks. I have corrected my terminology.

[Michael Rothgang]

Update: I realised at least one complication for smooth embeddings --- there's an explicit design decision about including an inverse map. Not including an invFun means you need to prove smoothness of the inverse (which currently cannot be stated in general, as mathlib doesn't have submanifolds yet).
In other words, I'll leave this as-is for the moment.

[Patrick Massot]

I'm sorry I missed this discussion. Let me look at those questions.

[Patrick Massot]

Michael Rothgang said:

Looking closely at the ToMathlib folder, I noticed a few design decision I don't find obvious. Can you help nme understand Chesterfon's fence here, i.e. describe why you decided this way?

1. Smooth germs
   Right now, smooth germs (of smooth functions $f : M \to \mathbb{R}$ are defined as the image of a particular ring homomorphism (RingHom.germOfContMDiffMap). Is there a reason why you didn't choose, say, ofFun '' { smooth functions $$M \to R$$ } instead? (Is this some detail about coercions I don't know yet?)

The reason is that defining it as the image of a ring morphism gives you the ring structure for free.

[Patrick Massot]

It even gives you a subring.

[Patrick Massot]

Michael Rothgang said:

2. In several places, you're using a definition instead of a structure: for instance, in ToMathlib/Analysis/CutOff or in Global/SmoothEmbedding. Is there a particular reason why? In mathlib, the topological embeddings are a structure... (In fact, I also wrote a definition of smooth embeddings (on branch#MR-submersions-embeddings-advanced) with the same design.)
   Put differently: what would you think of adding/upstreaming structure versions and (eventually) switching to it?

I always use functions and predicates because this is what is done for continuous functions and differentiable functions in Mathlib. But if you switch to bundles smooth maps and it brings no pain then I don't have strong feelings about this.

[Anatole Dedecker]

I don’t think it’s really a bundling question (IIUC), rather "should it be an and or a structure (extending docs#Embedding for example)

[Anatole Dedecker]

That is, in the linked branch, should we use Immersion or Immersion'

[Patrick Massot]

Oh I see! That conversation would have been a lot easier to follow with this link

[Patrick Massot]

So the answer is simply that having a definition with a single definition was simpler. Why adding a redundant one? Otherwise I usually prefer a structure over an and (and of course there is no discussion as soon as there are at least three conditions).

[Michael Rothgang]

Thanks for the responses, this is really helpful.
Regarding 1. Sure, I understand (and additional structure is always nice). I'm wondering: is that structure used in sphere-eversion? Given that germs of smooth functions are well-defined for the target just being a manifold, I'd rather add the general definition to mathlib (and add the ring homomorphism structure on top).

[Michael Rothgang]

Regarding 2: sure, makes sense.
Thinking about a mathlib-suitable version, as a user of Immersion I would certainly like to have differentiability at my disposal. What do you think about replacing Immersion' with a new constructor for Immersion, assuming only injectivity of the mfderiv and a mild hypothesis (like positive dimension or a connected domain)?

[Michael Rothgang]

In any case, this is not an urgent question: the proper definition of immersions (and embeddings) for Banach manifolds is different from this one. I intend to add immersions and embeddings to mathlib, but this will not happen very soon.

[Patrick Massot]

Michael Rothgang said:

Thanks for the responses, this is really helpful.
Regarding 1. Sure, I understand (and additional structure is always nice). I'm wondering: is that structure used in sphere-eversion? Given that germs of smooth functions are well-defined for the target just being a manifold, I'd rather add the general definition to mathlib (and add the ring homomorphism structure on top).

Oh yes it is definitely used a lot. But of course it doesn't mean it cannot be refactored.

[Patrick Massot]

About immersions, I think the reasonable thing to do is to have a main definition which easy to read and clearly correct and then smart constructors on top.

[Kevin Buzzard]

Interesting. In the bialgebra PR #10076 the original definition of a bialgebra was changed at the suggestion of a referee to something unreadable and then I made a dumb constructor for the mathematicians who had only read the textbooks and didn't know about currying maps from tensor products

[Eric Wieser]

It would be nice if we could have the readable definition in the docs, but let the smart one claim where notation.