Extension lemmas for Ulm's theorem

This file contains the one-generator extension interface used in the hard direction of Ulm's theorem, formulated against the classical invariants dim_{ℤ/pℤ}(P_α / P_{α+1}).

Kaplansky's finite-stage data

noncomputable def UlmsTheorem.stageAt (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : AddSubgroup G

S_α = S ∩ G_α.

Equations

• UlmsTheorem.stageAt p S α = S ⊓ UlmsTheorem.ulmSubgroup p α

noncomputable def UlmsTheorem.kaplanskyStar (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : AddSubgroup G

Kaplansky's S_α* = S_α ∩ p⁻¹G_{α+2}.

Equations

• One or more equations did not get rendered due to their size.

theorem UlmsTheorem.stageAt_succ_le_kaplanskyStar (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : stageAt p S (Order.succ α) ≤ kaplanskyStar p S α

S_{α+1} is contained in S_α*.

noncomputable def UlmsTheorem.stageAtSuccInStar (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : AddSubgroup ↥(kaplanskyStar p S α)

S_{α+1} viewed as a subgroup of S_α*.

Equations

• UlmsTheorem.stageAtSuccInStar p S α = AddSubgroup.comap (UlmsTheorem.kaplanskyStar p S α).subtype (UlmsTheorem.stageAt p S (Order.succ α))

noncomputable def UlmsTheorem.kaplanskyDomainQuotient (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : Type u

The source quotient in Kaplansky's relative-Ulm map.

Equations

• UlmsTheorem.kaplanskyDomainQuotient p S α = (↥(UlmsTheorem.kaplanskyStar p S α) ⧸ UlmsTheorem.stageAtSuccInStar p S α)

@[instance_reducible]

noncomputable instance UlmsTheorem.instAddCommGroupKaplanskyDomainQuotient (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : AddCommGroup (kaplanskyDomainQuotient p S α)

Equations

• UlmsTheorem.instAddCommGroupKaplanskyDomainQuotient p S α = id inferInstance

theorem UlmsTheorem.kaplanskyDomainQuotient_orderOf_dvd_p (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : kaplanskyDomainQuotient p S α) : p • x = 0

Every class in Kaplansky's source quotient is killed by p.

@[instance_reducible]

noncomputable instance UlmsTheorem.kaplanskyDomainQuotientModule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : Module (ZMod p) (kaplanskyDomainQuotient p S α)

Equations

• UlmsTheorem.kaplanskyDomainQuotientModule p S α = AddCommGroup.zmodModule ⋯

noncomputable def UlmsTheorem.kaplanskyLinearMap (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : kaplanskyDomainQuotient p S α →ₗ[ZMod p] ulmQuotient p α

An additive Kaplansky map is automatically ZMod p-linear.

Equations

• UlmsTheorem.kaplanskyLinearMap p S α U = AddMonoidHom.toZModLinearMap p U

noncomputable def UlmsTheorem.kaplanskyOccupiedSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : Submodule (ZMod p) (ulmQuotient p α)

The occupied part of the Ulm layer: the range of a Kaplansky map.

Equations

• UlmsTheorem.kaplanskyOccupiedSubmodule p S α U = (UlmsTheorem.kaplanskyLinearMap p S α U).range

@[reducible, inline]

abbrev UlmsTheorem.kaplanskyRoomQuotient (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : Type u

The remaining room in the Ulm layer, after quotienting by the occupied range.

Equations

• UlmsTheorem.kaplanskyRoomQuotient p S α U = (UlmsTheorem.ulmQuotient p α ⧸ UlmsTheorem.kaplanskyOccupiedSubmodule p S α U)

noncomputable def UlmsTheorem.kaplanskyRoomInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : Cardinal.{u}

The dimension of the unoccupied quotient of the Ulm layer.

Equations

• UlmsTheorem.kaplanskyRoomInvariant p S α U = Module.rank (ZMod p) (UlmsTheorem.kaplanskyRoomQuotient p S α U)

theorem UlmsTheorem.kaplansky_room_equation (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : kaplanskyRoomInvariant p S α U + Module.rank (ZMod p) ↥(kaplanskyOccupiedSubmodule p S α U) = ulmInvariant p α

Rank bookkeeping for Kaplansky's map: room + occupied = the ordinary Ulm invariant.

theorem UlmsTheorem.kaplansky_not_surjective_iff_room (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α) : ¬Function.Surjective ⇑U ↔ Nontrivial (kaplanskyRoomQuotient p S α U)

“Not onto means room”: a Kaplansky map fails to be surjective exactly when its room quotient is nontrivial.

theorem UlmsTheorem.exists_kaplanskyCorrection (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : ↥(kaplanskyStar p S α)) : ∃ y ∈ ulmSubgroup p (Order.succ α), p • y = p • ↑x

A chosen correction one level higher, with the same p-multiple as an element of S_α*. The eventual quotient class is independent of this choice.

noncomputable def UlmsTheorem.kaplanskyCorrection (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : ↥(kaplanskyStar p S α)) : G

A choice of a one-level-higher correction with the prescribed p-multiple.

Equations

• UlmsTheorem.kaplanskyCorrection p S α x = Classical.choose ⋯

theorem UlmsTheorem.kaplanskyCorrection_mem (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : ↥(kaplanskyStar p S α)) : kaplanskyCorrection p S α x ∈ ulmSubgroup p (Order.succ α)

theorem UlmsTheorem.kaplanskyCorrection_smul (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : ↥(kaplanskyStar p S α)) : p • kaplanskyCorrection p S α x = p • ↑x

noncomputable def UlmsTheorem.kaplanskySocleRep (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) (x : ↥(kaplanskyStar p S α)) : ↥(pSocleAt p α)

The order-p representative x-y ∈ P_α used in Kaplansky's map.

Equations

• UlmsTheorem.kaplanskySocleRep p S α x = ⟨↑x - UlmsTheorem.kaplanskyCorrection p S α x, ⋯⟩

noncomputable def UlmsTheorem.kaplanskyPreMap (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : ↥(kaplanskyStar p S α) →+ ulmQuotient p α

The pre-quotient Kaplansky homomorphism on S_α*.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def UlmsTheorem.kaplanskyMap (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : kaplanskyDomainQuotient p S α →+ ulmQuotient p α

Kaplansky's canonical linear map S_α*/S_(α+1) → P_α/P_(α+1).

Equations

• UlmsTheorem.kaplanskyMap p S α = QuotientAddGroup.lift (UlmsTheorem.stageAtSuccInStar p S α) (UlmsTheorem.kaplanskyPreMap p S α) ⋯

theorem UlmsTheorem.kaplanskyMap_injective (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : Function.Injective ⇑(kaplanskyMap p S α)

theorem UlmsTheorem.kaplanskyMap_range (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_1}) : (kaplanskyLinearMap p S α (kaplanskyMap p S α)).range = relativeOccupiedSubmodule p S α

The canonical Kaplansky map occupies exactly ((S + G_(α+1)) ∩ P_α) / P_(α+1) in the ordinary Ulm layer.

theorem UlmsTheorem.relativeUlmQuotient_nontrivial_iff_proper (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{0}) : Nontrivial (relativeUlmQuotient p S α) ↔ ∃ v ∈ pSocleAt p α, v ∉ ulmSubgroup p (Order.succ α) ∧ IsProper p S v

The relative Ulm quotient is nontrivial exactly when there is a proper order-p representative of exact height α.

theorem UlmsTheorem.kaplanskyMap_not_surjective_iff_proper (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{0}) : ¬Function.Surjective ⇑(kaplanskyMap p S α) ↔ ∃ v ∈ pSocleAt p α, v ∉ ulmSubgroup p (Order.succ α) ∧ IsProper p S v

Canonical form of Kaplansky's range lemma: his specified map is not onto exactly when there is an exact-height-α socle element proper over S.

theorem UlmsTheorem.kaplansky_range_lemma (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{0}) : ∃ (U : kaplanskyDomainQuotient p S α →+ ulmQuotient p α), Function.Injective ⇑U ∧ (¬Function.Surjective ⇑U ↔ ∃ v ∈ pSocleAt p α, v ∉ ulmSubgroup p (Order.succ α) ∧ IsProper p S v)

Kaplansky's range lemma, the central relative ingredient in the one-generator extension argument. The map sends a class represented by x ∈ S_α* to the class of x-y in P_α/P_{α+1}, where py = px and y ∈ G_{α+1}.

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

A finite height-preserving partial isomorphism, as used in Kaplansky's proof.

The stages are deliberately finite, not finitely generated pure subgroups. Requiring purity would make it impossible to cover a nonzero element of G_ω.

• A : AddSubgroup G

  The finite source subgroup.

• B : AddSubgroup H

  The finite target subgroup.

• hAfinite : (↑self.A).Finite
• hBfinite : (↑self.B).Finite
• e : ↥self.A ≃+ ↥self.B

  The partial additive equivalence between the stage subgroups.

• hφ : IsHeightPresOn p self.e.toAddMonoidHom

structure UlmsTheorem.UlmStageAt (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (α : Ordinal.{0}) : Type u

The exact local interface used by Kaplansky target selection at height α. Only filtration preservation at α, α+1, and α+2 enters the range argument. Keeping this separate from UlmStage lets cutoff-preserving ACM stages use the same construction below their cutoff.

• A : AddSubgroup G

  The finite source subgroup.

• B : AddSubgroup H

  The finite target subgroup.

• hAfinite : (↑self.A).Finite
• hBfinite : (↑self.B).Finite
• e : ↥self.A ≃+ ↥self.B

  The partial additive equivalence between the stage subgroups.

• hφ_at (x : ↥self.A) : ↑x ∈ ulmSubgroup p α ↔ ↑(self.e x) ∈ ulmSubgroup p α
• hφ_succ (x : ↥self.A) : ↑x ∈ ulmSubgroup p (Order.succ α) ↔ ↑(self.e x) ∈ ulmSubgroup p (Order.succ α)
• hφ_succSucc (x : ↥self.A) : ↑x ∈ ulmSubgroup p (Order.succ (Order.succ α)) ↔ ↑(self.e x) ∈ ulmSubgroup p (Order.succ (Order.succ α))

def UlmsTheorem.UlmStage.at (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (s : UlmStage p) (α : Ordinal.{0}) : UlmStageAt p α

A globally height-preserving stage supplies the local three-level interface at every height.

Equations

• UlmsTheorem.UlmStage.at p s α = { A := s.A, B := s.B, hAfinite := ⋯, hBfinite := ⋯, e := s.e, hφ_at := ⋯, hφ_succ := ⋯, hφ_succSucc := ⋯ }

noncomputable def UlmsTheorem.UlmStage.symm (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (s : UlmStage p) : UlmStage p

Reverse a finite partial isomorphism.

Equations

• UlmsTheorem.UlmStage.symm p s = { A := s.B, B := s.A, hAfinite := ⋯, hBfinite := ⋯, e := s.e.symm, hφ := ⋯ }

noncomputable def UlmsTheorem.kaplanskyStarEquiv (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) : ↥(kaplanskyStar p s.A α) ≃+ ↥(kaplanskyStar p s.B α)

A height-preserving stage isomorphism identifies Kaplansky's starred subgroups on the two sides.

Equations

• One or more equations did not get rendered due to their size.

theorem UlmsTheorem.kaplanskyStarEquiv_map_stageAtSucc (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) : AddSubgroup.map (kaplanskyStarEquiv p s).toAddMonoidHom (stageAtSuccInStar p s.A α) = stageAtSuccInStar p s.B α

noncomputable def UlmsTheorem.kaplanskyDomainEquiv (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) : kaplanskyDomainQuotient p s.A α ≃+ kaplanskyDomainQuotient p s.B α

The stage isomorphism induces an additive equivalence between the finite source quotients in Kaplansky's range maps.

Equations

• UlmsTheorem.kaplanskyDomainEquiv p s = QuotientAddGroup.congr (UlmsTheorem.stageAtSuccInStar p s.A α) (UlmsTheorem.stageAtSuccInStar p s.B α) (UlmsTheorem.kaplanskyStarEquiv p s) ⋯

theorem UlmsTheorem.kaplanskyDomain_rank_eq (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) : Module.rank (ZMod p) (kaplanskyDomainQuotient p s.A α) = Module.rank (ZMod p) (kaplanskyDomainQuotient p s.B α)

Corresponding finite stages give Kaplansky source quotients of equal ZMod p-dimension.

theorem UlmsTheorem.kaplanskyDomain_module_finite (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (hSfinite : (↑S).Finite) (α : Ordinal.{0}) : Module.Finite (ZMod p) (kaplanskyDomainQuotient p S α)

Kaplansky's source quotient is finite-dimensional when the stage itself is finite.

theorem UlmsTheorem.kaplansky_not_surjective_transfer (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) (hinv : ulmInvariant p α = ulmInvariant p α) (hGroom : ¬Function.Surjective ⇑(kaplanskyMap p s.A α)) : ¬Function.Surjective ⇑(kaplanskyMap p s.B α)

Non-surjectivity of Kaplansky's range map transfers across a finite height-preserving stage when the ordinary Ulm invariants at α agree.

Finiteness of the source quotient is essential here: injective endomorphisms of infinite-dimensional spaces need not be onto.

theorem UlmsTheorem.extend_by_one_of_mem (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (hB : IsPure p B) (φ : ↥A →+ ↥B) (hφ : IsHeightPresOn p φ) {g : G} (hg : g ∈ A) : ∃ (A' : AddSubgroup G) (hAA' : A ≤ A') (_ : g ∈ A') (B' : AddSubgroup H) (_ : IsPure p B') (_ : B ≤ B') (φ' : ↥A' →+ ↥B'), IsHeightPresOn p φ' ∧ ∀ (a : ↥A), ↑(φ' ⟨↑a, ⋯⟩) = ↑(φ a)

Trivial extension when the prescribed generator is already in the domain subgroup.

theorem UlmsTheorem.extend_by_one_fg_of_mem (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} (hA : IsPure p A) (hAfg : A.FG) {B : AddSubgroup H} (hB : IsPure p B) (hBfg : B.FG) (φ : ↥A →+ ↥B) (hφ : IsHeightPresOn p φ) {g : G} (hg : g ∈ A) : ∃ (A' : AddSubgroup G) (_ : IsPure p A') (_ : A'.FG) (hAA' : A ≤ A') (_ : g ∈ A') (B' : AddSubgroup H) (_ : IsPure p B') (_ : B'.FG) (_ : B ≤ B') (φ' : ↥A' →+ ↥B'), IsHeightPresOn p φ' ∧ ∀ (a : ↥A), ↑(φ' ⟨↑a, ⋯⟩) = ↑(φ a)

Trivial finite-stage extension when the prescribed generator is already in the domain subgroup.

def UlmsTheorem.adjoinElem {G : Type u} [AddCommGroup G] (A : AddSubgroup G) (g : G) : AddSubgroup G

Adjoin one element to a subgroup by taking the supremum with its cyclic closure.

Equations

• UlmsTheorem.adjoinElem A g = A ⊔ AddSubgroup.closure {g}

theorem UlmsTheorem.le_adjoinElem {G : Type u} [AddCommGroup G] (A : AddSubgroup G) (g : G) : A ≤ adjoinElem A g

theorem UlmsTheorem.mem_adjoinElem_right {G : Type u} [AddCommGroup G] (A : AddSubgroup G) (g : G) : g ∈ adjoinElem A g

theorem UlmsTheorem.adjoinElem_fg {G : Type u} [AddCommGroup G] {A : AddSubgroup G} (hAfg : A.FG) (g : G) : (adjoinElem A g).FG

theorem UlmsTheorem.adjoinElem_finite (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] (hG : IsPrimaryPGroup p G) {A : AddSubgroup G} (hAfinite : (↑A).Finite) (g : G) : (↑(adjoinElem A g)).Finite

Adjoining one element to a finite subgroup of a primary group remains finite.

theorem UlmsTheorem.adjoinElem_eq_sup_zmultiples {G : Type u} [AddCommGroup G] (A : AddSubgroup G) (g : G) : adjoinElem A g = A ⊔ AddSubgroup.zmultiples g

theorem UlmsTheorem.mem_adjoinElem_iff {G : Type u} [AddCommGroup G] {A : AddSubgroup G} {g x : G} : x ∈ adjoinElem A g ↔ ∃ a ∈ A, ∃ (n : ℤ), a + n • g = x

theorem UlmsTheorem.dvd_of_zsmul_mem_of_not_mem (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {A : AddSubgroup G} {g : G} (hg_notin : g ∉ A) (hpg_in : p • g ∈ A) (k : ℤ) (hk : k • g ∈ A) : ↑p ∣ k

theorem UlmsTheorem.socle_extend_build_map (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) {g : G} (hg_notin : g ∉ A) {h : H} (hpg_in : p • g ∈ A) (hrel : p • h = ↑(φ ⟨p • g, hpg_in⟩)) : ∃ (φ' : ↥(adjoinElem A g) →+ ↥⊤), (∀ (a : ↥A), ↑(φ' ⟨↑a, ⋯⟩) = ↑(φ a)) ∧ ↑(φ' ⟨g, ⋯⟩) = h

theorem UlmsTheorem.phi_zsmul_eq_zsmul_h (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) {g : G} (hg_notin : g ∉ A) (hpg_in : p • g ∈ A) {h : H} (hh_eq : p • h = ↑(φ ⟨p • g, hpg_in⟩)) (k : ℤ) (hk : k • g ∈ A) : ↑(φ ⟨k • g, hk⟩) = k • h

theorem UlmsTheorem.extend_well_defined (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) {g : G} (hg_notin : g ∉ A) (hpg_in : p • g ∈ A) {h : H} (hh_eq : p • h = ↑(φ ⟨p • g, hpg_in⟩)) {a₁ a₂ : G} {n₁ n₂ : ℤ} (ha₁ : a₁ ∈ A) (ha₂ : a₂ ∈ A) (heq : a₁ + n₁ • g = a₂ + n₂ • g) : ↑(φ ⟨a₁, ha₁⟩) + n₁ • h = ↑(φ ⟨a₂, ha₂⟩) + n₂ • h

theorem UlmsTheorem.not_mem_succ_add_zsmul_of_proper (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {A : AddSubgroup G} {x : G} {α : Ordinal.{0}} (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p A x) (hpxA : p • x ∈ A) (a : ↥A) (n : ℤ) (hn : ¬↑p ∣ n) : ↑a + n • x ∉ ulmSubgroup p (Order.succ α)

If x has exact height α, is proper over A, and p • x ∈ A, then no coefficient prime to p can move a translate of x into G_(α+1). This is the filtration form of the height calculation used when Kaplansky says the extended map is still height-preserving.

theorem UlmsTheorem.proper_adjoin_rep_mem_iff (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) (hφ : IsHeightPresOn p φ) {x : G} {w : H} {α β : Ordinal.{0}} (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hwα : w ∈ ulmSubgroup p α) (hwSucc : w ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p A x) (hwProper : IsProper p B w) (hpxA : p • x ∈ A) (hpw : p • w = ↑(φ ⟨p • x, hpxA⟩)) (a : ↥A) (n : ℤ) : ↑a + n • x ∈ ulmSubgroup p β ↔ ↑(φ a) + n • w ∈ ulmSubgroup p β

The elementwise filtration calculation behind the one-generator extension. If x and w have the same exact height, are proper over the matched subgroups, and satisfy the same p-relation, then corresponding normal forms a + n • x and φ(a) + n • w lie in exactly the same Ulm subgroups.

theorem UlmsTheorem.socle_extend_build_map_heightPres (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) (hφ : IsHeightPresOn p φ) {x : G} (hx_notin : x ∉ A) {w : H} {α : Ordinal.{0}} (hpxA : p • x ∈ A) (hpw : p • w = ↑(φ ⟨p • x, hpxA⟩)) (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hwα : w ∈ ulmSubgroup p α) (hwSucc : w ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p A x) (hwProper : IsProper p B w) : ∃ (φ' : ↥(adjoinElem A x) →+ ↥⊤), (∀ (a : ↥A), ↑(φ' ⟨↑a, ⋯⟩) = ↑(φ a)) ∧ ↑(φ' ⟨x, ⋯⟩) = w ∧ IsHeightPresOn p φ'

The quotient-built homomorphism on A + ⟨x⟩ is height-preserving once the chosen image w satisfies Kaplansky's exact-height and properness conditions.

theorem UlmsTheorem.kaplansky_extend_one_of_target (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hG : IsReducedPGroup p G) (s : UlmStage p) {x : G} (hx_notin : x ∉ s.A) {w : H} {α : Ordinal.{0}} (hpxA : p • x ∈ s.A) (hpw : p • w = ↑(s.e ⟨p • x, hpxA⟩)) (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hwα : w ∈ ulmSubgroup p α) (hwSucc : w ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p s.A x) (hwProper : IsProper p s.B w) : ∃ (s' : UlmStage p) (hAA : s.A ≤ s'.A) (_ : s.B ≤ s'.B), x ∈ s'.A ∧ ∀ (a : ↥s.A), ↑(s'.e ⟨↑a, ⋯⟩) = ↑(s.e a)

Once the target representative required on page 30 has been found, the actual finite-stage extension is formal algebra: build the quotient map, restrict its codomain to its range, and use height preservation for injectivity.

theorem UlmsTheorem.exists_kaplanskyNormalized (p : ℕ) {G : Type u} [AddCommGroup G] {A : AddSubgroup G} (hAfinite : (↑A).Finite) (g : G) : ∃ (x : G), x - g ∈ A ∧ IsProper p A x ∧ ∀ (y : G), y - g ∈ A → IsProper p A y → ulmHeight p (p • y) ≤ ulmHeight p (p • x)

A finite coset has a representative satisfying both of Kaplansky's normalizations: first maximize the height of the representative, then, among the proper representatives, maximize the height of its p-multiple.

theorem UlmsTheorem.exists_kaplanskyTarget_caseI (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) {x : G} (hpxA : p • x ∈ s.A) (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p s.A x) (hpxMax : ∀ (y : G), y - x ∈ s.A → IsProper p s.A y → ulmHeight p (p • y) ≤ ulmHeight p (p • x)) (hcaseI : p • x ∉ ulmSubgroup p (Order.succ (Order.succ α))) : ∃ (w : H), p • w = ↑(s.e ⟨p • x, hpxA⟩) ∧ w ∈ ulmSubgroup p α ∧ w ∉ ulmSubgroup p (Order.succ α) ∧ IsProper p s.B w

Kaplansky's Case I target construction.

If p • x has exact height α+1, any height-α root of its image is automatically proper over the target stage. The proof uses the second normalization of x to rule out a higher translate.

theorem UlmsTheorem.exists_kaplanskyTarget_caseII (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {α : Ordinal.{0}} (s : UlmStageAt p α) {x : G} (hinv : ulmInvariant p α = ulmInvariant p α) (hpxA : p • x ∈ s.A) (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p s.A x) (hcaseII : p • x ∈ ulmSubgroup p (Order.succ (Order.succ α))) : ∃ (w : H), p • w = ↑(s.e ⟨p • x, hpxA⟩) ∧ w ∈ ulmSubgroup p α ∧ w ∉ ulmSubgroup p (Order.succ α) ∧ IsProper p s.B w

Kaplansky's Case II target construction.

When p • x lies two levels higher, subtract a higher root to expose a proper exact-height socle element. The canonical range lemma and equality of the ordinary Ulm invariant transfer the resulting room to the target side; adding that target socle element to a higher root gives the required image.

theorem UlmsTheorem.kaplansky_extend_one_of_normalized (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hG : IsReducedPGroup p G) (s : UlmStage p) {x : G} {α : Ordinal.{0}} (hinv : ulmInvariant p α = ulmInvariant p α) (hx_notin : x ∉ s.A) (hpxA : p • x ∈ s.A) (hxα : x ∈ ulmSubgroup p α) (hxSucc : x ∉ ulmSubgroup p (Order.succ α)) (hxProper : IsProper p s.A x) (hpxMax : ∀ (y : G), y - x ∈ s.A → IsProper p s.A y → ulmHeight p (p • y) ≤ ulmHeight p (p • x)) : ∃ (s' : UlmStage p) (hAA : s.A ≤ s'.A) (_ : s.B ≤ s'.B), x ∈ s'.A ∧ ∀ (a : ↥s.A), ↑(s'.e ⟨↑a, ⋯⟩) = ↑(s.e a)

Kaplansky's one-step extension from an already normalized element.

The full kaplansky_extend_one theorem below first searches a finite coset for such an x. Once x is given with exact height α, properness, and the maximal-p x normalization, target selection uses the ordinary Ulm invariant only at this single height α. This height-local form is the one needed by the below-base band of the ACM construction, where invariant equality is known only below a cutoff.

theorem UlmsTheorem.kaplansky_extend_one (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hG : IsReducedPGroup p G) (hinv : ∀ (β : Ordinal.{0}), ulmInvariant p β = ulmInvariant p β) (s : UlmStage p) (g : G) (hpgA : p • g ∈ s.A) : ∃ (s' : UlmStage p) (hAA : s.A ≤ s'.A) (_ : s.B ≤ s'.B), g ∈ s'.A ∧ ∀ (a : ↥s.A), ↑(s'.e ⟨↑a, ⋯⟩) = ↑(s.e a)

Kaplansky's page-30 one-step extension.

The input condition p • g ∈ A is the precise one-step hypothesis. A normalized representative of the coset g + A has an attained exact height; the two target-selection lemmas above then cover whether its p-multiple has height exactly one higher or lies at least two levels higher.

theorem UlmsTheorem.kaplansky_extend (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hG : IsReducedPGroup p G) (hinv : ∀ (β : Ordinal.{0}), ulmInvariant p β = ulmInvariant p β) (s : UlmStage p) (g : G) : ∃ (s' : UlmStage p) (hAA : s.A ≤ s'.A) (_ : s.B ≤ s'.B), g ∈ s'.A ∧ ∀ (a : ↥s.A), ↑(s'.e ⟨↑a, ⋯⟩) = ↑(s.e a)

Kaplansky's finite-stage extension theorem.

Starting from finite subgroups related by a height-preserving isomorphism, extend the stage to cover a prescribed source element. This is the iterated conclusion used by the back-and-forth construction, not the single px ∈ A step on page 30: primaryness first supplies a power of p lying in A, and the proof then applies the single-step construction repeatedly. Only the source group must be reduced in this direction; the target reducedness hypothesis enters when this theorem is applied symmetrically for the back step. At each single step exists_kaplanskyNormalized supplies Kaplansky's two normalizations, and Case II uses the canonical range theorem.