Ulm's theorem

Public entry point for the Ulm-theorem track of the project.

theorem UlmsTheorem.ulm_invariants_of_iso (p : ℕ) [hp : Fact (Nat.Prime p)] {G H : Type u} [AddCommGroup G] [AddCommGroup H] (hiso : Nonempty (G ≃+ H)) (α : Ordinal.{0}) : ulmInvariant p α = ulmInvariant p α

Public easy direction of Ulm's theorem: an isomorphism preserves all classical Ulm invariants.

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

Public hard direction of Ulm's theorem: equal classical Ulm invariants imply isomorphism for countable reduced abelian p-groups.

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

Ulm's theorem: two countable reduced abelian p-groups are isomorphic iff their classical Ulm invariants agree.