Subgroup-level algebra for reduced abelian p-groups

This file contains the basic subgroup constructions used throughout the development: the natural-number powers pPow and the image-of-multiplication construction pImage.

Natural-number Ulm subgroups

def UlmsTheorem.pPow (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) : AddSubgroup G

p^n·G = { p^n • y | y : G }.

Equations

• UlmsTheorem.pPow p n = { carrier := {x : G | ∃ (y : G), p ^ n • y = x}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem UlmsTheorem.pPow_mem_iff (p : ℕ) {G : Type u_1} [AddCommGroup G] (x : G) (n : ℕ) : x ∈ pPow p n ↔ ∃ (y : G), p ^ n • y = x

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

theorem UlmsTheorem.pPow_succ_le (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) : pPow p (n + 1) ≤ pPow p n

theorem UlmsTheorem.pPow_antitone (p : ℕ) {G : Type u_1} [AddCommGroup G] : Antitone fun (n : ℕ) => pPow p n

theorem UlmsTheorem.pPow_succ_eq (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) : ↑(pPow p (n + 1)) = {x : G | ∃ y ∈ pPow p n, p • y = x}

p-image of a subgroup

def UlmsTheorem.pImage (p : ℕ) {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : AddSubgroup G

{ p • y | y ∈ H } as a subgroup of G.

Equations

• UlmsTheorem.pImage p H = { carrier := {x : G | ∃ y ∈ H, p • y = x}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem UlmsTheorem.mem_pImage (p : ℕ) {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) (x : G) : x ∈ pImage p H ↔ ∃ y ∈ H, p • y = x

theorem UlmsTheorem.pImage_pPow (p : ℕ) {G : Type u_1} [AddCommGroup G] (n : ℕ) : pImage p (pPow p n) = pPow p (n + 1)