Notation for `linear_pmap`

Stream: maths

[Moritz Doll]

I think the time has come that I really want to have notation for linear_pmap R E F, but I have no good idea. The natural choices would be E →ₗₚ[R] F or E →ₚₗ[R] F, but lp feels very wrong and I am not convinced about pl either. Are there maybe some good-looking arrows that could be used in conjunction with l?

[Yaël Dillies]

A dashed arrow, to illustrate that it's partial?

[Moritz Doll]

⇢ this one would be nice, but in VSCode it looks almost identical to the usual arrow.

[Moritz Doll]

or am I just blind?

[Moritz Doll]

I guess this one is used already ⇀

[Yaël Dillies]

Moritz Doll said:

⇢ this one would be nice, but in VSCode it looks almost identical to the usual arrow.

Actually I find them more different in VScode than on Zulip.

[Anatole Dedecker]

Why not stick with the →. notation from docs#pfun ? So something like →ₗ. ? Or is it too subtle ?

[Moritz Doll]

because I did not know that that exists :grinning:

[Yaël Dillies]

Is docs#linear_pfun actually implemented with pfun?

[Anatole Dedecker]

No (docs#linear_pmap)

[Yaël Dillies]

Sorry, I am writing this from a brick (aka my phone).

[Yaël Dillies]

Then that sounds like a semidangerous association of symbols.

[Moritz Doll]

Why do you think this is semidangerous? I don't think the two definitions will ever be used in the same file

[Yaël Dillies]

Semidangerous is not dangerous! Otherwise it wouldn't be called semidangerous.

[Moritz Doll]

but I've asked why it is semidangerous. and could you define that?

[Yaël Dillies]

Because I can see people finding both and assuming linear_pmap is implemented using pfun, but it's a mild concern, really.

[Frédéric Dupuis]

I don't think we should worry about this, you should never assume anything about implementation details from notation anyway.

[Moritz Doll]

fyi the PR is here #15751

[Mario Carneiro]

I don't think it's all that misleading to associate this with pfun. It very naturally induces one

[Mario Carneiro]

I would argue this is the "natural generalization" of pfun to linear maps

[Moritz Doll]

@Jireh Loreaux mentioned in a PR that the current E →ₗ.[𝕜] F looks too much like E →ₗ⋆[𝕜] F in VSCode, does anyone else have this issue?

[Jireh Loreaux]

A simple solution might be to reverse the order: E →.ₗ[𝕜] F instead of E →ₗ.[𝕜] F

[Jireh Loreaux]

And to be clear, it's not that I can't tell the difference at all on my machine, it's just that I have to do a double take and think about how the characters .and ⋆ normally render on my screen, which seems suboptimal.

[Jireh Loreaux]

(Alternative solution for me: get a bigger screen or better eyes! :rofl:)