The free quotient of a module containing a lattice of finite index

Let R be a principal ideal domain and M an R-module. Suppose that a free module R^ι of finite rank embeds into M with cokernel of finite exponent: some nonzero r ∈ R carries all of M into the image. Then M modulo its torsion is free of rank #ι, that is M ⧸ torsion R M ≃ R^ι. No finiteness of M is assumed: multiplication by r embeds M ⧸ torsion R M into R^ι, which already makes it finitely generated.

This is how the rank of a module is computed from an explicit lattice of finite index, for instance the rank [L : ℚ_p] + 1 of the p-adic completion of the multiplicative group of a p-adic field from the logarithm on its deep units.

Main results

• TauCeti.nonempty_quotient_torsion_linearEquiv_of_injective_of_smul_mem_range: if f : R^ι → M is injective and r • M ⊆ range f for some r ≠ 0, then M ⧸ torsion R M ≃ R^ι.

theorem TauCeti.nonempty_quotient_torsion_linearEquiv_of_injective_of_smul_mem_range {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] [Finite ι] {f : (ι → R) →ₗ[R] M} (hf : Function.Injective ⇑f) {r : R} (hr : r ≠ 0) (hrf : ∀ (x : M), r • x ∈ f.range) : Nonempty ((M ⧸ Submodule.torsion R M) ≃ₗ[R] ι → R)

Over a principal ideal domain R, if an injective linear map f : R^ι → M has cokernel killed by some nonzero r ∈ R, then M modulo its torsion is free on ι.