Zulip Chat Archive

Stream: maths

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


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

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

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

view this post on Zulip Eric Wieser (Mar 05 2021 at 15:49):

Whoops, wrong link, fixed

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

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

view this post on Zulip Yury G. Kudryashov (Mar 05 2021 at 15:53):

In linear algebra this is called restrict_scalars

view this post on Zulip Yury G. Kudryashov (Mar 05 2021 at 15:53):

I think, it should be renamed to alg_hom.restrict_scalars

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

view this post on Zulip Yury G. Kudryashov (Mar 05 2021 at 15:55):

And your new def should be alg_equiv.restrict_scalars.

view this post on Zulip Eric Wieser (Mar 05 2021 at 16:02):

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

view this post on Zulip Anne Baanen (Mar 05 2021 at 16:20):

I see restrict_base instead of restrict_scalars in #6548?

view this post on Zulip Eric Wieser (Mar 05 2021 at 16:22):

Oh, whoops

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

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