Z-Groups

A Z-group is a group whose Sylow subgroups are all cyclic.

Main definitions

• IsZGroup G: a predicate stating that all Sylow subgroups of G are cyclic.

Main results

• IsZGroup.isCyclic_abelianization: a finite Z-group has cyclic abelianization.

TODO: Show that if G is a Z-group with commutator subgroup G', then G = G' ⋊ G/G' where G' and G/G' are cyclic of coprime orders.

class IsZGroup (G : Type u_1) [Group G] : Prop

A Z-group is a group whose Sylow subgroups are all cyclic.

• isZGroup (p : ℕ) : Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P

theorem isZGroup_iff (G : Type u_1) [Group G] : IsZGroup G ↔ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P

instance IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime {G : Type u_1} [Group G] [IsZGroup G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) : IsCyclic ↥↑P

theorem IsZGroup.of_squarefree {G : Type u_1} [Group G] (hG : Squarefree (Nat.card G)) : IsZGroup G

theorem IsZGroup.of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} [hG' : IsZGroup G'] (hf : Function.Injective ⇑f) : IsZGroup G

instance IsZGroup.instSubtypeMemSubgroup {G : Type u_1} [Group G] [IsZGroup G] (H : Subgroup G) : IsZGroup ↥H

theorem IsZGroup.of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} [Finite G] [hG : IsZGroup G] (hf : Function.Surjective ⇑f) : IsZGroup G'

instance IsZGroup.instQuotientSubgroupOfFinite {G : Type u_1} [Group G] [Finite G] [IsZGroup G] (H : Subgroup G) [H.Normal] : IsZGroup (G ⧸ H)

theorem IsZGroup.exponent_eq_card (G : Type u_1) [Group G] [Finite G] [IsZGroup G] : Monoid.exponent G = Nat.card G

instance IsZGroup.instIsCyclicOfFiniteOfIsNilpotent {G : Type u_1} [Group G] [Finite G] [IsZGroup G] [hG : Group.IsNilpotent G] : IsCyclic G

instance IsZGroup.isCyclic_abelianization {G : Type u_1} [Group G] [Finite G] [IsZGroup G] : IsCyclic (Abelianization G)

A finite Z-group has cyclic abelianization.