Zulip Chat Archive

Stream: maths

Topic: module.restrict_scalars


view this post on Zulip Nicolò Cavalleri (Aug 16 2020 at 15:56):

Now that is_scalar_tower is there could it be a good idea to remove module.restrict_scalars from mathlib by substituting it with is_scalar_tower? In abstract lemmas it should be no problem to require two additional instances (one of semimodule and one of is_scalar_tower) and in practical cases, it should be always possible to define such instances: I mean manually defining restrict_scalars and proving there is an instance of is_scalar_tower

view this post on Zulip Anne Baanen (Aug 16 2020 at 16:08):

That sounds like a good idea! I can't think of any disadvantages really: adding one pair of semimodule and is_scalar_tower instances per definition seems less painful than writing out restrict_scalars R A M potentially many times.

view this post on Zulip Nicolò Cavalleri (Aug 16 2020 at 16:08):

Yes I completely agree! I believe restrict_scalars is very painful

view this post on Zulip Nicolò Cavalleri (Aug 16 2020 at 16:09):

In any case I uploaded a compromise of the two things in the derivations PR, and I'd do it as a refactor in another PR in case

view this post on Zulip Adam Topaz (Aug 16 2020 at 16:25):

Wouldn't the construction of the restriction of scalars functor be more annoying without restrict_scalars?

view this post on Zulip Nicolò Cavalleri (Aug 16 2020 at 16:30):

In this case we could probably leave just the definition of it and the bare minimum needed for the functor

view this post on Zulip Adam Topaz (Aug 16 2020 at 16:42):

I don't have any actual opinions on this, but, playing devil's advocate, it might be worthwhile to have some consistency in the API for left/right adjoins in algebra. So while in this case the restriction of scalars functor is just the identity on the underlying type, this will not be the case in all situations. On the other hand, maybe it makes sense to make/use analogues of is_scalar_tower for all forgetful functors.

view this post on Zulip Kenny Lau (Aug 17 2020 at 19:24):

No! module.restrict_scalars is how you make the instance module R M given algebra R S and module S M, and is_scalar_tower R S M is how you prove theorems.

view this post on Zulip Kenny Lau (Aug 17 2020 at 19:25):

cf. the same situation with algebra.comap and is_algebra_tower (now is_scalar_tower)

view this post on Zulip Nicolò Cavalleri (Aug 17 2020 at 21:47):

Sorry can you elaborate further? I am not sure I understand what you support. The point I was trying to make above is that until now, is_scalar_tower was not there and restrict_scalars was used for everything so also "to prove theorems" as you say. The idea is to leave just the definition of restrict scalars so to use it to help making instances but removing any lemma that has to do with it and using is_scalar_tower instead

view this post on Zulip Nicolò Cavalleri (Aug 17 2020 at 21:48):

I mean similar to what I did in the first draft of derivations here in Zulip

view this post on Zulip Johan Commelin (Aug 18 2020 at 03:40):

I think you both agree with each other (-;

view this post on Zulip Nicolò Cavalleri (Aug 18 2020 at 08:53):

Yes this what I also thought but I was confused from the "No!"

view this post on Zulip Kenny Lau (Aug 18 2020 at 09:06):

I was saying "No!" to "remove module.restrict_scalars from mathlib"

view this post on Zulip Kenny Lau (Aug 18 2020 at 09:06):

I guess I was taking it out of context

view this post on Zulip Eric Wieser (Aug 18 2020 at 09:13):

docs#semimodule.restrict_scalars because I'm lazy and someone else might be too


Last updated: May 19 2021 at 00:40 UTC