## Stream: maths

### Topic: module.restrict_scalars

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

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

#### Nicolò Cavalleri (Aug 16 2020 at 16:08):

Yes I completely agree! I believe restrict_scalars is very painful

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

#### Adam Topaz (Aug 16 2020 at 16:25):

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

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

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

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

#### Kenny Lau (Aug 17 2020 at 19:25):

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

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

#### Nicolò Cavalleri (Aug 17 2020 at 21:48):

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

#### Johan Commelin (Aug 18 2020 at 03:40):

I think you both agree with each other (-;

#### Nicolò Cavalleri (Aug 18 2020 at 08:53):

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

#### Kenny Lau (Aug 18 2020 at 09:06):

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

#### Kenny Lau (Aug 18 2020 at 09:06):

I guess I was taking it out of context

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