Documentation

LeanPool.UlmsTheorem.Ulm.Classification

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.

source
@[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
Instances For
    source
    @[reducible, inline]
    abbrev UlmsTheorem.BFForthPolicy (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] :
    Prop

    Policy for extending a finite stage so that it covers a chosen source element.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev UlmsTheorem.BFBackPolicy (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] :
      Prop

      Policy for extending a finite stage so that it covers a chosen target element.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem UlmsTheorem.iso_of_ulmInvariant_eq_of_backAndForth (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] [Countable G] [Countable H] (hforth : BFForthPolicy p) (hback : 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.

        source
        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.