Pure subgroups and height-preserving partial maps

This file contains the basic hard-direction infrastructure for Ulm's theorem: ordinal height, p-order, purity, and height-preserving maps on subgroups.

noncomputable def UlmsTheorem.ulmHeight (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) : WithTop Ordinal.{0}

The ordinal Ulm height of an element.

Equations

• UlmsTheorem.ulmHeight p x = ⨆ (α : Ordinal.{0}), ⨆ (_ : x ∈ UlmsTheorem.ulmSubgroup p α), ↑α

def UlmsTheorem.IsProper (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) (x : G) : Prop

x is proper with respect to S when its height is maximal in the coset x + S.

Equations

• UlmsTheorem.IsProper p S x = ∀ (s : ↥S), UlmsTheorem.ulmHeight p x ≥ UlmsTheorem.ulmHeight p (x + ↑s)

theorem UlmsTheorem.ulmHeight_le_of_mem_imp (p : ℕ) {G : Type u} [AddCommGroup G] (x y : G) (h : ∀ (α : Ordinal.{0}), x ∈ ulmSubgroup p α → y ∈ ulmSubgroup p α) : ulmHeight p x ≤ ulmHeight p y

Filtration-membership domination implies domination of ordinal Ulm heights.

theorem UlmsTheorem.coe_le_ulmHeight_of_mem (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (α : Ordinal.{0}) (hx : x ∈ ulmSubgroup p α) : ↑α ≤ ulmHeight p x

Membership in G_α gives the corresponding lower bound on Ulm height.

theorem UlmsTheorem.ulmHeight_le_of_not_mem_succ (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (α : Ordinal.{0}) (hxs : x ∉ ulmSubgroup p (Order.succ α)) : ulmHeight p x ≤ ↑α

Failure of membership at the successor of α bounds the Ulm height by α.

Unlike the exact-height lemma below, this does not assume membership in G_α. It is useful when properness rules out a higher representative in a coset.

theorem UlmsTheorem.mem_ulmSubgroup_of_le_ulmHeight (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (γ : Ordinal.{0}) (h : ↑γ ≤ ulmHeight p x) : x ∈ ulmSubgroup p γ

The converse of coe_le_ulmHeight_of_mem. A lower bound on the Ulm height is membership in the filtration: if γ ≤ h(x) then x ∈ G_γ.

The supremum defining ulmHeight is therefore attained whenever it is bounded by an ordinal, so h(x) ≥ γ and x ∈ G_γ are interchangeable. This is the bridge that lets a height condition stated with ulmHeight be used as a filtration hypothesis.

The three cases are genuinely different: at 0 the filtration is everything, at a successor the previous lemma bounds the height strictly below, and at a limit the inductive hypothesis supplies membership at every smaller level, which is exactly the intersection defining G_γ.

theorem UlmsTheorem.mem_ulmSubgroup_iff_le_ulmHeight (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (γ : Ordinal.{0}) : x ∈ ulmSubgroup p γ ↔ ↑γ ≤ ulmHeight p x

Membership in the filtration and a lower bound on the Ulm height are the same statement.

theorem UlmsTheorem.ulmHeight_eq_of_mem_not_mem_succ (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (α : Ordinal.{0}) (hx : x ∈ ulmSubgroup p α) (hxs : x ∉ ulmSubgroup p (Order.succ α)) : ulmHeight p x = ↑α

An element in G_α but not G_(α+1) has Ulm height exactly α.

theorem UlmsTheorem.isProper_iff_forall_not_mem_succ (p : ℕ) {G : Type u} [AddCommGroup G] (S : AddSubgroup G) {x : G} {α : Ordinal.{0}} (hx : x ∈ ulmSubgroup p α) (hxs : x ∉ ulmSubgroup p (Order.succ α)) : IsProper p S x ↔ ∀ (c : ↥S), x + ↑c ∉ ulmSubgroup p (Order.succ α)

For an element of exact height α, properness over S says exactly that no S-translate reaches G_(α+1).

Both Kaplansky target constructions establish properness by ruling out a higher translate and consume it the same way, so this is the form they share.

theorem UlmsTheorem.exists_ulmHeight_eq_of_ne_zero (p : ℕ) {G : Type u} [AddCommGroup G] (hG : IsPReduced p G) {x : G} (hx0 : x ≠ 0) : ∃ (α : Ordinal.{0}), x ∈ ulmSubgroup p α ∧ x ∉ ulmSubgroup p (Order.succ α)

In a reduced p-group, every nonzero element has an attained ordinal Ulm height.

Reducedness supplies a stage missing the element. The least such stage cannot be zero or a limit stage, so it is a successor α+1; minimality then puts the element in G_α but not in G_(α+1).

def UlmsTheorem.IsHeightPreserving (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (φ : G →+ H) : Prop

Height-preserving map between full groups.

Equations

• UlmsTheorem.IsHeightPreserving p φ = ∀ (x : G) (α : Ordinal.{0}), x ∈ UlmsTheorem.ulmSubgroup p α ↔ φ x ∈ UlmsTheorem.ulmSubgroup p α

def UlmsTheorem.IsHeightPresOn (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (φ : ↥A →+ ↥B) : Prop

Height-preserving map between subgroups A ≤ G and B ≤ H.

Equations

• UlmsTheorem.IsHeightPresOn p φ = ∀ (a : ↥A) (α : Ordinal.{0}), ↑a ∈ UlmsTheorem.ulmSubgroup p α ↔ ↑(φ a) ∈ UlmsTheorem.ulmSubgroup p α

noncomputable def UlmsTheorem.pOrder (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) : ℕ∞

The p-order of an element: the least n such that p^n • x = 0, or ⊤ if no such n exists.

Equations

• UlmsTheorem.pOrder p x = ⨅ (n : ℕ), ⨅ (_ : p ^ n • x = 0), ↑n

@[simp]

theorem UlmsTheorem.pOrder_zero (p : ℕ) {G : Type u} [AddCommGroup G] : pOrder p 0 = 0

theorem UlmsTheorem.smul_eq_zero_iff_le_pOrder (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (n : ℕ) : p ^ n • x = 0 ↔ pOrder p x ≤ ↑n

theorem UlmsTheorem.pOrder_le_succ_of_smul_p_le (p : ℕ) {G : Type u} [AddCommGroup G] {x : G} {n : ℕ} (h : pOrder p (p • x) ≤ ↑n) : pOrder p x ≤ ↑n + 1

Killing p • x at level n kills x at level n + 1.

theorem UlmsTheorem.smul_p_pOrder_le_of_le_succ (p : ℕ) {G : Type u} [AddCommGroup G] {x : G} {n : ℕ} (h : pOrder p x ≤ ↑n + 1) : pOrder p (p • x) ≤ ↑n

The converse: killing x at level n + 1 kills p • x at level n.

theorem UlmsTheorem.pOrder_smul_p (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (hx : 0 < pOrder p x) : pOrder p (p • x) = pOrder p x - 1

theorem UlmsTheorem.pOrder_pos_of_ne_zero (p : ℕ) {G : Type u} [AddCommGroup G] (x : G) (hx : x ≠ 0) : 0 < pOrder p x

def UlmsTheorem.IsPure (p : ℕ) {G : Type u} [AddCommGroup G] (A : AddSubgroup G) : Prop

A subgroup is p-pure if divisibility by powers of p seen in the ambient group is already witnessed internally.

Equations

• UlmsTheorem.IsPure p A = ∀ (n : ℕ) (x : ↥A), ↑x ∈ UlmsTheorem.pPow p n → x ∈ UlmsTheorem.pPow p n

def UlmsTheorem.IsIsotype (p : ℕ) {G : Type u} [AddCommGroup G] (A : AddSubgroup G) : Prop

An isotype subgroup is one whose induced Ulm filtration agrees with the ambient filtration on every element. This is stronger than purity, and it is the right hypothesis for ambient/intrinsic height equality.

Equations

• UlmsTheorem.IsIsotype p A = ∀ (x : ↥A) (α : Ordinal.{0}), ↑x ∈ UlmsTheorem.ulmSubgroup p α ↔ x ∈ UlmsTheorem.ulmSubgroup p α

theorem UlmsTheorem.IsPure_bot (p : ℕ) {G : Type u} [AddCommGroup G] : IsPure p ⊥

theorem UlmsTheorem.IsPure_top (p : ℕ) {G : Type u} [AddCommGroup G] : IsPure p ⊤

theorem UlmsTheorem.IsIsotype.isPure (p : ℕ) {G : Type u} [AddCommGroup G] {A : AddSubgroup G} (hA : IsIsotype p A) : IsPure p A

theorem UlmsTheorem.ulmHeight_subgroup_le_ambient (p : ℕ) {G : Type u} [AddCommGroup G] {A : AddSubgroup G} (x : ↥A) : ulmHeight p x ≤ ulmHeight p ↑x

theorem UlmsTheorem.IsIsotype.ulmHeight_eq (p : ℕ) {G : Type u} [AddCommGroup G] {A : AddSubgroup G} (hA : IsIsotype p A) (x : ↥A) : ulmHeight p ↑x = ulmHeight p x

theorem UlmsTheorem.IsHeightPreserving.injective (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hred : IsPReduced p G) {φ : G →+ H} (hφ : IsHeightPreserving p φ) : Function.Injective ⇑φ

theorem UlmsTheorem.IsHeightPresOn.injective (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] (hred : IsPReduced p G) {A : AddSubgroup G} {B : AddSubgroup H} {φ : ↥A →+ ↥B} (hφ : IsHeightPresOn p φ) : Function.Injective ⇑φ

theorem UlmsTheorem.not_mem_of_mem_of_not_mem_add {G : Type u} [AddCommGroup G] {S : AddSubgroup G} {a b : G} (ha : a ∈ S) (hb : b ∉ S) : a + b ∉ S

If a is in a subgroup but b is not, their sum is not in the subgroup. Useful for the ultrametric argument in the extension theorem.

theorem UlmsTheorem.mem_ulmSubgroup_zsmul_iff (p : ℕ) {G : Type u} [AddCommGroup G] [Fact (Nat.Prime p)] (hprim : IsPrimaryPGroup p G) {n : ℤ} (hn : ¬↑p ∣ n) (u : G) (β : Ordinal.{0}) : n • u ∈ ulmSubgroup p β ↔ u ∈ ulmSubgroup p β

Multiplication by an integer prime to p preserves the filtration.

In a primary group every element has p-power order, so an n prime to p is invertible on it: Bezout gives a·n + b·p^k = 1 with p^k • u = 0, whence u = a • (n • u). Membership of n • u and of u therefore agree at every level.

This generalizes mem_ulmSubgroup_zsmul_iff_of_pSocle off the socle, which is what the one-line extension step needs: the challenge element is a socle element, but the elements b + r·x it must be checked against are not.

theorem UlmsTheorem.ulmHeight_zsmul (p : ℕ) {G : Type u} [AddCommGroup G] [Fact (Nat.Prime p)] (hprim : IsPrimaryPGroup p G) {n : ℤ} (hn : ¬↑p ∣ n) (u : G) : ulmHeight p (n • u) = ulmHeight p u

Multiplication by an integer prime to p preserves Ulm height.

theorem UlmsTheorem.mem_ulmSubgroup_zsmul_iff_of_pSocle (p : ℕ) {G : Type u} [AddCommGroup G] [Fact (Nat.Prime p)] {g : G} (hpg : p • g = 0) {n : ℤ} (hn : ¬↑p ∣ n) (β : Ordinal.{u_1}) : n • g ∈ ulmSubgroup p β ↔ g ∈ ulmSubgroup p β

For an element g of the p-socle (p • g = 0), membership of n • g in a Ulm subgroup is equivalent to membership of g, provided p ∤ n. Proof: Bezout gives a * n + b * p = 1, so g = a • (n • g) + b • (p • g) = a • (n • g).

theorem UlmsTheorem.IsPure.map_of_heightPres (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} (hA : IsPure p A) (φ : G →+ H) (hφ : IsHeightPreserving p φ) : IsPure p (AddSubgroup.map φ A)

theorem UlmsTheorem.IsPure.range_of_heightPresOn (p : ℕ) {G : Type u} [AddCommGroup G] {H : Type u} [AddCommGroup H] {A : AddSubgroup G} {B : AddSubgroup H} (hA : IsPure p A) (φ : ↥A →+ ↥B) (hφ : IsHeightPresOn p φ) : IsPure p (AddSubgroup.map (B.subtype.comp φ) ⊤)