Zulip Chat Archive

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 RRR \subset R' are rings, MM is an RR' module and ss generates MM as an RR module then it also generates MM as an RR' 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

Thanks! That's helpful to know.

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: Dec 20 2023 at 11:08 UTC