Reducedness and height theory

This file contains the reducedness predicate used in the project and the basic finite p-height calculus.

Primary, reduced, and separable groups

def UlmsTheorem.IsPrimaryPGroup (p : ℕ) (G : Type u_1) [AddCommGroup G] : Prop

G is p-primary if every element is killed by some power of p.

This hypothesis is logically independent from reducedness. In particular, torsion-free groups such as ℤ must not enter Ulm's classification theorem merely because their p-socle is trivial.

Equations

• UlmsTheorem.IsPrimaryPGroup p G = ∀ (x : G), ∃ (n : ℕ), p ^ n • x = 0

def UlmsTheorem.IsPReduced (p : ℕ) (G : Type u_1) [AddCommGroup G] : Prop

The p-Ulm filtration of G is reduced if it eventually reaches zero.

For the countable p-primary groups classified below, this is equivalent to saying that G has no nontrivial divisible subgroup: the eventual stable Ulm subgroup is the maximal divisible subgroup. Crucially, this does not require G_ω = 0; reduced groups may contain elements of infinite height and have arbitrary countable Ulm length.

Equations

• UlmsTheorem.IsPReduced p G = ∃ (α : Ordinal.{0}), UlmsTheorem.ulmSubgroup p α = ⊥

structure UlmsTheorem.IsReducedPGroup (p : ℕ) (G : Type u_1) [AddCommGroup G] : Prop

A reduced abelian p-group: primary, with zero divisible part.

• primary : IsPrimaryPGroup p G
• reduced : IsPReduced p G

def UlmsTheorem.IsPSeparable (p : ℕ) (G : Type u_1) [AddCommGroup G] : Prop

G is p-separable if it has no nonzero element of infinite p-height.

This was formerly (and incorrectly) called IsReducedPGroup. It is strictly stronger than reducedness: it says G_ω = 0.

Equations

• UlmsTheorem.IsPSeparable p G = ∀ (x : G), (∀ (n : ℕ), ∃ (y : G), p ^ n • y = x) → x = 0

theorem UlmsTheorem.isPSeparable_iff_iInf (p : ℕ) {G : Type u_1} [AddCommGroup G] : IsPSeparable p G ↔ ⨅ (n : ℕ), pPow p n = ⊥

G is p-separable iff ⋂_n p^n·G = 0.

p-height

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

The p-height of x: ⊤ if x = 0, otherwise the supremum of the natural numbers n such that x ∈ p^n·G.

Equations

• UlmsTheorem.pHeight p x = if x = 0 then ⊤ else sSup (WithTop.some '' {n : ℕ | ∃ (y : G), p ^ n • y = x})

@[simp]

theorem UlmsTheorem.pHeight_zero (p : ℕ) {G : Type u_1} [AddCommGroup G] : pHeight p 0 = ⊤

theorem UlmsTheorem.pHeight_ge_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (x : G) (n : ℕ) : ↑n ≤ pHeight p x ↔ ∃ (y : G), p ^ n • y = x

theorem UlmsTheorem.pHeight_ge_iff_mem (p : ℕ) {G : Type u_1} [AddCommGroup G] (x : G) (n : ℕ) : ↑n ≤ pHeight p x ↔ x ∈ pPow p n

theorem UlmsTheorem.pHeight_add_ge (p : ℕ) {G : Type u_1} [AddCommGroup G] (x y : G) (n : ℕ) (hx : ↑n ≤ pHeight p x) (hy : ↑n ≤ pHeight p y) : ↑n ≤ pHeight p (x + y)

theorem UlmsTheorem.pHeight_add_ge_min (p : ℕ) {G : Type u_1} [AddCommGroup G] (x y : G) : min (pHeight p x) (pHeight p y) ≤ pHeight p (x + y)

theorem UlmsTheorem.pHeight_add_eq_min_of_ne (p : ℕ) {G : Type u_1} [AddCommGroup G] (x y : G) (h : pHeight p x ≠ pHeight p y) : pHeight p (x + y) = min (pHeight p x) (pHeight p y)