Zulip Chat Archive

Stream: maths

Topic: Notation for `affine_map`

Yury G. Kudryashov (Oct 18 2020 at 17:54):

Now affine_map has only 3 explicit arguments, so I think it's time we add a notation. R →ₐ S is taken by docs#alg_hom (at least until someone migrates it to docs#mul_semiring_action_hom). We have the following options:

P₁ →ₐ[k] P₂; lean will be able to tell it from alg_hom because of [k]
P₁ →ᵃᶠᶠ[k] P₂ (I found no subscript f);
P₁ →ᵃ[k] P₂.
What do you think?

Patrick Massot (Oct 18 2020 at 18:52):

I like 1 and 3. The middle one seems too long

Yury G. Kudryashov (Oct 18 2020 at 19:24):

I was wrong about 1: of course, alg_hom needs to know the ring.

Yury G. Kudryashov (Oct 18 2020 at 19:29):

#4675

Patrick Massot (Oct 18 2020 at 19:31):

I'm tempted to merge right away, but it would be nice to read @Joseph Myers's opinion first.

Yury G. Kudryashov (Oct 18 2020 at 19:31):

And wait for the CI

Yury G. Kudryashov (Oct 18 2020 at 19:31):

BTW, I'm working on affine_equiv

Patrick Massot (Oct 18 2020 at 19:31):

bors will wait for CI anyway

Joseph Myers (Oct 18 2020 at 20:34):

Any of those notations seem fine to me (hoping the notation for affine_equiv is consistent with that for affine_map).

Patrick Massot (Oct 18 2020 at 20:35):

It's sold then!

Eric Wieser (Oct 18 2020 at 20:52):

As someone reading this on android, any tips for working out the symbol being proposed here (and other unicode-heavy messages)? Both the github page and zulip seem unaware of these unicode characters!

Yury G. Kudryashov (Oct 18 2020 at 20:57):

I really dislike the fact that Android doesn't let me easily install a more unicode-friendly system font.

Yury G. Kudryashov (Oct 18 2020 at 20:59):

Here is item 3 in $\LaTeX$ : $P_1\to^a[k]P_2$

Eric Wieser (Oct 18 2020 at 21:11):

Ah, just the monospace font is lacking, I can recover it (→ᵃ[ℝ]) through copy paste

Eric Wieser (Oct 18 2020 at 21:12):

Can you elaborate on mul_semiring_action_hom? Is it identical to alg_hom, or is it weaker?

Eric Wieser (Oct 18 2020 at 21:15):

And can/should docs#distrib_mul_action_hom` replace docs#linear_map?

Mario Carneiro (Oct 18 2020 at 21:17):

not with a name like that

Eric Wieser (Oct 18 2020 at 21:26):

Well, can one be an abbreviation of/ extend the other so that they're at least defeq?

Yury G. Kudryashov (Oct 18 2020 at 21:31):

Bad name is the main reason why I haven't redefined linear_map to be distrib_mul_action_hom yet.

Yury G. Kudryashov (Oct 19 2020 at 17:16):

affine equivs: #2909

Last updated: Dec 20 2023 at 11:08 UTC