[Merged by Bors] - feat(geometry/manifold): bundled smooth map #3904

Nicknamen · 2020-08-21T22:52:36Z

First part of #3641 as a separate PR.

src/geometry/manifold/times_cont_mdiff.lean

Nicknamen · 2020-08-22T08:27:00Z

src/geometry/manifold/times_cont_mdiff_map.lean

+/-- Bundled smooth maps. -/
+@[reducible] def smooth_map := times_cont_mdiff_map I I' M M' ⊤
+
+notation `C[` n `](` I `, ` M `; ` I' `, ` M' `)` := times_cont_mdiff_map I I' M M' n


I don't particularly like this notation but for some arcane reason Lean accepts C^n](I, M; I' M') but not C^n(I, M; I' M') which is the one I would prefer.

Lean doesn't allow/like an opening parenthesis ( as a token in notation.

This notation is bad though: after declaring this notation, whenever Lean sees ]( it will treat them as a single token, which is problematic if you meant to write ] (. So for example, this example will fail after this notation is declared, because there is no space between ] (.

example {α} [group α](x : α) : x = x := rfl

Ok do you have suggestions for a better notation? I am not really sure about how to invent a good one!

If you reorder the arguments of times_cont_mdiff_map, you could do

notation `C[` n `]` := times_cont_mdiff_map n

and then you can write C[n] I M I' M'. Would that be acceptable?

Oh, that doesn't work with the notations below this...
You could try C^n[ I, M; I', M' ], That should work, but uses square brackets...

It shouldn't be:

instance has_scalar' : has_scalar C^n ⦃I, N; 𝕜⦄ C^n ⦃I, N; J, V⦄

should work just fine (and if it doesn't it just means you need to adjust binding priorities)

But in fact I prefer the version with parentheses, it looks more readable to me.

I changed it but I still think it was better before for 3 reasons:

like this it seems C^n and ⦃I, N; 𝕜⦄ are separate arguments and to my eye it cofuses things: looking at statements before it was easy to get with a glimpse which things are together and which are not (in has_scalar C^n ⦃I, N; 𝕜⦄ C^n ⦃I, N; J, V⦄ it seems has_scalar is taking 4 arguments; also things like inhabited C^n ⦃I, M; I', M'⦄ or has_coe (E →L[𝕜] E') C^n ⦃𝓘(𝕜, E), E; 𝓘(𝕜, E'), E'⦄ now look confusing). Adding parenthesis in complicated statements is always bad of readability, when parentheses are more than 4 the eye can't follow them well anymore. I really don't see any reason why the space improves readability

again this is not in line with the notation of continuous functions

this is not in line with the notation in standard maths where there is no space

Coherence is a very important goal. We have spaces everywhere before parentheses in mathlib, so why would you want to remove them here? You even wrote yourself has_coe (E →L[𝕜] E') and not has_coe(E →L[𝕜] E')... In the same way, you should probably write 𝓘 (𝕜, E) instead of 𝓘(𝕜, E), by the way -- or even better 𝓘 𝕜 E, again for coherence. The goal is not to mimick the usual mathematical notation at all cost.

Indeed I want to remove them because of coherence!! The convention in mathlib seems to be that notation involving just one character and parentheses that are part of the notation do not have spaces in between them (I think this is very reasonable, but it is not me who chose this, it has been like this since ever, so we should ask someone else to understand why this choice was made!). Just to quote some examples:

C(X, Y) denotes continuous functions and does not have a space (and coherence with this is very important here in my opinion as this will become C⦃X, Y⦄).

𝓝[s] denotes neighborhood within and is written without space

X⟦n⟧ is notation for shift in category theory, written without space

f⟦n⟧ as above does not have a space

morphisms like →L[𝕜] involving one letter and a parenthesis do not have a space (they are not →L [𝕜])

![a, b, ...] does not have a space

ℤ_[p] or ℚ_[p] do not have spaces
I can list you other examples but you got the idea!

I think that if we decide not to follow this convention here we should propose to change it everywhere else in mathlib as well. We could ask on Zulip what people think of changing this across mathlib?

jcommelin · 2020-08-26T18:41:54Z

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -151,6 +151,10 @@ def model_with_corners_self (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
  continuous_to_fun  := continuous_id,
  continuous_inv_fun := continuous_id }

+localized "notation `Isf(` 𝕜 `, ` E `)` := model_with_corners_self 𝕜 E" in manifold


What does Isf stand for?

I is the most common letter used for model_with_corners and sf stands for self. It is like that because @sgouezel suggested Iself but I wanted something even shorter.

Johan's comment shows that Isf is essentially impossible to understand just by itself, so I think Iself is a better idea. A problem with your notation is that Iself( would work, but not Iself (, while usually there is a space before the parentheses. I don't know if there is a parsing trick to allow both, or if you should just register both versions (or just remove the parentheses, to have something that is more Lean-like, and let Iself just be a notation for model_with_corners_self).

I'm skeptical that any notation which requires a struggle to make work is going to be robust, and to me model_with_corners_self is a big improvement over Isf (or even Iself).

Remember that the reader counts more than the writer when developing new notations. :-) They are not merely to save keystrokes!

In this context, this is a statement with full notation

instance has_scalar' : has_scalar C∞(𝓘(𝕜, N), N; 𝓘(𝕜), 𝕜) C∞(𝓘(𝕜, N), N; 𝓘(𝕜, V), V)

This is a statement with partial notation

instance has_scalar' : has_scalar C∞((model_with_corners_self 𝕜 N), N; (model_with_corners_self 𝕜 𝕜), 𝕜) C∞((model_with_corners_self 𝕜 N), N; (model_with_corners_self 𝕜 V), V)

and this is a statement without notation

instance has_scalar' : has_scalar (times_cont_mdiff_map (model_with_corners_self 𝕜 N) (model_with_corners_self 𝕜 𝕜) N 𝕜 ⊤) (times_cont_mdiff_map (model_with_corners_self 𝕜 N) (model_with_corners_self 𝕜 V) N V ⊤)

I believe the point here is not at all saving keystrokes (I actually never introduced any of my notations for this reason), the point is that statements in differential geometry, which has way more stuff going on formally than many areas of maths, are unreadable without notations. If we take a differential geometry textbook and remove notation, and write everything with long names fulls of underscore, I wonder if anyone could actually understand the statements after a while. If the first statement also looks unreadable to you, it might help to know that it looked very readable to me after one day of using this notation, whereas the second and third statements looked to me very unreadable even after months of usage.

In this precise situation, we will very rarely consider a smooth structure on a vector space that does not come from model_with_corners_self and the point of this notation is not to draw all the attention to this, since this is just a technical thing needed for formalization and it is quickly left behind in standard maths. The point is also that the human brain generally recognizes shapes when reading, it does not read every single letter (there's a lot of nice games showing this), so any notation will not represent any effort after having learned it the first time. For the same reason in the case of not using notation, after having learned what model_with_corners_self is, when people will read it they will just give a glance to it and they will not read every single letter, which will therefore have no real reason to be there. In addition, I also bet that the first time someone reads model_with_corners_self they will right-click anyways it to see what it is since, being a concept which is not explicitly on most geometry books, they will want to verify that it is what they think. So I am not sure it would really save effort even the first time someone sees it.

A similar thing is valid for Iself, I believe that if I wrote Iself Johan would have all the same asked "What does I stand for?" so I am not sure why it is a better idea (again, the first time that someone will see it they will right-click it anyways, no matter what notation is, and the second time, when they learned, the name won't matter, as long as it is something reasonable which is easy to remember). If it were for me, I would use just a symbol related to the letter I such as 𝓘 but if neither this nor Isf can be accepted (although again I would not see why) I would at least like anything which is shorter then model_with_corners_self such as Iself. Putting aside theoretical explanations, I've been practically using the geometry library without notation for more than 2 months and I strongly believe the experience of using it with notation is multiple times better: it is not just quicker to write, but more readable, cleaner and it contains way fewer lines: having to break a statement over multiple lines is distracting. If you are not convinced I can show you a whole file in the two versions to see the difference in practice.

As for parenthesis, sure although I do not see why the notation we used up to know for continuous functions was not a problem: it does exactly what you do not like. If the point is that you accept this for one-letter notation only, then I repropose the notation 𝓘, which would solve both problems.

I vote for 𝓘

Ok cool I fixed it to \MCI. Another idea could be 𝓢 for self, also considering that it is written \MCS that is an acronym of Model with Corners Self.

sgouezel · 2020-08-29T13:54:02Z

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -151,6 +151,10 @@ def model_with_corners_self (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
  continuous_to_fun  := continuous_id,
  continuous_inv_fun := continuous_id }

+localized "notation `Isf(` 𝕜 `, ` E `)` := model_with_corners_self 𝕜 E" in manifold


Johan's comment shows that Isf is essentially impossible to understand just by itself, so I think Iself is a better idea. A problem with your notation is that Iself( would work, but not Iself (, while usually there is a space before the parentheses. I don't know if there is a parsing trick to allow both, or if you should just register both versions (or just remove the parentheses, to have something that is more Lean-like, and let Iself just be a notation for model_with_corners_self).

src/geometry/manifold/times_cont_mdiff.lean

src/geometry/manifold/times_cont_mdiff_map.lean

sgouezel · 2020-08-29T14:03:01Z

src/geometry/manifold/times_cont_mdiff_map.lean

+/-- Bundled smooth maps. -/
+@[reducible] def smooth_map := times_cont_mdiff_map I I' M M' ⊤
+
+notation `C[` n `](` I `, ` M `; ` I' `, ` M' `)` := times_cont_mdiff_map I I' M M' n


Maybe change to a calligraphic C, i.e., 𝓒 (type with \MCC) to avoid ambiguities. I think 𝓒^n[ I, M; I', M'] is fine, can you change to it?

src/geometry/manifold/times_cont_mdiff_map.lean

jcommelin · 2020-09-11T11:19:16Z

@sgouezel @Nicknamen What is the status here?

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel · 2020-09-20T12:58:31Z

If you change the notations to C^ and 𝓘, which seems to be the most reasonable choice given the arguments you have given, I think it should be good to go.

…mmunity/mathlib into smooth_bundled_map

PatrickMassot · 2020-09-23T20:01:15Z

bors merge

Nicknamen · 2020-09-23T21:17:54Z

I think there actually were a couple of points still open...

bors · 2020-09-23T22:34:08Z

Pull request successfully merged into master.

Build succeeded:

Nicknamen requested a review from sgouezel August 21, 2020 22:55

Bundled smooth maps

24e81ea

Nicknamen force-pushed the smooth_bundled_map branch from 4a29b58 to 24e81ea Compare August 22, 2020 07:41

Nicknamen commented Aug 22, 2020

View reviewed changes

src/geometry/manifold/times_cont_mdiff.lean Show resolved Hide resolved

Nicknamen commented Aug 22, 2020

View reviewed changes

Nicknamen added the awaiting-review The author would like community review of the PR label Aug 22, 2020

jcommelin reviewed Aug 26, 2020

View reviewed changes

Nicknamen mentioned this pull request Aug 28, 2020

[Merged by Bors] - feat(geometry/manifold): smooth bundled maps #3641

Closed

sgouezel reviewed Aug 29, 2020

View reviewed changes

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 2, 2020

Update src/geometry/manifold/times_cont_mdiff_map.lean

3e2f3a5

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Nicknamen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 18, 2020

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 20, 2020

Nicknamen added 2 commits September 22, 2020 15:55

Applied suggested changes

5c57c1e

Merge branch 'smooth_bundled_map' of https://github.com/leanprover-co…

8993873

…mmunity/mathlib into smooth_bundled_map

Nicknamen force-pushed the smooth_bundled_map branch from 1b61589 to 8993873 Compare September 22, 2020 14:02

Trying with different notation

01b663a

Nicknamen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 23, 2020

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 23, 2020

Changing notation again

65ff8cf

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 23, 2020

bors bot pushed a commit that referenced this pull request Sep 23, 2020

feat(geometry/manifold): bundled smooth map (#3904)

9aeffa8

bors bot changed the title ~~feat(geometry/manifold): bundled smooth map~~ [Merged by Bors] - feat(geometry/manifold): bundled smooth map Sep 23, 2020

bors bot closed this Sep 23, 2020

bors bot deleted the smooth_bundled_map branch September 23, 2020 22:34

Nicknamen mentioned this pull request Oct 24, 2020

Adding diffeos and smooth bundled maps AnthonyBordg/Geometry_in_Lean#8

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(geometry/manifold): bundled smooth map #3904

[Merged by Bors] - feat(geometry/manifold): bundled smooth map #3904

Nicknamen commented Aug 21, 2020

Nicknamen Aug 22, 2020

fpvandoorn Aug 27, 2020

Nicknamen Aug 27, 2020 •

edited

fpvandoorn Aug 27, 2020

fpvandoorn Aug 27, 2020

sgouezel Sep 23, 2020

sgouezel Sep 23, 2020

Nicknamen Sep 23, 2020 •

edited

sgouezel Sep 23, 2020

Nicknamen Sep 23, 2020 •

edited

jcommelin Aug 26, 2020

Nicknamen Aug 27, 2020

sgouezel Aug 29, 2020

semorrison Sep 1, 2020

Nicknamen Sep 14, 2020 •

edited

sgouezel Sep 20, 2020

Nicknamen Sep 22, 2020

sgouezel Aug 29, 2020

sgouezel Aug 29, 2020

jcommelin commented Sep 11, 2020

sgouezel commented Sep 20, 2020

PatrickMassot commented Sep 23, 2020

Nicknamen commented Sep 23, 2020

bors bot commented Sep 23, 2020

[Merged by Bors] - feat(geometry/manifold): bundled smooth map #3904

[Merged by Bors] - feat(geometry/manifold): bundled smooth map #3904

Conversation

Nicknamen commented Aug 21, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Nicknamen Aug 27, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Nicknamen Sep 23, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Nicknamen Sep 23, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Nicknamen Sep 14, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin commented Sep 11, 2020

sgouezel commented Sep 20, 2020

PatrickMassot commented Sep 23, 2020

Nicknamen commented Sep 23, 2020

bors bot commented Sep 23, 2020

Nicknamen Aug 27, 2020 •

edited

Nicknamen Sep 23, 2020 •

edited

Nicknamen Sep 23, 2020 •

edited

Nicknamen Sep 14, 2020 •

edited