Iwasawa

Results named in Tau Ceti's TauCeti.RingTheory.Iwasawa modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe 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).

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

Lean

Formalized in Tau Ceti as TauCeti.Iwasawa.exists_isPseudoIsomorphism_elementary.

Sources

LeanTauCeti.Iwasawa.exists_isPseudoIsomorphism_elementary

Uses 2

Proof usesThe height-one primes of O⟦X⟧ · The structure theorem over a regular local ring of dimension at most two

TheoremThe 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).

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

Lean

Formalized in Tau Ceti as TauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_quotient_pow.

Sources

LeanTauCeti.Iwasawa.exists_isPseudoIsomorphism_pi_quotient_pow

Used by 1

Used byThe structure theorem over a regular local ring of dimension at most two

TheoremThe 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).

TauCeti.Iwasawa.exists_isPseudoIsomorphism_prod_pi_quotient_pow.{u, v} {A : Type u} [CommRing A]
  {M : Type v} [AddCommGroup M] [_root_.Module A M] [IsRegularLocalRing A]
  (hdim : ringKrullDim A ≤ 2) [Module.Finite A M] :
  ∃ r ι x 𝔭 n,
    (∀ (i : ι), (𝔭 i).asIdeal.height = 1 ∧ n i ≠ 0) ∧ ∃ f, TauCeti.Iwasawa.IsPseudoIsomorphism f