Finiteness of tensor products over a larger scalar ring #
Let S be an R-algebra, M a finite S-module and N a finite R-module. Then M ⊗[R] N,
with S acting through M, is a finite S-module. This is the finiteness counterpart of
Mathlib's Module.Free.tensor; Mathlib's Module.Finite.tensorProduct is the case S = R and
Module.Finite.base_change the case M = S.
Main results #
Module.Finite.tensor:M ⊗[R] Nis finite overS.
instance
Module.Finite.tensor
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
[AddCommMonoid N]
[Module R N]
[Module.Finite S M]
[Module.Finite R N]
:
Module.Finite S (TensorProduct R M N)
The tensor product of a finite S-module with a finite R-module is a finite S-module.