## Stream: maths

### Topic: What are the arrows in R ⟶ S induces S-Alg ⥤ R-Alg

#### Eric Wieser (Mar 05 2021 at 15:38):

We currently have docs#is_scalar_tower.restrict_base which is defined as (A →ₐ[S] B) → (algebra.comap R S A →ₐ[R] algebra.comap R S B), and documented as R ⟶ S induces S-Alg ⥤ R-Alg.

I want to add this for alg_equiv in #6548 (defined the obvious way), but I have no ideas what arrows I should be using in the docstring for the new method. Are these the arrows from category_theory?

#### Yury G. Kudryashov (Mar 05 2021 at 15:46):

I see no docstring for docs@is_scalar_tower.comap. The arrows in your quote are indeed from category_theory.

#### Yury G. Kudryashov (Mar 05 2021 at 15:47):

I would prefer to have docstrings readable by people who are not fluent in category theory and its Lean implementation.

#### Yury G. Kudryashov (Mar 05 2021 at 15:49):

I mean, it's OK to mention the category theory interpretation but there should be an actual explanation of the meaning as well.

#### Eric Wieser (Mar 05 2021 at 15:50):

Maybe I'll just stick with "restrict_base but for alg_equiv instead of alg_hom" as my description for the new def

#### Yury G. Kudryashov (Mar 05 2021 at 15:53):

In linear algebra this is called restrict_scalars

#### Yury G. Kudryashov (Mar 05 2021 at 15:53):

I think, it should be renamed to alg_hom.restrict_scalars

#### Yury G. Kudryashov (Mar 05 2021 at 15:54):

Probably the current name is an artifact from the time when we used a type tag instead of [is_scalar_tower]

#### Yury G. Kudryashov (Mar 05 2021 at 15:55):

And your new def should be alg_equiv.restrict_scalars.

#### Eric Wieser (Mar 05 2021 at 16:02):

The names you suggest are exactly what the PR already renames them to :)

#### Anne Baanen (Mar 05 2021 at 16:20):

I see restrict_base instead of restrict_scalars in #6548?

Oh, whoops

#### Eric Wieser (Mar 05 2021 at 16:26):

I'll look at the docstring for docs#linear_map.restrict_scalars for inspiration on what to use as documentation instead of the arrows

#### Eric Wieser (Mar 05 2021 at 16:35):

Updated the PR to use the name restrict_scalars thanks for pointing out my blindness to the difference in name

Last updated: May 14 2021 at 20:13 UTC