The index-p subgroups of an abelian group of exponent p separate its points

An abelian group G all of whose elements satisfy g ^ p = 1, for a prime p, is an elementary abelian p-group, that is an 𝔽_p-vector space written multiplicatively. Its subgroups of index p are the hyperplanes, and the point of this file is that they separate points: every σ ≠ 1 is avoided by some index-p subgroup, equivalently the intersection of all of them — the Frattini subgroup — is trivial. More generally, a subgroup N avoiding σ extends to an index-p subgroup still avoiding σ, which is the form needed to separate σ from a given subgroup rather than from 1.

The proof avoids setting up the vector-space structure. By Zorn's lemma, take H ⊇ N maximal among the subgroups not containing σ. For b ∉ H the subgroup H ⊔ ⟨b⟩ is strictly larger, so by maximality it contains σ; as G is commutative this reads σ = h * b ^ n with h ∈ H, so the class of σ lies in the cyclic group generated by the class of b in G ⧸ H. That cyclic group has prime order p, and in a group of prime order every nontrivial element is a generator, so the class of b lies in turn in the group generated by the class of σ. Hence G ⧸ H is generated by the class of σ, an element of order p, and H has index p.

Commutativity is a genuine hypothesis for odd p — a group of exponent 3 need not be abelian — but for p = 2 it is automatic (Commute.of_orderOf_dvd_two), which is how the exponent-two corollary below drops it.

Main results

• TauCeti.zpowers_eq_zpowers_of_mem_zpowers: a nontrivial element of the cyclic subgroup generated by an element of prime order generates that subgroup.
• TauCeti.exists_le_index_eq_notMem_of_exponent_dvd: in a commutative group of exponent dividing a prime p, every subgroup avoiding σ lies in a subgroup of index p avoiding σ.
• TauCeti.exists_index_eq_notMem_of_exponent_dvd: in such a group every σ ≠ 1 lies outside some subgroup of index p.
• TauCeti.exists_le_index_eq_two_notMem_of_exponent_dvd_two and TauCeti.exists_index_eq_two_notMem_of_exponent_dvd_two: the case p = 2, where commutativity is automatic.

theorem TauCeti.zpowers_eq_zpowers_of_mem_zpowers {G : Type u_1} [Group G] {p : ℕ} (hp : Nat.Prime p) {y z : G} (hpow : y ^ p = 1) (hz : z ≠ 1) (hzy : z ∈ Subgroup.zpowers y) : Subgroup.zpowers z = Subgroup.zpowers y

If y ^ p = 1 for a prime p, then every nontrivial element z of the cyclic subgroup generated by y generates that subgroup: ⟨y⟩ has order p, and a group of prime order is generated by each of its nontrivial elements.

theorem TauCeti.exists_le_index_eq_notMem_of_exponent_dvd {G : Type u_1} [Group G] {p : ℕ} [IsMulCommutative G] (hp : Nat.Prime p) (hexp : Monoid.exponent G ∣ p) {N : Subgroup G} {σ : G} (hσ : σ ∉ N) : ∃ (H : Subgroup G), N ≤ H ∧ H.index = p ∧ σ ∉ H

Index-p subgroups separate a point from a subgroup in exponent p. In a commutative group all of whose elements satisfy g ^ p = 1, for p prime, every subgroup N avoiding an element σ lies in some subgroup of index p that still avoids σ.

Equivalently: every subgroup is the intersection of the index-p subgroups containing it.

theorem TauCeti.exists_index_eq_notMem_of_exponent_dvd {G : Type u_1} [Group G] {p : ℕ} [IsMulCommutative G] (hp : Nat.Prime p) (hexp : Monoid.exponent G ∣ p) {σ : G} (hσ : σ ≠ 1) : ∃ (H : Subgroup G), H.index = p ∧ σ ∉ H

Index-p subgroups separate the points of an abelian group of exponent p. In a commutative group all of whose elements satisfy g ^ p = 1, for p prime, every σ ≠ 1 lies outside some subgroup of index p.

Equivalently: the intersection of the index-p subgroups — the Frattini subgroup of an elementary abelian p-group — is trivial.

theorem TauCeti.exists_le_index_eq_two_notMem_of_exponent_dvd_two {G : Type u_1} [Group G] (hexp : Monoid.exponent G ∣ 2) {N : Subgroup G} {σ : G} (hσ : σ ∉ N) : ∃ (H : Subgroup G), N ≤ H ∧ H.index = 2 ∧ σ ∉ H

Index-two subgroups separate a point from a subgroup in exponent two. In a group all of whose elements square to 1, every subgroup N avoiding an element σ lies in some subgroup of index 2 that still avoids σ.

This is the case p = 2 of TauCeti.exists_le_index_eq_notMem_of_exponent_dvd, where commutativity is not an extra hypothesis: a group of exponent two is automatically abelian.

theorem TauCeti.exists_index_eq_two_notMem_of_exponent_dvd_two {G : Type u_1} [Group G] (hexp : Monoid.exponent G ∣ 2) {σ : G} (hσ : σ ≠ 1) : ∃ (H : Subgroup G), H.index = 2 ∧ σ ∉ H

Index-two subgroups separate the points of a group of exponent two. In a group all of whose elements square to 1, every σ ≠ 1 lies outside some subgroup of index 2.