English
A finite group G is a Z-group iff it is isomorphic to a semidirect product of two cyclic subgroups of coprime order.
Русский
Конечная группа G является Z-группой тогда и только тогда, когда она изоморфна полуручным полупродуктам двух циклических подгрупп взаимно простого порядка.
LaTeX
$$$IsZGroup(G) \\iff \\exists N,H,\\phi, e:\\ G \\cong N \\rtimes_{\\phi} H \\land IsCyclic(H) \\land IsCyclic(N) \\land (|N|,|H|)=1$$$
Lean4
/-- A finite group `G` is a Z-group if and only if `G` is isomorphic to a semidirect product of two
cyclic subgroups of coprime order. -/
theorem isZGroup_iff_exists_mulEquiv [Finite G] :
IsZGroup G ↔
∃ (N H : Subgroup G) (φ : H →* MulAut N) (_ : G ≃* N ⋊[φ] H),
IsCyclic H ∧ IsCyclic N ∧ (Nat.card N).Coprime (Nat.card H) :=
by
refine ⟨fun hG ↦ ?_, ?_⟩
· obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index
have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv
refine
⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm, isCyclic_of_surjective _ h1.surjective,
hG.isCyclic_commutator, ?_⟩
exact Nat.card_congr h1.toEquiv ▸ hG.coprime_commutator_index
· rintro ⟨N, H, φ, e, hH, hN, hHN⟩
have : IsZGroup (N ⋊[φ] H) := isZGroup_of_coprime SemidirectProduct.range_inl_eq_ker_rightHom.ge hHN
exact IsZGroup.of_injective (f := e.toMonoidHom) e.injective
