Classification machinery for countable reduced abelian p-groups

This module contains the hard-direction interface for Ulm's theorem: the back-and-forth construction on finite partial isomorphisms and the final isomorphism-from-invariants statement.

Isomorphism-from-equivalences back-and-forth assembly

BFIsoStep is a finite stage carrying an actual AddEquiv (rather than a plain hom). The chain construction below proves iso_of_ulmInvariant_eq_of_backAndForth: given abstract hforth/hback hypotheses that supply BFIsoStep extensions, the colimit is an isomorphism. kaplansky_extend supplies the concrete forth hypothesis, and applying it to the inverse stage supplies the back hypothesis.

@[reducible, inline]

abbrev UlmsTheorem.BFIsoStep (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] : Type u

A finite stage carrying a true partial isomorphism.

Equations

• UlmsTheorem.BFIsoStep p = UlmsTheorem.UlmStage p

theorem UlmsTheorem.iso_of_ulmInvariant_eq_of_backAndForth (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] [Countable G] [Countable H] (hforth : UlmsTheorem.BFForthPolicy✝ p) (hback : UlmsTheorem.BFBackPolicy✝ p) : Nonempty (G ≃+ H)

Back-and-forth assembly: abstract hforth/hback hypotheses for BFIsoStep imply the two groups are isomorphic. Proved in full; no open obligation within.

theorem UlmsTheorem.iso_of_ulmInvariant_eq (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] [Countable G] [Countable H] (hG : IsReducedPGroup p G) (hH : IsReducedPGroup p H) (hinv : ∀ (α : Ordinal.{0}), ulmInvariant p α = ulmInvariant p α) : Nonempty (G ≃+ H)

Hard direction of Ulm's theorem: equal Ulm invariants imply isomorphism, using the proved Kaplansky finite-stage extension in both directions.