Zulip Chat Archive

Stream: Is there code for X?

Topic: Effect of changing the base field on span


view this post on Zulip 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.

view this post on Zulip 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 :-/

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 06 2020 at 23:54):

Again, we need to generalize is_algebra_tower to is_scalar_tower

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Lutz (Aug 07 2020 at 01:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anne Baanen (Aug 07 2020 at 10:15):

#3717 created.


Last updated: May 16 2021 at 05:21 UTC