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.
• IsZGroup.isCyclic_commutator: a finite Z-group has cyclic commutator subgroup.

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 IsPGroup.isCyclic_of_isZGroup {G : Type u_1} [Group G] [IsZGroup G] {p : ℕ} [Fact (Nat.Prime p)] {P : Subgroup G} (hP : IsPGroup p ↥P) : 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.commutator_lt (G : Type u_1) [Group G] [Finite G] [IsZGroup G] [Nontrivial G] : commutator G < ⊤

instance IsZGroup.instIsSolvableOfFinite {G : Type u_1} [Group G] [Finite G] [IsZGroup G] : IsSolvable G

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.

theorem IsZGroup.isCyclic_commutator (G : Type u_1) [Group G] [Finite G] [IsZGroup G] : IsCyclic ↥(commutator G)

A finite Z-group has cyclic commutator subgroup.

theorem IsZGroup.isZGroup_of_coprime {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [Group G] [Group G'] [Group G''] {f : G →* G'} {f' : G' →* G''} [Finite G] [IsZGroup G] [IsZGroup G''] (h_le : f'.ker ≤ f.range) (h_cop : (Nat.card G).Coprime (Nat.card G'')) : IsZGroup G'

An extension of coprime Z-groups is a Z-group.