English
If p^n divides |G|, there exists a subgroup of G of order p^n.
Русский
Если p^n делит порядок G, существует подгруппа G порядка p^n.
LaTeX
$$∃ K: Subgroup G, card K = p^n$$
Lean4
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
then `H` is contained in a subgroup of cardinality `p ^ (n + 1)`
if `p ^ (n + 1)` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_succ [Finite G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime] (hdvd : p ^ (n + 1) ∣ Nat.card G)
{H : Subgroup G} (hH : Nat.card H = p ^ n) : ∃ K : Subgroup G, Nat.card K = p ^ (n + 1) ∧ H ≤ K :=
let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
have hcard : Nat.card (G ⧸ H) = s * p :=
(mul_left_inj' (show Nat.card H ≠ 0 from Nat.card_pos.ne')).1
(by rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
have hm : s * p % p = Nat.card (normalizer H ⧸ H.subgroupOf H.normalizer) % p :=
Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H) ▸
hcard ▸ (IsPGroup.of_card hH).card_modEq_card_fixedPoints _
have hm' : p ∣ Nat.card (normalizer H ⧸ H.subgroupOf H.normalizer) :=
Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)
let ⟨x, hx⟩ := @exists_prime_orderOf_dvd_card' _ (QuotientGroup.Quotient.group _) _ _ hp hm'
have hequiv : H ≃ H.subgroupOf H.normalizer := (subgroupOfEquivOfLe le_normalizer).symm.toEquiv
⟨Subgroup.map (normalizer H).subtype (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)),
by
show
Nat.card (Subgroup.map H.normalizer.subtype (comap (mk' (H.subgroupOf H.normalizer)) (Subgroup.zpowers x))) =
p ^ (n + 1)
suffices
Nat.card (Subtype.val '' (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)) =
p ^ (n + 1)
by convert this using 2
rw [Nat.card_image_of_injective Subtype.val_injective
(Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer),
pow_succ, ← hH, Nat.card_congr hequiv, ← hx, ← Nat.card_zpowers, ← Nat.card_prod]
exact Nat.card_congr (preimageMkEquivSubgroupProdSet (H.subgroupOf H.normalizer) (zpowers x)),
by
intro y hy
simp only [Subgroup.coe_subtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩
dsimp only
rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
simpa using hy⟩
