Zulip Chat Archive

Stream: maths

Topic: Notation for `affine_map`


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 18 2020 at 18:52):

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

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:24):

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

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:29):

#4675

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:31):

And wait for the CI

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:31):

BTW, I'm working on affine_equiv

view this post on Zulip Patrick Massot (Oct 18 2020 at 19:31):

bors will wait for CI anyway

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Oct 18 2020 at 20:35):

It's sold then!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 20:59):

Here is item 3 in LaTeX\LaTeX: P1a[k]P2P_1\to^a[k]P_2

view this post on Zulip Eric Wieser (Oct 18 2020 at 21:11):

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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Oct 18 2020 at 21:15):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 21:17):

not with a name like that

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 19 2020 at 17:16):

affine equivs: #2909


Last updated: May 09 2021 at 11:09 UTC