The structure theorem up to pseudo-isomorphism

Let A be a noetherian integrally closed domain. A finitely generated torsion A-module M admits a pseudo-isomorphism M → ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ onto a finite product of quotients by powers of height-one primes, with every nᵢ positive. Over a regular local ring of dimension at most two, such as the Iwasawa algebra Λ = O⟦T⟧, every finitely generated module M admits a pseudo-isomorphism M → Aʳ × ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ. This is the existence half of the structure theorem for finitely generated modules over such rings; it is the form in which the theorem feeds the structure theory of Iwasawa modules, where the height-one primes of O⟦T⟧ are (ϖ) and the ideals generated by irreducible distinguished polynomials.

The torsion case is local at the finitely many primes of height one in the support of M. At such a prime 𝔭 the ring A_𝔭 is a discrete valuation ring, so the structure theorem over a principal ideal domain decomposes M_𝔭 as a sum of quotients A_𝔭 ⧸ (𝔭 A_𝔭) ^ k; these are the localizations of the A ⧸ 𝔭 ^ k, and the isomorphism lifts to a map ∏ A ⧸ 𝔭 ^ k → M that is bijective at 𝔭. Summing these maps over the primes gives a pseudo-isomorphism onto M, since the factor belonging to 𝔭 vanishes at every other prime of height at most one. Pseudo-isomorphisms onto torsion modules can be reversed. The general case over a regular local ring of dimension at most two combines this with the splitting off of the torsion submodule and the reflexive hull of the torsion-free quotient.

Main results

• TauCeti.Iwasawa.exists_bijective_localizedModule_map_pi_quotient_pow: at a prime 𝔭 of height one, a finitely generated torsion module M receives a map from some ∏ᵢ A ⧸ 𝔭 ^ nᵢ that is bijective after localizing at 𝔭.
• TauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_quotient_pow: over a noetherian integrally closed domain, a finitely generated torsion module admits a pseudo-isomorphism to ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ with each 𝔭ᵢ of height one and each nᵢ positive.
• TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_pi_quotient_pow: over a regular local ring of dimension at most two, a finitely generated module admits a pseudo-isomorphism to Aʳ × ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (5.1.7)–(5.1.10).
• N. Bourbaki, Commutative Algebra, Chapter VII, §4.4, Theorem 5.

theorem TauCeti.Iwasawa.exists_bijective_localizedModule_map_pi_quotient_pow {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] [Module.Finite A M] (hM : Module.IsTorsion A M) {𝔭 : Ideal A} [𝔭.IsPrime] (h𝔭 : 𝔭.height = 1) : ∃ (ι : Type u) (x : Fintype ι) (n : ι → ℕ) (h : ((i : ι) → A ⧸ 𝔭 ^ n i) →ₗ[A] M), Function.Bijective ⇑((LocalizedModule.map 𝔭.primeCompl) h)

Elementary divisors at a height-one prime. Let A be a noetherian integrally closed domain and 𝔭 a prime of height one. A finitely generated torsion module M receives a linear map from a finite product ∏ᵢ A ⧸ 𝔭 ^ nᵢ that becomes bijective after localizing at 𝔭.

theorem TauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_quotient_pow {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] [Module.Finite A M] (hM : Module.IsTorsion A M) : ∃ (ι : Type u) (x : Fintype ι) (𝔭 : ι → PrimeSpectrum A) (n : ι → ℕ), (∀ (i : ι), (𝔭 i).asIdeal.height = 1 ∧ n i ≠ 0) ∧ ∃ (f : M →ₗ[A] (i : ι) → A ⧸ (𝔭 i).asIdeal ^ n i), IsPseudoIsomorphism f

The structure theorem for torsion modules. Over a noetherian integrally closed domain A, a finitely generated torsion module M admits a pseudo-isomorphism M → ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ onto a finite product, with each 𝔭ᵢ a prime of height one and each nᵢ positive. Neukirch–Schmidt–Wingberg, (5.1.10).

theorem TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_pi_quotient_pow {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) [Module.Finite A M] : ∃ (r : ℕ) (ι : Type u) (x : Fintype ι) (𝔭 : ι → PrimeSpectrum A) (n : ι → ℕ), (∀ (i : ι), (𝔭 i).asIdeal.height = 1 ∧ n i ≠ 0) ∧ ∃ (f : M →ₗ[A] (Fin r → A) × ((i : ι) → A ⧸ (𝔭 i).asIdeal ^ n i)), IsPseudoIsomorphism f

The structure theorem over a regular local ring of dimension at most two. Let A be a regular local ring of dimension at most two, such as the Iwasawa algebra O⟦T⟧. A finitely generated A-module M admits a pseudo-isomorphism M → Aʳ × ∏ᵢ A ⧸ 𝔭ᵢ ^ nᵢ, with each 𝔭ᵢ a prime of height one and each nᵢ positive. Neukirch–Schmidt–Wingberg, Theorem (5.1.10).