The structure theorem for Iwasawa modules

Let O be a discrete valuation ring with uniformiser ϖ, complete for its maximal ideal, and let Λ = O⟦X⟧ be the Iwasawa algebra over O. An elementary Λ-module is a module Λʳ × ∏ᵢ Λ ⧸ (ϖ ^ mᵢ) × ∏ⱼ Λ ⧸ (Fⱼ ^ nⱼ) with each Fⱼ an irreducible distinguished polynomial. Every finitely generated Λ-module admits a pseudo-isomorphism, that is a map with finite kernel and cokernel when the residue field of O is finite, onto an elementary module. The vertical factors are powers of the uniformiser ϖ, not of p, which matters when O is ramified over ℤ_p.

This specialises the structure theorem over a regular local ring of dimension two (TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_pi_quotient_pow) to Λ, whose height-one primes are (ϖ) and the ideals (F) with F irreducible and distinguished (PowerSeries.height_eq_one_iff_of_isDiscreteValuationRing). In terms of the elementary module, the Iwasawa invariants of a torsion module are μ = Σ mᵢ and λ = Σ nⱼ deg Fⱼ, and its characteristic polynomial is ∏ Fⱼ ^ nⱼ.

Main definitions

• TauCeti.Iwasawa.Elementary O ϖ r m F n: the elementary module O⟦X⟧ʳ × ∏ᵢ O⟦X⟧ ⧸ (ϖ ^ mᵢ) × ∏ⱼ O⟦X⟧ ⧸ (Fⱼ ^ nⱼ).

Main results

• TauCeti.Iwasawa.exists_isPseudoIsomorphism_elementary: every finitely generated O⟦X⟧-module admits a pseudo-isomorphism onto an elementary module, with every exponent positive and every Fⱼ irreducible and distinguished.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, Theorem (5.3.8).
• L. Washington, Introduction to Cyclotomic Fields, second edition, GTM 83, Theorem 13.12.

@[reducible, inline]

abbrev TauCeti.Iwasawa.Elementary (O : Type u_1) [CommRing O] (ϖ : O) (r : ℕ) {a b : ℕ} (m : Fin a → ℕ) (F : Fin b → Polynomial O) (n : Fin b → ℕ) : Type u_1

The elementary O⟦X⟧-module O⟦X⟧ʳ × ∏ᵢ O⟦X⟧ ⧸ (ϖ ^ mᵢ) × ∏ⱼ O⟦X⟧ ⧸ (Fⱼ ^ nⱼ), with vertical factors indexed by Fin a and horizontal factors indexed by Fin b.

theorem TauCeti.Iwasawa.exists_isPseudoIsomorphism_elementary {O : Type u_1} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] {ϖ : O} {M : Type u_2} [AddCommGroup M] [Module (PowerSeries O) M] (hϖ : Irreducible ϖ) [Module.Finite (PowerSeries O) M] : ∃ (r : ℕ) (a : ℕ) (b : ℕ) (m : Fin a → ℕ) (F : Fin b → Polynomial O) (n : Fin b → ℕ), (∀ (i : Fin a), m i ≠ 0) ∧ (∀ (j : Fin b), (F j).IsDistinguishedAt (IsLocalRing.maximalIdeal O) ∧ Irreducible (F j) ∧ n j ≠ 0) ∧ ∃ (f : M →ₗ[PowerSeries O] Elementary O ϖ r m F n), IsPseudoIsomorphism f

The structure theorem for Iwasawa modules. Let O be a discrete valuation ring with uniformiser ϖ, complete for its maximal ideal. Every finitely generated O⟦X⟧-module admits a pseudo-isomorphism onto an elementary module O⟦X⟧ʳ × ∏ᵢ O⟦X⟧ ⧸ (ϖ ^ mᵢ) × ∏ⱼ O⟦X⟧ ⧸ (Fⱼ ^ nⱼ) with every mᵢ and nⱼ positive and every Fⱼ irreducible and distinguished. Neukirch–Schmidt–Wingberg, Theorem (5.3.8).