feat: Relative Sylow's first theorems (#8944)

Prove variants of Sylow' first theorem relative to a subgroup. From PFR Co-authored-by: Sébastien Gouëzel <[email protected]>
leanprover-community · Dec 19, 2023 · 363e9f6 · 363e9f6
1 parent e851153
commit 363e9f6
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 0 deletions.
diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean
@@ -67,6 +67,8 @@ theorem iff_card [Fact p.Prime] [Fintype G] : IsPGroup p G ↔ ∃ n : ℕ, card
   exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm
 #align is_p_group.iff_card IsPGroup.iff_card
 
+alias ⟨exists_card_eq, _⟩ := iff_card
+
 section GIsPGroup
 
 variable (hG : IsPGroup p G)

diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
@@ -653,6 +653,33 @@ theorem exists_subgroup_card_pow_prime [Fintype G] (p : ℕ) {n : ℕ} [Fact p.P
   ⟨K, hK.1⟩
 #align sylow.exists_subgroup_card_pow_prime Sylow.exists_subgroup_card_pow_prime
 
+lemma exists_subgroup_card_pow_prime_of_le_card {m p : ℕ} (hp : p.Prime) (h : IsPGroup p G)
+    (hm : p ^ m ≤ Nat.card G) : ∃ H : Subgroup G, Nat.card H = p ^ m := by
+  have : Fact p.Prime := ⟨hp⟩
+  have : Finite G := Nat.finite_of_card_ne_zero $ by linarith [Nat.one_le_pow m p hp.pos]
+  cases nonempty_fintype G
+  obtain ⟨n, hn⟩ := h.exists_card_eq
+  simp_rw [Nat.card_eq_fintype_card] at hn hm ⊢
+  refine exists_subgroup_card_pow_prime _ ?_
+  rw [hn] at hm ⊢
+  exact pow_dvd_pow _ $ (pow_le_pow_iff_right hp.one_lt).1 hm
+
+lemma exists_subgroup_le_card_pow_prime_of_le_card {m p : ℕ} (hp : p.Prime) (h : IsPGroup p G)
+    {H : Subgroup G} (hm : p ^ m ≤ Nat.card H) : ∃ H' ≤ H, Nat.card H' = p ^ m := by
+  obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hm
+  refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩
+  rw [← H'card]
+  let e : H' ≃* H'.map H.subtype := H'.equivMapOfInjective (Subgroup.subtype H) H.subtype_injective
+  exact Nat.card_congr e.symm.toEquiv
+
+lemma exists_subgroup_le_card_le {k p : ℕ} (hp : p.Prime) (h : IsPGroup p G) {H : Subgroup G}
+    (hk : k ≤ Nat.card H) (hk₀ : k ≠ 0) : ∃ H' ≤ H, Nat.card H' ≤ k ∧ k < p * Nat.card H' := by
+  obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
+    exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt
+  obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)
+  refine ⟨H', H'H, ?_⟩
+  simpa only [pow_succ, H'card] using And.intro hmk hkm
+
 theorem pow_dvd_card_of_pow_dvd_card [Fintype G] {p n : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
     (hdvd : p ^ n ∣ card G) : p ^ n ∣ card P :=
   (hp.1.coprime_pow_of_not_dvd