## 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.

#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).

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: May 09 2021 at 11:09 UTC