Splitting off the torsion submodule up to pseudo-isomorphism

Let A be a noetherian integrally closed domain and M a finitely generated A-module with torsion submodule T = torsion A M. The exact sequence 0 → T → M → M ⧸ T → 0 need not split, but it splits up to pseudo-isomorphism: there is a linear map φ : M → T such that m ↦ (φ m, m mod T) is a pseudo-isomorphism M → T × M ⧸ T. This reduces the structure theory of finitely generated modules over such rings, and in particular over the Iwasawa algebra Λ = O⟦T⟧, to the torsion and the torsion-free cases separately.

The proof is local at the finitely many primes of height one in the support of T. At such a prime 𝔭 the ring A_𝔭 is a discrete valuation ring, so the finitely generated torsion-free module (M ⧸ T)_𝔭 is free and the localized sequence splits. Its splitting descends to a map φ : M → T restricting to multiplication by some s ∉ 𝔭 on T, and by prime avoidance one s works at every such prime. The final step is TauCeti.Iwasawa.isPseudoIsomorphism_prod_mkQ: if φ : M → N restricts to multiplication by a on a finitely generated submodule N, then (φ, mod N) is a pseudo-isomorphism once a lies in no prime of height at most one in the support of N.

Main results

• TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_torsion_mkQ: over a noetherian integrally closed domain, a finitely generated module M admits a pseudo-isomorphism M → torsion A M × M ⧸ torsion A M whose second component is the quotient map.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (5.1.7) and Remarks 1–2 after it.

theorem TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_torsion_mkQ {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] [Module.Finite A M] : ∃ (φ : M →ₗ[A] ↥(Submodule.torsion A M)), IsPseudoIsomorphism (φ.prod (Submodule.torsion A M).mkQ)

Splitting off the torsion submodule. Over a noetherian integrally closed domain A, a finitely generated module M admits a pseudo-isomorphism M → torsion A M × M ⧸ torsion A M whose second component is the quotient map. Neukirch–Schmidt–Wingberg, (5.1.7).