restrict_scalars vs enrich_scalars

Stream: general

[Oliver Nash]

I just opened #7807 in which I propose adding a trivial (but useful!) equiv. While I was there I decided to update a doc string and as a result of writing it I now wonder if we could save some confusion by renaming what we currently call restrict_scalars to enrich_scalars.

[Oliver Nash]

Here's the relevant doc string:

/-- A type synonym representing the functor from the category of modules over `A`, regarded as a
(semi)ring, to the category of modules over `A`, regarded as an `R`-algebra.

Warning: use this type synonym judiciously! Often what one wants instead of `restrict_scalars` is
actually the following setup:
`[comm_semiring R] [semiring A] [algebra R A] [module R M] [module A M] [is_scalar_tower R A M]` (*)
which is just the way of saying "let `M` be a module over the `R`-algebra `A`".

Mathematically, when `A` is an `R`-algebra, there are two different functors:
 1. The functor from the category of modules over the (semi)ring `A` to the category of modules over
    the `R`-algebra `A`. This is what is defined here, and is called `restrict_scalars` (though
    perhaps a better name would be `enrich_scalars`).
 2. The functor from the category of modules over the `R`-algebra `A` to the category of modules
    over the (semi)ring `R`. This is the true restriction of scalars but when one uses the setup (*)
    above, it is invisible functor available for free through typeclass inference.

A standard example of when one might want to invoke 1 would be if one has a vector space over a
field of characteristic zero and wishes to make use of the `ℚ`-algebra structure. -/
@[nolint unused_arguments]
def restrict_scalars (R A M : Type*) : Type* := M

[Eric Wieser]

Just to make things more confusing, I think docs#algebra.comap is exactly the same as docs#restrict_scalars

[Eric Wieser]

Or at least, they could be unified into the same type alias, because the structures they confer are defeq

[Oliver Nash]

Yes, it's essentially the same.

[Sebastien Gouezel]

The pojnt of restrict_scalars, as I understand it, is not really to get a module over the R-algebra A, but mainly a module over R. And this operation is commonly called restriction of scalars, right?

[Oliver Nash]

Well I think it depends. What restrict_scalars actually provides is a module over the R-algebra A. Because of how we set things up, once you have a module over an R-algebra A, you can invisibly restrict scalars to get an R-module. However I don't know what the person who invokes it wants until they use it.

[Oliver Nash]

E.g., we could have some theorem somehwere which demands the following: (K L V : Type*) [field K] [field L] [algebra K L] [add_comm_group V] [module K V] [module L V] [is_scalar_tower K L V].

[Oliver Nash]

If we only have [field L] [char_zero L] [add_comm_group V] [module L V] then we can use such a theorem on restrict_scalars ℚ L V.

[Oliver Nash]

So I claim that restrict_scalars is really _enriching_ the scalars.

[Eric Wieser]

It's enriching them with extra typeclasses but restricting them to a type of (usually) smaller cardinality, right?

[Eric Wieser]

I'm a little confused by the discussion above - isn't the whole point of restrict_scalars R A M to provide a module R M instance when only module A M is available?

[Sebastien Gouezel]

I agree that it is enriching the scalars, in the sense that instead of having one scalar field now we have two. But in most cases the new field L is a subfield of the original one K, so the new action consists in forgetting how a bunch of elements act (the ones in K \ L). In this sense, you are forgetting information, and I think that's why is called scalar restriction. In any case, it's standard math terminology, so I don't think it would make sense to change our naming here.

[Oliver Nash]

I absolutely do not want to diverge from standard math terminology. In fact I want to get back to it since I think we are applying it incorrectly in this case and it causes confusion.

[Eric Wieser]

In this sense, you are forgetting information,

well, for [algebra L K] [module K M], the instance module K (restrict_scalars L K M) still exists, so the action of elements in K \ L hasn't been forgotten

[Oliver Nash]

Right!

[Eric Wieser]

Without any mathematical training to ground my interpretation, I read "restrict_scalars R A M" as "provide M with a new action by the restricted "set" R of elements from A"

[Oliver Nash]

I claim that mathematically, the data required to perform restriction of scalars is a module over an algebra. What we currently call restrict_scalars allows us to get this data if somehow (e.g., vector space over field of char 0) we are not explicitly in this situation and want to get there.

[Oliver Nash]

Once we are there, we _may_ then use this data to restrict scalars or we may not.

[Oliver Nash]

Eric Wieser said:

Without any mathematical training to ground my interpretation, I read "restrict_scalars R A M" as "provide M with a new action by the restricted "set" R of elements from A"

I agree with this. If everyone (except me) reads it this way then we're fine as we are.

[Eric Wieser]

I'd note that probably restrict_scalars shouldn't ever appear in a lemma or definition statement, only in a proof / implementation

[Oliver Nash]

Technically I think it could but I agree that is the right rule of thumb.