Zulip Chat Archive

Stream: Is there code for X?

Topic: extension of scalars


view this post on Zulip Kenny Lau (Oct 24 2020 at 16:58):

A:RAlg,M:RModARM:AModA : R-Alg, M : R-Mod \vdash A \otimes_R M : A-Mod

view this post on Zulip Kenny Lau (Oct 24 2020 at 16:58):

if AA is an RR-algebra and MM is an RR-module then ARMA \otimes_R M is an AA-module

view this post on Zulip Reid Barton (Oct 24 2020 at 17:10):

AFAIK, nothing has changed since https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/base.20change.20of.20module/near/208897020

view this post on Zulip Reid Barton (Oct 24 2020 at 17:10):

except that I've been slowly working on the case of localizations

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:18):

we can't even state that theorem if A is a non-commutative algebra, right, as we dont have modules over non-commutative rings?

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 17:18):

It looks like my "eew, is_subring" comment is no longer valid, which is at least some progress.

view this post on Zulip Reid Barton (Oct 24 2020 at 17:19):

Eric Wieser said:

we can't even state that theorem if A is a non-commutative algebra, right, as we dont have modules over non-commutative rings?

In my version of the question, I was quite careful to avoid describing exactly what sorts of things RR and SS were :upside_down:

view this post on Zulip Johan Commelin (Oct 24 2020 at 17:26):

Kenny Lau said:

if AA is an RR-algebra and MM is an RR-module then ARMA \otimes_R M is an AA-module

See the flat-module branch


Last updated: May 07 2021 at 23:11 UTC