refactor(group_theory/p_group): Move lemmas to is_p_group namespace (#…

…9188)

Moves `card_modeq_card_fixed_points`, `nonempty_fixed_point_of_prime_not_dvd_card`, and `exists_fixed_point_of_prime_dvd_card_of_fixed_point` to the `is_p_group` namespace. I think this simplifies things, since they already had explicit `hG : is_p_group G` hypotheses anyway.

src/group_theory/p_group.lean

@@ -18,6 +18,8 @@ It also contains proofs of some corollaries of this lemma about existence of fix
 
 open_locale big_operators
 
+open fintype mul_action
+
 variables (p : ℕ) (G : Type*) [group G]
 
 /-- A p-group is a group in which every element has prime power order -/
@@ -33,19 +35,19 @@ forall_congr (λ g, ⟨λ ⟨k, hk⟩, exists_imp_exists (by exact λ j, Exists.
   ((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 :=
+lemma of_card [fintype G] {n : ℕ} (hG : card G = p ^ n) : is_p_group p G :=
 λ g, ⟨n, by rw [←hG, pow_card_eq_one]⟩
 
 lemma of_bot : is_p_group p (⊥ : subgroup G) :=
 of_card (subgroup.card_bot.trans (pow_zero p).symm)
 
 lemma iff_card [fact p.prime] [fintype G] :
-  is_p_group p G ↔ ∃ n : ℕ, fintype.card G = p ^ n :=
+  is_p_group p G ↔ ∃ n : ℕ, card G = p ^ n :=
 begin
-  have hG : 0 < fintype.card G := fintype.card_pos_iff.mpr has_one.nonempty,
+  have hG : 0 < card G := 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,
+  suffices : ∀ q ∈ nat.factors (card G), q = p,
+  { use (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,
@@ -91,25 +93,18 @@ begin
   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 :=
+variables {α : Type*} [mul_action G α]
+
+lemma card_orbit (a : α) [fintype (orbit G a)] :
+  ∃ n : ℕ, card (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),
+  let ϕ := orbit_equiv_quotient_stabilizer G a,
+  haveI := of_equiv (orbit G a) ϕ,
+  rw [card_congr ϕ, ←subgroup.index_eq_card],
+  exact hG.index (stabilizer G a),
 end
 
-end is_p_group
-
-namespace mul_action
-
-open fintype
-
-variables (α : Type*) [mul_action G α] [fintype α] [fintype (fixed_points G α)]
-  (hG : is_p_group p G) [fact p.prime]
-
-include hG
+variables (α) [fintype α] [fintype (fixed_points G α)]
 
 /-- 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 `α` -/
@@ -137,13 +132,13 @@ end
 
 /-- 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 ∣ card α) :
+lemma nonempty_fixed_point_of_prime_not_dvd_card (hpα : ¬ p ∣ card α) :
   (fixed_points G α).nonempty :=
 @set.nonempty_of_nonempty_subtype _ _ begin
 rw [←card_pos_iff, pos_iff_ne_zero],
-  contrapose! hp,
-  rw [←nat.modeq_zero_iff_dvd, ←hp],
-  exact card_modeq_card_fixed_points α hG,
+  contrapose! hpα,
+  rw [←nat.modeq_zero_iff_dvd, ←hpα],
+  exact hG.card_modeq_card_fixed_points α,
 end
 
 /-- If a p-group acts on `α` and the cardinality of `α` is a multiple
@@ -152,10 +147,10 @@ lemma exists_fixed_point_of_prime_dvd_card_of_fixed_point
   (hpα : p ∣ card α) {a : α} (ha : a ∈ fixed_points G α) :
   ∃ b, b ∈ fixed_points G α ∧ a ≠ b :=
 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),
+  nat.modeq_zero_iff_dvd.mp ((hG.card_modeq_card_fixed_points α).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
+end is_p_group

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 _ (is_p_group.of_card hH)).symm
+  exact ((is_p_group.of_card hH).card_modeq_card_fixed_points _).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 _ _ _ _ _ _ (is_p_group.of_card hH) hp,
+    (is_p_group.of_card hH).card_modeq_card_fixed_points _,
 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),