Torsion modules are those killed by localization

A module M over a commutative semiring R is S-torsion, for a submonoid S of R, exactly when its base change A ⊗[R] M to a localization A of R at S vanishes: the base change is a localization of M at S, and an element of M dies there exactly when some element of S kills it. Taking S to be the nonzerodivisors, a module is torsion exactly when its base change to the total ring of fractions vanishes. For abelian groups this is the classical characterization of torsion groups as the groups G with ℚ ⊗ G = 0.

Localizing a torsion module at any submonoid gives a torsion module over the localized ring, since non-zero-divisors stay non-zero-divisors after localization.

For an ideal generated by a finite set G, a module is ideal-power torsion exactly when its localization at every generator is zero. This identifies modules supported on the closed set V(G) without requiring finite generation of the module.

Main results

• Submonoid.isTorsion'_iff_subsingleton_tensorProduct: M is S-torsion if and only if A ⊗[R] M is trivial, for a localization A of R at S.
• TauCeti.Module.isTorsion_iff_subsingleton_tensorProduct: M is torsion if and only if K ⊗[R] M is trivial, for the total ring of fractions K of R.
• TauCeti.isAddTorsion_iff_subsingleton_rat_tensorProduct: an abelian group G is torsion if and only if ℚ ⊗[ℤ] G is trivial.
• Module.IsTorsion.localizedModule: the localization of a torsion module is torsion.
• Ideal.primaryComponent_span_eq_top_iff_subsingleton_localized: ideal-power torsion is detected by vanishing on the complementary principal opens.

theorem Submonoid.isTorsion'_iff_subsingleton_tensorProduct {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] : Module.IsTorsion' M ↥S ↔ Subsingleton (TensorProduct R A M)

A module is S-torsion if and only if its base change to a localization at S is trivial.

theorem TauCeti.Module.isTorsion_iff_subsingleton_tensorProduct {R : Type u_1} [CommSemiring R] (K : Type u_2) [CommSemiring K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommMonoid M] [Module R M] : Module.IsTorsion R M ↔ Subsingleton (TensorProduct R K M)

A module is torsion if and only if its base change to the total ring of fractions is trivial.

theorem TauCeti.isAddTorsion_iff_subsingleton_rat_tensorProduct {G : Type u_1} [AddCommGroup G] : IsAddTorsion G ↔ Subsingleton (TensorProduct ℤ ℚ G)

An abelian group G is torsion if and only if its rationalization ℚ ⊗[ℤ] G is trivial.

theorem Module.IsTorsion.localizedModule {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (hM : IsTorsion R M) (S : Submonoid R) : IsTorsion (Localization S) (LocalizedModule S M)

The localization of a torsion module at a submonoid S is torsion over Localization S.

theorem Ideal.primaryComponent_span_eq_top_iff_subsingleton_localized {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (G : Finset R) : primaryComponent M (span ↑G) = ⊤ ↔ ∀ g ∈ G, Subsingleton (LocalizedModule (Submonoid.powers g) M)

A module is torsion for the ideal generated by a finite set G exactly when its localizations at the generators vanish. The module need not be finitely generated.