Additive groups in which every element has p-power order

Mathlib's IsPGroup is stated for multiplicative groups. This file records the facts about a p-primary additive group A, one in which every element a satisfies p ^ k • a = 0 for some k, that the theory of pro-p actions on finite discrete coefficient modules needs, in additive notation: the order of a finite such group is a power of p, namely p ^ padicValNat p (Nat.card A), and is divisible by p when the group is nontrivial; a nonzero element of p-power order has a nonzero multiple annihilated by p, a statement about natural multiples that holds in any additive monoid; a monoid additively equivalent to ZMod p is p-primary; a subgroup of a p-primary group is p-primary; and adjoining to a subgroup N an element x ∉ N with p • x ∈ N multiplies the order of N by p.

Main results

• TauCeti.prime_dvd_natCard_of_forall_exists_nsmul_eq_zero: p ∣ Nat.card A for a nontrivial finite p-primary additive group A.
• TauCeti.natCard_eq_pow_padicValNat_of_forall_exists_nsmul_eq_zero: Nat.card A = p ^ padicValNat p (Nat.card A) for a finite p-primary additive group A.
• TauCeti.exists_nsmul_pow_ne_zero_nsmul_nsmul_pow_eq_zero: a nonzero a with p ^ k • a = 0 has a nonzero multiple p ^ n • a with p • p ^ n • a = 0.
• TauCeti.forall_exists_nsmul_eq_zero_of_addEquiv_zmod: an additive monoid additively equivalent to ZMod p is p-primary.
• AddSubgroup.forall_exists_nsmul_eq_zero: an additive subgroup of a p-primary additive group is p-primary.
• TauCeti.subquotientEquivZModOfEqSupZmultiples: adjoining x ∉ N with p • x ∈ N gives a quotient additively equivalent to ZMod p, sending the class of x to 1.
• TauCeti.natCard_sup_zmultiples_of_nsmul_mem: |N ⊔ zmultiples x| = p * |N| when x ∉ N and p • x ∈ N.

theorem TauCeti.exists_nsmul_pow_ne_zero_nsmul_nsmul_pow_eq_zero {p : ℕ} {A : Type u_1} [AddMonoid A] {a : A} (ha : a ≠ 0) {k : ℕ} (hk : p ^ k • a = 0) : ∃ (n : ℕ), p ^ n • a ≠ 0 ∧ p • p ^ n • a = 0

A nonzero element a with p ^ k • a = 0 has a nonzero multiple p ^ n • a annihilated by p, that is, with p • p ^ n • a = 0.

theorem TauCeti.forall_exists_nsmul_eq_zero_of_addEquiv_zmod {p : ℕ} {A : Type u_1} [AddMonoid A] (e : A ≃+ ZMod p) (a : A) : ∃ (k : ℕ), p ^ k • a = 0

An additive monoid additively equivalent to ZMod p is p-primary: p itself annihilates every element.

theorem AddSubgroup.forall_exists_nsmul_eq_zero {p : ℕ} {A : Type u_1} [AddGroup A] (N : AddSubgroup A) (h : ∀ (a : A), ∃ (k : ℕ), p ^ k • a = 0) (x : ↥N) : ∃ (k : ℕ), p ^ k • x = 0

An additive subgroup of a p-primary additive group is p-primary: every element of N has p-power order when every element of the ambient group A does.

theorem TauCeti.prime_dvd_natCard_of_forall_exists_nsmul_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Type u_1} [AddGroup A] [Finite A] [Nontrivial A] (htors : ∀ (a : A), ∃ (k : ℕ), p ^ k • a = 0) : p ∣ Nat.card A

A nontrivial finite additive group in which every element has p-power order has order divisible by p.

theorem TauCeti.natCard_eq_pow_padicValNat_of_forall_exists_nsmul_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Type u_1} [AddGroup A] [Finite A] (htors : ∀ (a : A), ∃ (k : ℕ), p ^ k • a = 0) : Nat.card A = p ^ padicValNat p (Nat.card A)

A finite additive group in which every element has p-power order has order the power of p given by the p-adic valuation of its order.

noncomputable def TauCeti.subquotientEquivZModOfEqSupZmultiples {p : ℕ} [Fact (Nat.Prime p)] {M : Type u_1} [AddCommGroup M] {N K : AddSubgroup M} {x : M} (hgen : K = N ⊔ AddSubgroup.zmultiples x) (hx : x ∉ N) (hpx : p • x ∈ N) : ↥K ⧸ N.addSubgroupOf K ≃+ ZMod p

If K is obtained from N by adjoining x ∉ N with p • x ∈ N, then K ⧸ N is additively equivalent to ZMod p. The equivalence sends the class of x to 1 (see zmodAddEquivOfGenerator_symm_apply_generator).

Equations

• TauCeti.subquotientEquivZModOfEqSupZmultiples hgen hx hpx = (zmodAddEquivOfGenerator ⋯ ⋯).symm

theorem TauCeti.natCard_sup_zmultiples_of_nsmul_mem {p : ℕ} [Fact (Nat.Prime p)] {M : Type u_1} [AddCommGroup M] {N : AddSubgroup M} {x : M} (hx : x ∉ N) (hpx : p • x ∈ N) : Nat.card ↥(N ⊔ AddSubgroup.zmultiples x) = p * Nat.card ↥N

Adjoining to a subgroup N an element x ∉ N with p • x ∈ N multiplies its order by p: the quotient (N ⊔ zmultiples x) ⧸ N is cyclic of order p, generated by the class of x.