English
An extension of coprime Z-groups is a Z-group: if G, G'', and the connecting maps satisfy finiteness, Z-group structure, and coprimality, then G' is a Z-group.
Русский
Расширение Z-групп сохраняет Z-группу: если G и G'' являются Z-группами и выполняются условия сопоставления (порядки/coprirtness), то G' тоже Z-группа.
LaTeX
$$$IsZGroup(G')$$$
Lean4
/-- An extension of coprime Z-groups is a Z-group. -/
theorem isZGroup_of_coprime [Finite G] [IsZGroup G] [IsZGroup G''] (h_le : f'.ker ≤ f.range)
(h_cop : (Nat.card G).Coprime (Nat.card G'')) : IsZGroup G' :=
by
refine ⟨fun p hp P ↦ ?_⟩
have := Fact.mk hp
replace h_cop :=
(h_cop.of_dvd ((Subgroup.card_dvd_of_le h_le).trans (Subgroup.card_range_dvd f))
(Subgroup.index_ker f' ▸ f'.range.card_subgroup_dvd_card))
rcases P.2.le_or_disjoint_of_coprime h_cop with h | h
· replace h_le : P ≤ f.range := h.trans h_le
suffices IsCyclic (P.subgroupOf f.range)
by
have key := Subgroup.subgroupOfEquivOfLe h_le
exact isCyclic_of_surjective key key.surjective
obtain ⟨Q, hQ⟩ := Sylow.mapSurjective_surjective f.rangeRestrict_surjective p (P.subtype h_le)
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ
exact hQ ▸ isCyclic_of_surjective _ (f.rangeRestrict.subgroupMap_surjective Q)
· have := (P.2.map f').isCyclic_of_isZGroup
apply isCyclic_of_injective (f'.subgroupMap P)
rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]
