Torsion and reduction of abelian groups

For n ≠ 0, the n-torsion of a torsion-free abelian group M, such as ℤ, is zero, and the reduction M ⧸ nM = QuotSMulTop n M of a finitely generated abelian group is finite. These are recorded as instances, so that such groups meet the finiteness hypotheses of constructions that take both the n-torsion and the reduction mod n of a ℤ-module.

Main results

• TauCeti.subsingleton_torsionBy_int: the n-torsion of a torsion-free abelian group is zero for n ≠ 0.
• TauCeti.finite_quotSMulTop_int: M ⧸ nM is finite for n ≠ 0 and M finitely generated.
• TauCeti.subsingleton_quotSMulTop_of_surjective_zsmul, TauCeti.subsingleton_torsionBy_of_injective_zsmul: if multiplication by ℓ on V is surjective, respectively injective, then V ⧸ ℓV, respectively V[ℓ], is zero.

instance TauCeti.subsingleton_torsionBy_int (n : ℕ) [NeZero n] (M : Type u_1) [AddCommGroup M] [IsAddTorsionFree M] : Subsingleton ↥(Submodule.torsionBy ℤ M ↑n)

A torsion-free abelian group, such as ℤ, has no nonzero n-torsion for n ≠ 0.

instance TauCeti.finite_quotSMulTop_int (n : ℕ) [NeZero n] (M : Type u_1) [AddCommGroup M] [Module.Finite ℤ M] : Finite (QuotSMulTop (↑n) M)

The reduction M ⧸ nM of a finitely generated abelian group, such as ℤ ⧸ nℤ, is finite for n ≠ 0.

theorem TauCeti.subsingleton_quotSMulTop_of_surjective_zsmul {V : Type u_2} [AddCommGroup V] (ℓ : ℕ) (hV : Function.Surjective fun (x : V) => ↑ℓ • x) : Subsingleton (QuotSMulTop (↑ℓ) V)

If multiplication by ℓ is surjective on V, the reduction V ⧸ ℓV is zero.

theorem TauCeti.subsingleton_torsionBy_of_injective_zsmul {V : Type u_2} [AddCommGroup V] (ℓ : ℕ) (hV : Function.Injective fun (x : V) => ↑ℓ • x) : Subsingleton ↥(Submodule.torsionBy ℤ V ↑ℓ)

If multiplication by ℓ is injective on V, the ℓ-torsion V[ℓ] is zero.