What are the arrows in `R ⟶ S induces S-Alg ⥤ R-Alg`

Stream: maths

[Eric Wieser]

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]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

Whoops, wrong link, fixed

[Yury G. Kudryashov]

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]

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]

In linear algebra this is called restrict_scalars

[Yury G. Kudryashov]

I think, it should be renamed to alg_hom.restrict_scalars

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

And your new def should be alg_equiv.restrict_scalars.

[Eric Wieser]

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

[Anne Baanen]

I see restrict_base instead of restrict_scalars in #6548?

[Eric Wieser]

Oh, whoops

[Eric Wieser]

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]

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