Effect of changing the base field on span

Stream: Is there code for X?

[Patrick Lutz]

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]

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]

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]

Again, we need to generalize is_algebra_tower to is_scalar_tower

[Patrick Lutz]

@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]

Kenny Lau said:

Again, we need to generalize is_algebra_tower to is_scalar_tower

Thanks! That's helpful to know.

[Patrick Lutz]

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

[Thomas Browning]

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]

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]

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]

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

[Kenny Lau]

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]

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]

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

[Patrick Lutz]

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

[Kevin Buzzard]

@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]

#3717 created.