extension of scalars

Stream: Is there code for X?

[Kenny Lau]

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

[Kenny Lau]

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

[Reid Barton]

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]

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

[Eric Wieser]

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]

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

[Reid Barton]

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]

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