module.restrict_scalars

Stream: maths

[Nicolò Cavalleri]

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]

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]

Yes I completely agree! I believe restrict_scalars is very painful

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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

[Adam Topaz]

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]

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]

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

[Nicolò Cavalleri]

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]

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

[Johan Commelin]

I think you both agree with each other (-;

[Nicolò Cavalleri]

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

[Kenny Lau]

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

[Kenny Lau]

I guess I was taking it out of context

[Eric Wieser]

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