Results about p-groups

Mathlib's IsPGroup.to_quotient says that every quotient of a p-group is again a p-group. This file records the complementary behaviour, in which the group is fixed and the normal subgroup varies: how the property IsPGroup p (G ⧸ N) of the quotient behaves under intersection of normal subgroups and under preimage along a group homomorphism. It also records closure of p-groups under binary and finite products and under extensions, and their disjointness from subgroups of order prime to p.

The two quotient statements are group-theoretic, with no topology. They are what makes the family of normal subgroups with p-group quotient usable: IsPGroup.quotient_inf says the family is closed under binary intersection, hence downward directed, and IsPGroup.quotient_comap says it is contravariantly functorial. The profinite development uses the first to run a compactness argument on the family of open normal subgroups with p-group quotient, and the second to see that a homomorphism into a pro-p group kills their intersection.

Main results

• IsPGroup.exists_pow_pow_eq_one_map: every element in the image of a p-group under a monoid homomorphism has p-power order.
• IsPGroup.prod: a product of two p-groups is a p-group.
• IsPGroup.pi: a finite product of p-groups is a p-group.
• IsPGroup.of_subgroup_of_quotient: an extension of a p-group by a p-group is a p-group.
• TauCeti.disjoint_of_not_dvd_natCard_of_isPGroup: a p-group meets a subgroup of order prime to p trivially.
• IsPGroup.subsingleton_of_coprime, IsPGroup.subsingleton_of_ne: a group that is a p-group and a q-group for coprime p, q, in particular for distinct primes, is trivial.
• IsPGroup.smul_zmod_eq_self: a p-group acts trivially on the additive group ZMod p.
• TauCeti.exists_isPGroup_quotient_notMem_of_pow_pow_eq_one: in a finite commutative group, an element of p-power order survives in some p-group quotient.
• IsPGroup.index_eq_prime_of_isCoatom: a maximal subgroup of a finite p-group has index p.
• IsPGroup.exists_ne_one_le_centralizer: a nontrivial finite p-subgroup lies in the centralizer of one of its nontrivial elements.
• IsPGroup.quotient_inf: if G ⧸ M and G ⧸ N are p-groups, so is G ⧸ (M ⊓ N).
• IsPGroup.quotient_comap: if H ⧸ N is a p-group and f : G →* H, then G ⧸ N.comap f is a p-group.

theorem IsPGroup.exists_pow_pow_eq_one_map {p : ℕ} {G : Type u_1} [Group G] {M : Type u_3} [Monoid M] (hG : IsPGroup p G) (f : G →* M) (g : G) : ∃ (n : ℕ), f g ^ p ^ n = 1

Every element in the image of a p-group under a monoid homomorphism has p-power order. A homomorphism preserves powers and 1, so IsPGroup.exists_pow_pow_eq_one transports along it; this is what supplies the power-order hypothesis of a representation of a p-group.

theorem IsPGroup.prod {p : ℕ} {G : Type u_1} [Group G] {H : Type u_2} [Group H] (hG : IsPGroup p G) (hH : IsPGroup p H) : IsPGroup p (G × H)

A product of two p-groups is a p-group.

theorem IsPGroup.pi {p : ℕ} {ι : Type u_3} [Finite ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] (hG : ∀ (i : ι), IsPGroup p (G i)) : IsPGroup p ((i : ι) → G i)

A product of finitely many p-groups is a p-group.

theorem IsPGroup.of_subgroup_of_quotient {p : ℕ} {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] (hN : IsPGroup p ↥N) (hQ : IsPGroup p (G ⧸ N)) : IsPGroup p G

An extension of a p-group by a p-group is a p-group: if a normal subgroup N of G and the quotient G ⧸ N are both p-groups, then so is G. This is the converse of IsPGroup.to_subgroup and IsPGroup.to_quotient taken together.

theorem TauCeti.disjoint_of_not_dvd_natCard_of_isPGroup {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] {C Q : Subgroup G} (hC : ¬p ∣ Nat.card ↥C) (hQ : IsPGroup p ↥Q) : Disjoint C Q

A p-group meets a subgroup of order prime to p trivially.

theorem IsPGroup.subsingleton_of_coprime {p : ℕ} {G : Type u_1} [Group G] {q : ℕ} (hp : IsPGroup p G) (hq : IsPGroup q G) (hpq : p.Coprime q) : Subsingleton G

A group that is a p-group and a q-group for coprime p and q is trivial.

theorem IsPGroup.subsingleton_of_ne {p : ℕ} {G : Type u_1} [Group G] {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : IsPGroup p G) (hq : IsPGroup q G) (hpq : p ≠ q) : Subsingleton G

A group that is a p-group and a q-group for two distinct primes is trivial.

theorem IsPGroup.smul_zmod_eq_self {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : IsPGroup p G) [DistribMulAction G (ZMod p)] (g : G) (m : ZMod p) : g • m = m

A p-group acts trivially on the additive group ZMod p, for p prime: every additive action of g on ZMod p is multiplication by g • 1, an element fixed by the p-th power map, and g has p-power order.

theorem TauCeti.exists_isPGroup_quotient_notMem_of_pow_pow_eq_one {p : ℕ} {A : Type u_3} [Group A] [IsMulCommutative A] [Finite A] [hp : Fact (Nat.Prime p)] {a : A} {k : ℕ} (ha : a ^ p ^ k = 1) (ha1 : a ≠ 1) : ∃ (N : Subgroup A), IsPGroup p (A ⧸ N) ∧ a ∉ N

In a finite commutative group, a nontrivial element of p-power order survives in some p-group quotient: there is a subgroup N with A ⧸ N a p-group and a ∉ N. The subgroup is the kernel of raising to the power ordCompl[p] (Nat.card A), the part of the group order prime to p.

theorem IsPGroup.index_eq_prime_of_isCoatom {p : ℕ} {G : Type u_1} [Group G] [Finite G] [hp : Fact (Nat.Prime p)] (hG : IsPGroup p G) {H : Subgroup G} (hH : IsCoatom H) : H.index = p

A maximal subgroup of a finite p-group has index p.

theorem IsPGroup.exists_ne_one_le_centralizer {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] {P : Subgroup G} [Finite ↥P] (hP : IsPGroup p ↥P) (hne : P ≠ ⊥) : ∃ g ∈ P, g ≠ 1 ∧ P ≤ Subgroup.centralizer {g}

A nontrivial finite p-subgroup P of G lies in the centralizer of one of its nontrivial elements, namely of any nontrivial element of the centre of P.

theorem IsPGroup.quotient_inf {p : ℕ} {G : Type u_1} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (hM : IsPGroup p (G ⧸ M)) (hN : IsPGroup p (G ⧸ N)) : IsPGroup p (G ⧸ M ⊓ N)

The normal subgroups of G with p-group quotient are closed under binary intersection.

theorem IsPGroup.quotient_comap {p : ℕ} {G : Type u_1} [Group G] {H : Type u_2} [Group H] {N : Subgroup H} [N.Normal] (hN : IsPGroup p (H ⧸ N)) (f : G →* H) : IsPGroup p (G ⧸ Subgroup.comap f N)

The preimage of a normal subgroup with p-group quotient also has p-group quotient.