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.
• IsZGroup.coprime_commutator_index: the commutator subgroup of a finite Z-group is a Hall-subgroup (the commutator subgroup has cardinality coprime to its index).

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.instOfIsCyclic {G : Type u_1} [Group G] [IsCyclic G] : IsZGroup G

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 IsPGroup.smul_mul_inv_trivial_or_surjective {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [IsCyclic G] (hG : IsPGroup p G) {K : Type u_4} [Group K] [MulDistribMulAction K G] (hGK : (Nat.card G).Coprime (Nat.card K)) : (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g

If a cyclic p-group G acts on a group K of coprime order, then the map K × G → G defined by (k, g) ↦ k • g * g⁻¹ is either trivial or surjective.

theorem IsPGroup.commutator_eq_bot_or_commutator_eq_self {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {P K : Subgroup G} [IsCyclic ↥P] (hP : IsPGroup p ↥P) (hKP : K ≤ P.normalizer) (hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)) : ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P

If a cyclic p-subgroup P acts by conjugation on a subgroup K of coprime order, then either ⁅K, P⁆ = ⊥ or ⁅K, P⁆ = P.

theorem Sylow.commutator_eq_bot_or_commutator_eq_self {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] [(↑P).Normal] {K : Subgroup G} (h : K.IsComplement' ↑P) : ⁅K, ↑P⁆ = ⊥ ∨ ⁅K, ↑P⁆ = ↑P

If a normal cyclic Sylow p-subgroup P has a complement K, then either ⁅K, P⁆ = ⊥ or ⁅K, P⁆ = P.

theorem Sylow.le_center_or_le_commutator {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] [(↑P).Normal] : ↑P ≤ Subgroup.center G ∨ ↑P ≤ commutator G

A normal cyclic Sylow subgroup is either central or contained in the commutator subgroup.

theorem Sylow.normalizer_le_centralizer_or_le_commutator {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] : (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

A cyclic Sylow subgroup is either central in its normalizer or contained in the commutator subgroup.

theorem Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] : ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

If G has a cyclic Sylow p-subgroup, then the cardinality and index of the commutator subgroup of G cannot both be divisible by p.

theorem IsZGroup.coprime_commutator_index (G : Type u_1) [Group G] [Finite G] [IsZGroup G] : (Nat.card ↥(commutator G)).Coprime (commutator G).index

If G is a finite Z-group, then commutator G is a Hall subgroup of G.

theorem 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.