Skip to content

Iwasawa modules

Generic pseudo-null and directional pseudo-isomorphism calculus and the RingCat finite-quotient completed group algebra, topology, Hausdorffness, compactness and compact-route canonical-uniformity completeness.

Quoted from the project description in formalization.yaml of FormalFrontier/iwasawa-modules at commit e71db96b, Apache-2.0.

1 article: 1 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/iwasawa-modules, read at commit e71db96b (2026-11-04).
  • Lean toolchain v4.34.0-rc2, Mathlib at e37d88a2.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “independently reviewed published foundation; successor candidates require exact review”.
  • Review notes: “Prism, Atlas, Lattice and Anchor reviewed earlier original mathematical contributions. Separate independent reviews addressed the original development and subsequent published snapshots. Each successor requires its own exact-candidate review and applicable build and complete transitive standard-axiom evidence, including private and generated declarations. Schema validity or public API documentation alone is not acceptance.”
  • Reviewers: “Prism, Atlas, Lattice and Anchor (historical individual mathematical contributions)”, “Independent Formal Frontier reviewers (development and published-release candidates)”.
  • Automation: agent; framework “AI-assisted Lean authoring with pinned Lake and mathlib”; tool setup “Beacon's original bridges, native-module and lint contributions; independently contributed public clients and metadata. The default build checks production and test roots with pinned Lean/mathlib. Separately retained native doc-gen4 SQLite/raw-record runs supplied the eleven-module API catalogue, not a private-proof census.”; prompting notes “AI agents assisted with original construction, proof search, module migration, testing and documentation. Human/operator authorization for verified original project contributions does not assign copyright ownership or clear third-party reuse.”
  • Automation notes: “Mathematical and module/test contributions received independent review. The adapted native-documentation generator draws on the finite-group Tate cohomology, polynomial-root-stability and Anchor ideal-completion adapters; expression credit and the bounds of public API documentation are explained in docs/README.md. Exact release decisions are recorded separately.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Original Formal Frontier bridge definitions and proofs for Iwasawa modules, Beacon, IwasawaModules/PseudoIsomorphism and IwasawaModules/CompletedGroupAlgebra (original-proof; independently-proves).
  • mathlib4, Lean community contributors (software library; background).
  • Cohomology of Number Fields, Jürgen Neukirch, Alexander Schmidt, Kay Wingberg, Chapter V, sections 1, 3 and 5 (book; background).

Builds on

No other Formal Frontier library.

Headline results

Quoted from the headline results in README.md of FormalFrontier/iwasawa-modules at commit e71db96b, Apache-2.0.

DefinitionPseudo-nullity and short exact sequences#

Over any commutative ring, Module.IsPseudoNull says a module's support avoids primes of height at most one; equivalently, each such localization vanishes. Submodules, quotients and extensions preserve pseudo-nullity, and in a short exact sequence the middle term is pseudo-null exactly when both endpoints are (exact-sequence criterion). The predicate needs no finite-generation, Noetherianity or domain hypothesis.

Quoted from the headline results in README.md of FormalFrontier/iwasawa-modules at commit e71db96b, Apache-2.0.

Lean

Read from the source at commit e71db96b, without running Lean.

Sources
LeanModule.IsPseudoNull

Directional map calculus. A specified linear map has pseudo-null kernel and cokernel exactly when it is bijective after localization at every prime of height at most one. Identity and bijective maps qualify; composition preserves the predicate, with independent scalar and module universes. This gives no unrestricted reverse arrow or symmetric relation.

Completed group algebra. For a commutative coefficient ring R and a profinite group G, CompletedGroupAlgebra R G is the finite-quotient group-algebra limit in RingCat, so G need not be commutative. Its coordinate projections are compatible and detect equality; the canonical ring map from R[G] has a coordinate formula. No injectivity or density of this map is asserted.

Coefficientwise topology and separation. For any finite index type, even an empty one, coefficient extraction is a homeomorphism with a finite product; this part needs no group structure. The completed topology is induced by finite-quotient projections: a map into the completion is continuous iff each coordinate is. Hausdorff coefficients give finite-level and completed Hausdorff spaces. Multiplicative/topological-ring results retain their group and ring-continuity hypotheses.

Compact-route completeness. Finite-index coefficient spaces are compact over compact coefficients without a Hausdorff or topological-ring assumption. Finite-level completeness for canonical additive-group uniformity additionally needs a topological ring. Completed compactness and completed completeness by this route need compact and Hausdorff topological-ring coefficients; merely complete coefficients are not covered.

These noncomputable constructions also include the zero coefficient ring. Compact-module structure, Z_p[[Gamma]] comparisons, Iwasawa structure and invariants, growth, adjoints and full source coverage remain outside this library. The native API reference gives signatures and further declarations.

Main results

Its formalization.yaml lists 4 main results, and the scan finds 4 of them declared in the file the yaml gives; they are on their own page, not made articles.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.