Zulip Chat Archive

Stream: maths

Topic: Notation for ext_chart_at


Winston Yin (Nov 01 2022 at 00:34):

Would anyone object to a new notation for docs#ext_chart_at? They are quite a pain to type repetitively when working with manifolds. I propose 𝓔(I, x) to mean ext_chart_at I x, where the script E is entered with \MCE.

Winston Yin (Nov 01 2022 at 05:21):

PR #17294 shows the effect of the new notation for ext_chart_at.

Floris van Doorn (Nov 01 2022 at 20:09):

I haven't found ext_chart_at particularly annoying to write myself, so I'm neutral towards this proposal.
If we do this, do we want similar notation for chart_at?

Winston Yin (Nov 02 2022 at 07:34):

  • 𝓔(I, x) is much shorter, allowing formulas involving them to look like their regular mathematical counterparts. For me, it has made reading and thinking about these formulas much quicker.
  • I find myself going back and adding parentheses to ext_chart_at I x all the time when I need to append .symm, .source, .target. Writing 𝓔(I, x) would eliminate the need for this decision.
  • The notation 𝓝 for nhds seems like a negative improvement (5 keystrokes instead of 4 including shift key) compared to 𝓔 for ext_chart_at (5 instead of 14).

Winston Yin (Nov 02 2022 at 07:36):

As for chart_at, I guess a natural choice would be 𝓒 (\MCC), but it looks so darn similar to 𝓔.

Winston Yin (Nov 02 2022 at 07:39):

One alternative proposal would be to use 𝓒(H, x) (script C) for chart_at and e𝓒(I, x) or 𝓒ₑ(I, x) for ext_chart_at (also script C).

Kevin Buzzard (Nov 02 2022 at 07:41):

If you just want this for files you're writing you can use local notation, this trick (or a local abbreviation) is used several times in mathlib to save typing

Floris van Doorn (Nov 02 2022 at 07:57):

Not everything is about saving keystrokes. We use 𝓝 in mathlib because it is commonly used notation for neighborhoods.

Patrick Massot (Nov 02 2022 at 08:13):

Winston, the neighborhood notation does save key, you only need to type \nh to trigger it.

Winston Yin (Nov 02 2022 at 10:16):

I suppose a local notation is sufficient for my use. Thanks for the comments!


Last updated: Dec 20 2023 at 11:08 UTC