feat(group_theory/p_group): Generalize to infinite p-groups (#9082)

Defines p-groups, and generalizes the results of `p_group.lean` to infinite p-groups. The eventual goal is to generalize Sylow's theorems to infinite groups.

src/group_theory/p_group.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2018 . All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Thomas Browning
 -/
 
+import group_theory.index
 import group_theory.perm.cycle_type
+import group_theory.quotient_group
 
 /-!
 # p-groups
@@ -14,71 +16,143 @@ then the number of fixed points of the action is congruent mod `p` to the cardin
 It also contains proofs of some corollaries of this lemma about existence of fixed points.
 -/
 
+open_locale big_operators
+
+variables (p : ℕ) (G : Type*) [group G]
+
+/-- A p-group is a group in which every element has prime power order -/
+def is_p_group : Prop := ∀ g : G, ∃ k : ℕ, g ^ (p ^ k) = 1
+
+variables {p} {G}
+
+namespace is_p_group
+
+lemma iff_order_of [hp : fact p.prime] :
+  is_p_group p G ↔ ∀ g : G, ∃ k : ℕ, order_of g = p ^ k :=
+forall_congr (λ g, ⟨λ ⟨k, hk⟩, exists_imp_exists (by exact λ j, Exists.snd)
+  ((nat.dvd_prime_pow hp.out).mp (order_of_dvd_of_pow_eq_one hk)),
+  exists_imp_exists (λ k hk, by rw [←hk, pow_order_of_eq_one])⟩)
+
+lemma of_card [fintype G] {n : ℕ} (hG : fintype.card G = p ^ n) : is_p_group p G :=
+λ g, ⟨n, by rw [←hG, pow_card_eq_one]⟩
+
+lemma iff_card [fact p.prime] [fintype G] :
+  is_p_group p G ↔ ∃ n : ℕ, fintype.card G = p ^ n :=
+begin
+  have hG : 0 < fintype.card G := fintype.card_pos_iff.mpr has_one.nonempty,
+  refine ⟨λ h, _, λ ⟨n, hn⟩, of_card hn⟩,
+  suffices : ∀ q ∈ nat.factors (fintype.card G), q = p,
+  { use (fintype.card G).factors.length,
+    rw [←list.prod_repeat, ←list.eq_repeat_of_mem this, nat.prod_factors hG] },
+  intros q hq,
+  obtain ⟨hq1, hq2⟩ := (nat.mem_factors hG).mp hq,
+  haveI : fact q.prime := ⟨hq1⟩,
+  obtain ⟨g, hg⟩ := equiv.perm.exists_prime_order_of_dvd_card q hq2,
+  obtain ⟨k, hk⟩ := (iff_order_of.mp h) g,
+  exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm,
+end
+
+lemma to_le {H K : subgroup G} (hK : is_p_group p K) (hHK : H ≤ K) : is_p_group p H :=
+begin
+  simp_rw [is_p_group, subtype.ext_iff, subgroup.coe_pow] at hK ⊢,
+  exact λ h, hK ⟨h, hHK h.2⟩,
+end
+
+variables (hG : is_p_group p G)
+
+include hG
+
+lemma to_subgroup (H : subgroup G) : is_p_group p H :=
+begin
+  simp_rw [is_p_group, subtype.ext_iff, subgroup.coe_pow],
+  exact λ h, hG h,
+end
+
+lemma to_quotient (H : subgroup G) [H.normal] :
+  is_p_group p (quotient_group.quotient H) :=
+begin
+  refine quotient.ind' (forall_imp (λ g, _) hG),
+  exact exists_imp_exists (λ k h, (quotient_group.coe_pow H g _).symm.trans (congr_arg coe h)),
+end
+
+variables [hp : fact p.prime]
+
+include hp
+
+lemma index (H : subgroup G) [fintype (quotient_group.quotient H)] :
+  ∃ n : ℕ, H.index = p ^ n :=
+begin
+  obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normal_core),
+  obtain ⟨k, hk1, hk2⟩ := (nat.dvd_prime_pow hp.out).mp ((congr_arg _
+    (H.normal_core.index_eq_card.trans hn)).mp (subgroup.index_dvd_of_le H.normal_core_le)),
+  exact ⟨k, hk2⟩,
+end
+
+lemma card_orbit {α : Type*} [mul_action G α] (a : α) [fintype (mul_action.orbit G a)] :
+  ∃ n : ℕ, fintype.card (mul_action.orbit G a) = p ^ n :=
+begin
+  let ϕ := mul_action.orbit_equiv_quotient_stabilizer G a,
+  haveI := fintype.of_equiv (mul_action.orbit G a) ϕ,
+  rw [fintype.card_congr ϕ, ←subgroup.index_eq_card],
+  exact index hG (mul_action.stabilizer G a),
+end
+
+end is_p_group
+
 namespace mul_action
 
-open fintype equiv finset subgroup
-open_locale big_operators classical
+open fintype
 
-variables {G : Type*} (α : Type*) [group G] [mul_action G α] [fintype G] [fintype α]
-  [fintype (fixed_points G α)] {p n : ℕ} [fact p.prime] (hG : card G = p ^ n)
+variables (α : Type*) [mul_action G α] [fintype α] [fintype (fixed_points G α)]
+  (hG : is_p_group p G) [fact p.prime]
 
 include hG
 
 /-- If `G` is a `p`-group acting on a finite set `α`, then the number of fixed points
   of the action is congruent mod `p` to the cardinality of `α` -/
 lemma card_modeq_card_fixed_points : card α ≡ card (fixed_points G α) [MOD p] :=
-calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
-  card_congr (sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
-... = ∑ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a} : card_sigma _
-... ≡ ∑ a : fixed_points G α, 1 [MOD p] :
 begin
+  classical,
+  calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
+    card_congr (equiv.sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
+  ... = ∑ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a} : card_sigma _
+  ... ≡ ∑ a : fixed_points G α, 1 [MOD p] : _
+  ... = _ : by simp; refl,
   rw [←zmod.eq_iff_modeq_nat p, nat.cast_sum, nat.cast_sum],
-  refine eq.symm (sum_bij_ne_zero (λ a _ _, quotient.mk' a.1)
-    (λ _ _ _, mem_univ _)
-    (λ a₁ a₂ _ _ _ _ h,
-      subtype.eq ((mem_fixed_points' α).1 a₂.2 a₁.1 (quotient.exact' h)))
-      (λ b, _)
-      (λ a ha _, by rw [← mem_fixed_points_iff_card_orbit_eq_one.1 a.2];
-        simp only [quotient.eq']; congr)),
-  { refine quotient.induction_on' b (λ b _ hb, _),
-    have : card (orbit G b) ∣ p ^ n,
-    { rw [← hG, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)],
-      exact card_quotient_dvd_card _ },
-    rcases (nat.dvd_prime_pow (fact.out p.prime)).1 this with ⟨k, _, hk⟩,
-    have hb' :¬ p ^ 1 ∣ p ^ k,
-    { rw [pow_one, ← hk, ← nat.modeq_zero_iff_dvd, ← zmod.eq_iff_modeq_nat,
-        nat.cast_zero, ← ne.def],
-      exact eq.mpr (by simp only [quotient.eq']; congr) hb },
-    have : k = 0 := nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge (mt (pow_dvd_pow p) hb'))),
-    refine ⟨⟨b, mem_fixed_points_iff_card_orbit_eq_one.2 $ by rw [hk, this, pow_zero]⟩,
-      mem_univ _, _, rfl⟩,
-    rw [nat.cast_one], exact one_ne_zero }
+  have key : ∀ x, card {y // (quotient.mk' y : quotient (orbit_rel G α)) = quotient.mk' x} =
+    card (orbit G x) := λ x, by simp only [quotient.eq']; congr,
+  refine eq.symm (finset.sum_bij_ne_zero (λ a _ _, quotient.mk' a.1) (λ _ _ _, finset.mem_univ _)
+    (λ a₁ a₂ _ _ _ _ h, subtype.eq ((mem_fixed_points' α).mp a₂.2 a₁.1 (quotient.exact' h)))
+      (λ b, quotient.induction_on' b (λ b _ hb, _)) (λ a ha _, by
+      { rw [key, mem_fixed_points_iff_card_orbit_eq_one.mp a.2] })),
+  obtain ⟨k, hk⟩ := hG.card_orbit b,
+  have : k = 0 := nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge (mt (pow_dvd_pow p)
+    (by rwa [pow_one, ←hk, ←nat.modeq_zero_iff_dvd, ←zmod.eq_iff_modeq_nat, ←key])))),
+  exact ⟨⟨b, mem_fixed_points_iff_card_orbit_eq_one.2 $ by rw [hk, this, pow_zero]⟩,
+    finset.mem_univ _, (ne_of_eq_of_ne nat.cast_one one_ne_zero), rfl⟩,
 end
-... = _ : by simp; refl
 
 /-- If a p-group acts on `α` and the cardinality of `α` is not a multiple
   of `p` then the action has a fixed point. -/
-lemma nonempty_fixed_point_of_prime_not_dvd_card
-  (hp : ¬ p ∣ fintype.card α) :
+lemma nonempty_fixed_point_of_prime_not_dvd_card (hp : ¬ p ∣ card α) :
   (fixed_points G α).nonempty :=
 @set.nonempty_of_nonempty_subtype _ _ begin
-  rw [← fintype.card_pos_iff, pos_iff_ne_zero],
-  assume h,
-  have := card_modeq_card_fixed_points α hG,
-  rw [h, nat.modeq_zero_iff_dvd] at this,
-  contradiction
+rw [←card_pos_iff, pos_iff_ne_zero],
+  contrapose! hp,
+  rw [←nat.modeq_zero_iff_dvd, ←hp],
+  exact card_modeq_card_fixed_points α hG,
 end
 
 /-- If a p-group acts on `α` and the cardinality of `α` is a multiple
   of `p`, and the action has one fixed point, then it has another fixed point. -/
 lemma exists_fixed_point_of_prime_dvd_card_of_fixed_point
-  (hpα : p ∣ fintype.card α) {a : α} (ha : a ∈ fixed_points G α) :
+  (hpα : p ∣ card α) {a : α} (ha : a ∈ fixed_points G α) :
   ∃ b, b ∈ fixed_points G α ∧ a ≠ b :=
-have hpf : p ∣ fintype.card (fixed_points G α),
-  from nat.modeq_zero_iff_dvd.1 ((card_modeq_card_fixed_points α hG).symm.trans hpα.modeq_zero_nat),
-have hα : 1 < fintype.card (fixed_points G α),
-  from (fact.out p.prime).one_lt.trans_le (nat.le_of_dvd (fintype.card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf),
-let ⟨⟨b, hb⟩, hba⟩ := fintype.exists_ne_of_one_lt_card hα ⟨a, ha⟩ in
-⟨b, hb, λ hab, hba $ by simp [hab]⟩
+have hpf : p ∣ card (fixed_points G α) :=
+  nat.modeq_zero_iff_dvd.mp ((card_modeq_card_fixed_points α hG).symm.trans hpα.modeq_zero_nat),
+have hα : 1 < card (fixed_points G α) :=
+  (fact.out p.prime).one_lt.trans_le (nat.le_of_dvd (card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf),
+let ⟨⟨b, hb⟩, hba⟩ := exists_ne_of_one_lt_card hα ⟨a, ha⟩ in
+⟨b, hb, λ hab, hba (by simp_rw [hab])⟩
 
 end mul_action

src/group_theory/sylow.lean

@@ -80,7 +80,7 @@ lemma card_quotient_normalizer_modeq_card_quotient [fintype G] {p : ℕ} {n : 
   ≡ card (quotient H) [MOD p] :=
 begin
   rw [← fintype.card_congr (fixed_points_mul_left_cosets_equiv_quotient H)],
-  exact (card_modeq_card_fixed_points _ hH).symm
+  exact (card_modeq_card_fixed_points _ (is_p_group.of_card hH)).symm
 end
 
 /-- If `H` is a subgroup of `G` of cardinality `p ^ n`, then the cardinality of the
@@ -140,7 +140,7 @@ have hcard : card (quotient H) = s * p :=
 have hm : s * p % p =
   card (quotient (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H)) % p :=
   card_congr (fixed_points_mul_left_cosets_equiv_quotient H) ▸ hcard ▸
-    @card_modeq_card_fixed_points _ _ _ _ _ _ _ p _ hp hH,
+    @card_modeq_card_fixed_points p _ _ _ _ _ _ (is_p_group.of_card hH) hp,
 have hm' : p ∣ card (quotient (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H)) :=
   nat.dvd_of_mod_eq_zero
     (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),