# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: extension of scalars

#### Kenny Lau (Oct 24 2020 at 16:58):

$A : R-Alg, M : R-Mod \vdash A \otimes_R M : A-Mod$

#### Kenny Lau (Oct 24 2020 at 16:58):

if $A$ is an $R$-algebra and $M$ is an $R$-module then $A \otimes_R M$ is an $A$-module

#### 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

#### Reid Barton (Oct 24 2020 at 17:10):

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

#### 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?

#### 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.

#### 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 $R$ and $S$ were :upside_down:

#### Johan Commelin (Oct 24 2020 at 17:26):

Kenny Lau said:

if $A$ is an $R$-algebra and $M$ is an $R$-module then $A \otimes_R M$ is an $A$-module

See the `flat-module`

branch

Last updated: May 07 2021 at 23:11 UTC