Ulm invariants

For a prime p and a reduced abelian p-group G, the Ulm invariant at ordinal α is f_G(α) = dim_{ℤ/pℤ} (P_α / P_{α+1}), where P_α = G[p] ∩ p^α·G = pSocleAt p α.

We also keep the raw filtration quotient G_α / G_{α+1} available as layerQuotient / layerInvariant; this is useful auxiliary data, but it is not the classical Ulm invariant used in Ulm's theorem.

Main definitions

• layerQuotient p α G : the quotient group (p^α·G) / (p^(α+1)·G)
• layerInvariant p α G : the cardinal rank of layerQuotient as a ℤ/pℤ-module
• ulmQuotient p α G : the quotient group P_α / P_{α+1}
• ulmInvariant p α G : the cardinal rank of ulmQuotient as a ℤ/pℤ-module
• ulmLength p G : the least ordinal α with p^α·G = 0 (exists for reduced groups)

References

• Fuchs, "Abelian Groups", Chapter 11, §1
• Kaplansky, "Infinite Abelian Groups", Theorem 14

The raw filtration quotient G_α / G_{α+1}

noncomputable def UlmsTheorem.layerSuccIncl (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : ↥(ulmSubgroup p (Order.succ α)) →+ ↥(ulmSubgroup p α)

G_(α+1) as a subgroup of G_α.

Equations

• UlmsTheorem.layerSuccIncl p α = (UlmsTheorem.ulmSubgroup p (Order.succ α)).subtype.codRestrict (UlmsTheorem.ulmSubgroup p α) ⋯

noncomputable def UlmsTheorem.layerQuotient (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Type u_1

The quotient G_α / G_{α+1}. This is useful auxiliary filtration data, but it is not the classical Ulm invariant.

Equations

• UlmsTheorem.layerQuotient p α = (↥(UlmsTheorem.ulmSubgroup p α) ⧸ AddSubgroup.comap (UlmsTheorem.ulmSubgroup p α).subtype (UlmsTheorem.ulmSubgroup p (Order.succ α)))

@[instance_reducible]

noncomputable instance UlmsTheorem.instAddCommGroupLayerQuotient (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : AddCommGroup (layerQuotient p α)

Equations

• UlmsTheorem.instAddCommGroupLayerQuotient p α = id inferInstance

theorem UlmsTheorem.layerQuotient_orderOf_dvd_p (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (x : layerQuotient p α) : p • x = 0

Every element of G_α / G_{α+1} has order p.

@[instance_reducible]

noncomputable instance UlmsTheorem.layerQuotientModule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Module (ZMod p) (layerQuotient p α)

Equations

• UlmsTheorem.layerQuotientModule p α = AddCommGroup.zmodModule ⋯

noncomputable def UlmsTheorem.layerInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Cardinal.{u_1}

The raw filtration-layer rank dim_{ℤ/pℤ}(G_α / G_{α+1}).

Equations

• UlmsTheorem.layerInvariant p α = Module.rank (ZMod p) (UlmsTheorem.layerQuotient p α)

The classical Ulm quotient P_α / P_{α+1}

noncomputable def UlmsTheorem.ulmDenSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Submodule (ZMod p) ↥(pSocleAt p α)

P_(α+1) as a ZMod p-submodule of P_α.

Equations

• UlmsTheorem.ulmDenSubmodule p α = (AddSubgroup.toZModSubmodule p) (UlmsTheorem.pSocleAtSuccSubgroupOf p α)

@[reducible, inline]

abbrev UlmsTheorem.ulmQuotient (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Type u_1

The classical Ulm quotient at α: P_α / P_{α+1}.

Equations

• UlmsTheorem.ulmQuotient p α = (↥(UlmsTheorem.pSocleAt p α) ⧸ UlmsTheorem.ulmDenSubmodule p α)

theorem UlmsTheorem.ulmQuotient_orderOf_dvd_p (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (x : ulmQuotient p α) : p • x = 0

Every element of the classical Ulm quotient has order p.

noncomputable def UlmsTheorem.ulmInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : Cardinal.{u_1}

The classical Ulm invariant f_G(α) = dim_{ℤ/pℤ}(P_α / P_{α+1}).

Equations

• UlmsTheorem.ulmInvariant p α = Module.rank (ZMod p) (UlmsTheorem.ulmQuotient p α)

Hill, marked-graded, and overhang invariants

noncomputable def UlmsTheorem.markedGradedDen (p : ℕ) {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : AddSubgroup ↥(pSocleAt p α)

The marked-graded denominator P_(α+1) + (S ∩ P_α), viewed as a subgroup of P_α.

Equations

• UlmsTheorem.markedGradedDen p S α = AddSubgroup.comap (UlmsTheorem.pSocleAt p α).subtype (UlmsTheorem.pSocleAt p (Order.succ α) ⊔ S ⊓ UlmsTheorem.pSocleAt p α)

noncomputable def UlmsTheorem.markedGradedSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Submodule (ZMod p) ↥(pSocleAt p α)

The marked-graded denominator as a ZMod p-submodule of P_α.

Equations

• UlmsTheorem.markedGradedSubmodule p S α = (AddSubgroup.toZModSubmodule p) (UlmsTheorem.markedGradedDen p S α)

@[reducible, inline]

abbrev UlmsTheorem.markedGradedQuotient (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Type u_1

The marked-graded socle space P_α / (P_(α+1) + (S ∩ P_α)).

Equations

• UlmsTheorem.markedGradedQuotient p S α = (↥(UlmsTheorem.pSocleAt p α) ⧸ UlmsTheorem.markedGradedSubmodule p S α)

noncomputable def UlmsTheorem.markedGradedInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Cardinal.{u_1}

The rank of the marked-graded socle space dim_(ZMod p) P_α / (P_(α+1) + (S ∩ P_α)).

Equations

• UlmsTheorem.markedGradedInvariant p S α = Module.rank (ZMod p) (UlmsTheorem.markedGradedQuotient p S α)

theorem UlmsTheorem.markedGradedInvariant_bot (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : markedGradedInvariant p ⊥ α = ulmInvariant p α

With no marked subgroup, the marked-graded invariant is the ordinary Ulm invariant.

noncomputable def UlmsTheorem.hillDen (p : ℕ) {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : AddSubgroup ↥(pSocleAt p α)

The Fuchs/Walker Hill denominator P_α ∩ (S + G_(α+1)), viewed inside P_α.

Equations

• UlmsTheorem.hillDen p S α = AddSubgroup.comap (UlmsTheorem.pSocleAt p α).subtype (UlmsTheorem.pSocleAt p α ⊓ (S ⊔ UlmsTheorem.ulmSubgroup p (Order.succ α)))

noncomputable def UlmsTheorem.hillSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Submodule (ZMod p) ↥(pSocleAt p α)

The Hill denominator as a ZMod p-submodule of P_α.

Equations

• UlmsTheorem.hillSubmodule p S α = (AddSubgroup.toZModSubmodule p) (UlmsTheorem.hillDen p S α)

@[reducible, inline]

abbrev UlmsTheorem.hillQuotient (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Type u_1

The Fuchs/Walker Hill (relative Ulm) space P_α / (P_α ∩ (S + G_(α+1))).

Equations

• UlmsTheorem.hillQuotient p S α = (↥(UlmsTheorem.pSocleAt p α) ⧸ UlmsTheorem.hillSubmodule p S α)

noncomputable def UlmsTheorem.hillInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Cardinal.{u_1}

The Fuchs/Walker Hill invariant. Its nonzero classes are exactly the order-p, exact-height-α elements proper with respect to S.

Equations

• UlmsTheorem.hillInvariant p S α = Module.rank (ZMod p) (UlmsTheorem.hillQuotient p S α)

theorem UlmsTheorem.hillInvariant_bot (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) : hillInvariant p ⊥ α = ulmInvariant p α

With no marked subgroup, the Hill invariant is the ordinary Ulm invariant.

@[reducible, inline]

noncomputable abbrev UlmsTheorem.relativeUlmDen (p : ℕ) {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : AddSubgroup ↥(pSocleAt p α)

BCM's "relative Ulm" terminology names the same quotient as the Fuchs/Walker Hill invariant.

Equations

• UlmsTheorem.relativeUlmDen p S α = UlmsTheorem.hillDen p S α

@[reducible, inline]

noncomputable abbrev UlmsTheorem.relativeUlmSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Submodule (ZMod p) ↥(pSocleAt p α)

The relative Ulm submodule, in the equivalent Hill-invariant formulation.

Equations

• UlmsTheorem.relativeUlmSubmodule p S α = UlmsTheorem.hillSubmodule p S α

@[reducible, inline]

abbrev UlmsTheorem.relativeUlmQuotient (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Type u_1

The relative Ulm quotient by the Hill denominator.

Equations

• UlmsTheorem.relativeUlmQuotient p S α = UlmsTheorem.hillQuotient p S α

@[reducible, inline]

noncomputable abbrev UlmsTheorem.relativeUlmInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Cardinal.{u_1}

The relative Ulm invariant, expressed as the rank of the Hill quotient.

Equations

• UlmsTheorem.relativeUlmInvariant p S α = UlmsTheorem.hillInvariant p S α

theorem UlmsTheorem.markedGradedSubmodule_le_hillSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : markedGradedSubmodule p S α ≤ hillSubmodule p S α

The marked-graded denominator is contained in the Hill denominator.

theorem UlmsTheorem.ulmDenSubmodule_le_hillSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : ulmDenSubmodule p α ≤ hillSubmodule p S α

The ordinary Ulm denominator P_(α+1) is contained in the Hill denominator.

noncomputable def UlmsTheorem.relativeOccupiedSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Submodule (ZMod p) (ulmQuotient p α)

The subspace of the ordinary Ulm layer occupied by the marked subgroup S.

Equations

• UlmsTheorem.relativeOccupiedSubmodule p S α = Submodule.map (UlmsTheorem.ulmDenSubmodule p α).mkQ (UlmsTheorem.hillSubmodule p S α)

noncomputable def UlmsTheorem.occupiedQuotientEquivRelative (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : (ulmQuotient p α ⧸ relativeOccupiedSubmodule p S α) ≃ₗ[ZMod p] hillQuotient p S α

Quotienting the ordinary Ulm layer by its occupied subspace gives the relative Ulm space.

Equations

• UlmsTheorem.occupiedQuotientEquivRelative p S α = (UlmsTheorem.ulmDenSubmodule p α).quotientQuotientEquivQuotient (UlmsTheorem.hillSubmodule p S α) ⋯

theorem UlmsTheorem.relativeUlmInvariant_add_occupiedInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : relativeUlmInvariant p S α + Module.rank (ZMod p) ↥(relativeOccupiedSubmodule p S α) = ulmInvariant p α

The occupied-space equation underlying the Barwise–Eklof room criterion: relative room + occupied = the ordinary Ulm invariant.

noncomputable def UlmsTheorem.overhangSubmodule (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Submodule (ZMod p) (markedGradedQuotient p S α)

The BCM overhang, as the kernel subspace inside the marked-graded quotient. This ordinal-indexed definition extends BCM's finite-level construction.

Equations

• UlmsTheorem.overhangSubmodule p S α = Submodule.map (UlmsTheorem.markedGradedSubmodule p S α).mkQ (UlmsTheorem.hillSubmodule p S α)

noncomputable def UlmsTheorem.overhangInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Cardinal.{u_1}

The dimension of the BCM overhang space.

Equations

• UlmsTheorem.overhangInvariant p S α = Module.rank (ZMod p) ↥(UlmsTheorem.overhangSubmodule p S α)

noncomputable def UlmsTheorem.markedGradedToHill (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : markedGradedQuotient p S α →ₗ[ZMod p] hillQuotient p S α

The canonical quotient map from the marked-graded space onto the Hill space.

Equations

• UlmsTheorem.markedGradedToHill p S α = Submodule.factor ⋯

theorem UlmsTheorem.markedGradedToHill_surjective (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : Function.Surjective ⇑(markedGradedToHill p S α)

theorem UlmsTheorem.hillInvariant_add_overhangInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : hillInvariant p S α + overhangInvariant p S α = markedGradedInvariant p S α

BCM's exact-sequence dimension equation: the marked-graded invariant is the Hill invariant plus the overhang dimension.

theorem UlmsTheorem.relativeUlmInvariant_add_overhangInvariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (S : AddSubgroup G) (α : Ordinal.{u_2}) : relativeUlmInvariant p S α + overhangInvariant p S α = markedGradedInvariant p S α

The same BCM equation in relative-Ulm terminology.

Ulm length

noncomputable def UlmsTheorem.ulmLength (p : ℕ) {G : Type u_1} [AddCommGroup G] : Ordinal.{0}

The least ordinal α at which p^α·G = 0, or zero if no such ordinal exists. Reducedness guarantees that this infimum is attained.

Equations

• UlmsTheorem.ulmLength p = sInf {α : Ordinal.{0} | UlmsTheorem.ulmSubgroup p α = ⊥}

theorem UlmsTheorem.ulmLength.exists_zero (p : ℕ) {G : Type u_1} [AddCommGroup G] (hred' : IsPReduced p G) : ∃ (α : Ordinal.{0}), ulmSubgroup p α = ⊥

The set {α | p^α·G = 0} is nonempty for a reduced p-group.

theorem UlmsTheorem.ulmLength.at_ulmLength (p : ℕ) {G : Type u_1} [AddCommGroup G] (hred : IsPReduced p G) : ulmSubgroup p (ulmLength p) = ⊥

p^(ulmLength)·G = 0.

theorem UlmsTheorem.ulmLength.inv_zero_of_ge (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (hred : IsPReduced p G) (α : Ordinal.{0}) (hα : ulmLength p ≤ α) : ulmInvariant p α = 0

Ulm invariants vanish above the Ulm length.

Ulm sequence as a function ℕ → Cardinal (for successor-length groups)

noncomputable def UlmsTheorem.tailInvariants (p : ℕ) [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddCommGroup G] (γ : Ordinal.{u_2}) (n : ℕ) : Fin n → Cardinal.{u_1}

For groups of Ulm length ω·γ + n, the tail Ulm invariants are those at ω·γ, ω·γ+1, ..., ω·γ+(n-1).

Equations

• UlmsTheorem.tailInvariants p γ n k = UlmsTheorem.ulmInvariant p (Ordinal.omega0 * γ + ↑↑k)