Documentation

LeanPool.UlmsTheorem.PGroups.UlmSubgroups

Ordinal Ulm subgroups #

This file contains the transfinite Ulm filtration ulmSubgroup and its basic structural lemmas.

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

p^α·G by transfinite recursion: p^0·G = G, p^(α+1)·G = {p•x | x ∈ p^α·G}, and p^λ·G = ⋂_{β<λ} p^β·G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem UlmsTheorem.ulmSubgroup_zero (p : ℕ) {G : Type u_1} [AddCommGroup G] :
    ulmSubgroup p 0 = ⊤
    source
    theorem UlmsTheorem.ulmSubgroup_add_one (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) :
    ulmSubgroup p (α + 1) = pImage p (ulmSubgroup p α)
    source
    theorem UlmsTheorem.ulmSubgroup_succ (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) :
    ulmSubgroup p (Order.succ α) = pImage p (ulmSubgroup p α)
    source
    theorem UlmsTheorem.ulmSubgroup_limit (p : ℕ) {G : Type u_1} [AddCommGroup G] (o : Ordinal.{u_2}) (ho : Order.IsSuccLimit o) :
    ulmSubgroup p o = ⨅ (β : Ordinal.{u_2}), ⨅ (_ : β < o), ulmSubgroup p β
    source
    theorem UlmsTheorem.mem_ulmSubgroup_succ_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (x : G) :
    x ∈ ulmSubgroup p (Order.succ α) ↔ ∃ y ∈ ulmSubgroup p α, p • y = x
    source
    @[simp]
    theorem UlmsTheorem.mem_ulmSubgroup_add_one_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (x : G) :
    x ∈ ulmSubgroup p (α + 1) ↔ ∃ y ∈ ulmSubgroup p α, p • y = x
    source
    theorem UlmsTheorem.mem_ulmSubgroup_limit_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] {o : Ordinal.{u_2}} (ho : Order.IsSuccLimit o) (x : G) :
    x ∈ ulmSubgroup p o ↔ ∀ β < o, x ∈ ulmSubgroup p β
    source
    theorem UlmsTheorem.ulmSubgroup_antitone (p : ℕ) {G : Type u_1} [AddCommGroup G] :
    Antitone fun (α : Ordinal.{u_2}) => ulmSubgroup p α
    source
    theorem UlmsTheorem.ulmSubgroup_nat (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) :
    ulmSubgroup p ↑n = pPow p n
    source
    theorem UlmsTheorem.mem_ulmSubgroup_nat_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) (x : G) :
    x ∈ ulmSubgroup p ↑n ↔ ∃ (y : G), p ^ n • y = x
    source
    theorem UlmsTheorem.mem_ulmSubgroup_add_nat_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (n : ℕ) (x : G) :
    x ∈ ulmSubgroup p (α + ↑n) ↔ ∃ y ∈ ulmSubgroup p α, p ^ n • y = x
    source
    theorem UlmsTheorem.ulmSubgroup_add_nat (p : ℕ) {G : Type u_1} [AddCommGroup G] (α : Ordinal.{u_2}) (n : ℕ) :
    ↑(ulmSubgroup p (α + ↑n)) = {x : G | ∃ y ∈ ulmSubgroup p α, p ^ n • y = x}
    source
    theorem UlmsTheorem.map_ulmSubgroup_le (p : ℕ) {G : Type u_1} [AddCommGroup G] {H : Type u_2} [AddCommGroup H] (φ : G →+ H) (α : Ordinal.{u_3}) :
    AddSubgroup.map φ (ulmSubgroup p α) ≤ ulmSubgroup p α
    source
    theorem UlmsTheorem.add_zsmul_mem_iff_of_mem (p : ℕ) {G : Type u_1} [AddCommGroup G] {β : Ordinal.{0}} {x c : G} (hx : x ∈ ulmSubgroup p β) (n : ℤ) :
    c + n • x ∈ ulmSubgroup p β ↔ c ∈ ulmSubgroup p β

    Translating by a multiple of an element already in G_β does not change membership in G_β.