Torsion in tensor products

An annihilator of either factor annihilates its tensor product with an arbitrary module. Similarly, the tensor product of commutative additive monoids is torsion if either factor is torsion. No flatness or finite generation is required. These facts supply the tensor closure properties used in Hurewicz theorems modulo a class of abelian groups.

If an ideal I kills one factor and the other factor X satisfies I • X = X, the tensor product vanishes. This is how modules killed by an idempotent ideal m are seen to be killed by m ⊗ - in almost mathematics.

For an ideal I of R and an R-algebra S, scalar extension sends I-power torsion to IS-power torsion, where IS is the extended ideal I.map (algebraMap R S): if J kills m, then JS kills 1 ⊗ m. Conversely, for finitely generated I, flat scalar extension of a module without I-power torsion has no IS-power torsion.

References

• J.-P. Serre, Groupes d'homotopie et classes de groupes abéliens, Ann. of Math. 58 (1953).
• O. Gabber, L. Ramero, Almost ring theory, Lecture Notes in Math. 1800, Springer (2003), Remark 2.1.4(i).

theorem TauCeti.isTorsionBy_tensorProduct_left {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] {r : S} (h : Module.IsTorsionBy S M r) : Module.IsTorsionBy S (TensorProduct R M N) r

An annihilator for a commuting scalar action on the left factor annihilates the tensor product. This includes integer annihilators of modules over any commutative ring.

theorem TauCeti.isTorsionBy_tensorProduct_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {S : Type u_4} [Semiring S] [Module S M] [Module S N] [SMulCommClass R S M] [TensorProduct.CompatibleSMul R S M N] {r : S} (h : Module.IsTorsionBy S N r) : Module.IsTorsionBy S (TensorProduct R M N) r

An annihilator of the right factor annihilates the tensor product when the scalar action can be moved between its factors.

theorem TauCeti.isAddTorsion_tensorProduct_left {R : Type u_1} [CommSemiring R] {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] (h : IsAddTorsion A) : IsAddTorsion (TensorProduct R A B)

Tensoring a torsion commutative additive monoid on the left with any commutative additive monoid gives a torsion monoid.

theorem TauCeti.isAddTorsion_tensorProduct_right {R : Type u_1} [CommSemiring R] {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] (h : IsAddTorsion B) : IsAddTorsion (TensorProduct R A B)

Tensoring a torsion commutative additive monoid on the right with any commutative additive monoid gives a torsion monoid.

theorem TauCeti.subsingleton_tensorProduct_of_isTorsionBySet_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {I : Ideal R} (hM : I • ⊤ = ⊤) (hN : Module.IsTorsionBySet R N ↑I) : Subsingleton (TensorProduct R M N)

If I • X = X and I kills K, then X ⊗ K = 0: for i ∈ I one has (i • x) ⊗ k = x ⊗ (i • k) = 0.

theorem TauCeti.subsingleton_tensorProduct_of_isTorsionBySet_left {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {I : Ideal R} (hM : Module.IsTorsionBySet R M ↑I) (hN : I • ⊤ = ⊤) : Subsingleton (TensorProduct R M N)

If I kills M and I • X = X, then M ⊗ X = 0.

theorem TauCeti.map_le_torsionOf_one_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_3} [AddCommGroup M] [Module R M] {J : Ideal R} {m : M} (hm : m ∈ Submodule.torsionBySet R M ↑J) : Ideal.map (algebraMap R S) J ≤ Ideal.torsionOf S (TensorProduct R S M) (1 ⊗ₜ[R] m)

If an ideal J kills m, then the extended ideal JS kills 1 ⊗ m.

theorem TauCeti.one_tmul_mem_primaryComponent_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} {M : Type u_3} [AddCommGroup M] [Module R M] {m : M} (hm : m ∈ Ideal.primaryComponent M I) : 1 ⊗ₜ[R] m ∈ Ideal.primaryComponent (TensorProduct R S M) (Ideal.map (algebraMap R S) I)

Base change sends I-power torsion elements to IS-power torsion elements.

theorem TauCeti.primaryComponent_map_tensorProduct_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} {M : Type u_3} [AddCommGroup M] [Module R M] (hM : Ideal.primaryComponent M I = ⊤) : Ideal.primaryComponent (TensorProduct R S M) (Ideal.map (algebraMap R S) I) = ⊤

The base change of an I-power torsion module is IS-power torsion.

theorem TauCeti.primaryComponent_map_tensorProduct_eq_bot {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} {M : Type u_3} [AddCommGroup M] [Module R M] [Module.Flat R S] (hI : I.FG) (hM : Ideal.primaryComponent M I = ⊥) : Ideal.primaryComponent (TensorProduct R S M) (Ideal.map (algebraMap R S) I) = ⊥

Flat base change of a module without I-power torsion has no IS-power torsion, for finitely generated I.