## Stream: Is there code for X?

### Topic: Effect of changing the base field on span

#### Patrick Lutz (Aug 06 2020 at 17:10):

Is there anything in mathlib saying something like the following? If $R \subset R'$ are rings, $M$ is an $R'$ module and $s$ generates $M$ as an $R$ module then it also generates $M$ as an $R'$ module.

#### Kevin Buzzard (Aug 06 2020 at 22:28):

Do you want R' to be an R-algebra or do you want R to be a subring of R'? Do you want to not be asked that question :-/

#### Patrick Lutz (Aug 06 2020 at 22:36):

Kevin Buzzard said:

Do you want R' to be an R-algebra or do you want R to be a subring of R'? Do you want to not be asked that question :-/

Either way might be okay.

#### Kenny Lau (Aug 06 2020 at 23:54):

Again, we need to generalize is_algebra_tower to is_scalar_tower

#### Patrick Lutz (Aug 07 2020 at 01:46):

@Thomas Browning What do you think about this? Maybe we should work on this? We need something like it to prove the primitive element theorem I think (and probably for other stuff we'll want to do).

#### Patrick Lutz (Aug 07 2020 at 01:46):

Kenny Lau said:

Again, we need to generalize is_algebra_tower to is_scalar_tower

#### Patrick Lutz (Aug 07 2020 at 01:49):

Actually, if I understand this thread, this is already being worked on? Is that correct?

#### Thomas Browning (Aug 07 2020 at 01:52):

Patrick Lutz said:

Thomas Browning What do you think about this? Maybe we should work on this? We need something like it to prove the primitive element theorem I think (and probably for other stuff we'll want to do).

It doesn't sound too hard to bash this directly, but I could be wrong. If you can isolate the result that we need, then I'll take a stab at it.

#### Anne Baanen (Aug 07 2020 at 08:57):

Since @Nicolò Cavalleri also needs is_scalar_tower for #3688 and asked my help, I can take a stab at is_scalar_tower right now.

#### Anne Baanen (Aug 07 2020 at 08:59):

My plan: introduce is_scalar_tower G M N as a typeclass with a field smul_assoc : ∀ (x : R) (y : M) (z : N), (x • y) • z = x • (y • z), then define is_algebra_tower as an abbreviation (along the lines of semimodule vs. module vs. vector_space).

#### Anne Baanen (Aug 07 2020 at 09:01):

Is there an instance that people would like to see in the PR, or just introduce the typeclass?

#### Kenny Lau (Aug 07 2020 at 09:04):

Patrick Lutz said:

Actually, if I understand this thread, this is already being worked on? Is that correct?

nah I always say it needs to be done but then I never 'ave the time to do it

#### Kenny Lau (Aug 07 2020 at 09:04):

Anne Baanen said:

Is there an instance that people would like to see in the PR, or just introduce the typeclass?

I think you can look at the instances in algbera_tower

#### Kenny Lau (Aug 07 2020 at 09:04):

but I guess you could also just introduce the typeclass and let other people fill in the instances

#### Patrick Lutz (Aug 07 2020 at 09:11):

By the way, for now, Thomas has proved the case of this that we actually needed at the moment.

#### Kevin Buzzard (Aug 07 2020 at 09:57):

@Anne Baanen I think this typeclass offers a solution to the problem I whinged about in the very long "algebra is not scaling for me" thread

#### Anne Baanen (Aug 07 2020 at 10:15):

#3717 created.

Last updated: May 16 2021 at 05:21 UTC