Finiteness properties under localization #
In this file we establish behaviour of Module.Finite
under localizations.
Main results #
Module.Finite.of_isLocalizedModule
: IfM
is a finiteR
-module,S
is a submonoid ofR
,Rₚ
is the localization ofR
atS
andMₚ
is the localization ofM
atS
, thenMₚ
is a finiteRₚ
-module.Module.Finite.of_localizationSpan_finite
: IfM
is anR
-module and{ r }
is a finite set generating the unit ideal such thatMᵣ
is a finiteRᵣ
-module for eachr
, thenM
is a finiteR
-module.
If there exists a finite set { r }
of R
such that Mᵣ
is Rᵣ
-finite for each r
,
then M
is a finite R
-module.
General version for any modules Mᵣ
and rings Rᵣ
satisfying the correct universal properties.
See Module.Finite.of_localizationSpan_finite
for the specialized version.
See of_localizationSpan'
for a version without the finite set assumption.
If there exists a set { r }
of R
such that Mᵣ
is Rᵣ
-finite for each r
,
then M
is a finite R
-module.
General version for any modules Mᵣ
and rings Rᵣ
satisfying the correct universal properties.
See Module.Finite.of_localizationSpan_finite
for the specialized version.
If there exists a finite set { r }
of R
such that Mᵣ
is Rᵣ
-finite for each r
,
then M
is a finite R
-module.
See of_localizationSpan
for a version without the finite set assumption.
If there exists a set { r }
of R
such that Mᵣ
is Rᵣ
-finite for each r
,
then M
is a finite R
-module.