From 18dc1a18613cf28876efdd115053587cb5328e5a Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 16 Sep 2021 05:50:06 +0000 Subject: [PATCH] feat(group_theory/p_group): p-groups are preserved by isomorphisms (#9203) Adds three lemmas about transporting `is_p_group` across injective, surjective, and bijective homomorphisms. Co-authored-by: tb65536 --- src/group_theory/p_group.lean | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/group_theory/p_group.lean b/src/group_theory/p_group.lean index c7d3942420325..03aaa2e1b2035 100644 --- a/src/group_theory/p_group.lean +++ b/src/group_theory/p_group.lean @@ -75,18 +75,29 @@ variables (hG : is_p_group p G) include hG +lemma of_injective {H : Type*} [group H] (ϕ : H →* G) (hϕ : function.injective ϕ) : + is_p_group p H := +begin + simp_rw [is_p_group, ←hϕ.eq_iff, ϕ.map_pow, ϕ.map_one], + exact λ h, hG (ϕ h), +end + lemma to_subgroup (H : subgroup G) : is_p_group p H := +hG.of_injective H.subtype subtype.coe_injective + +lemma of_surjective {H : Type*} [group H] (ϕ : G →* H) (hϕ : function.surjective ϕ) : + is_p_group p H := begin - simp_rw [is_p_group, subtype.ext_iff, subgroup.coe_pow], - exact λ h, hG h, + refine λ h, exists.elim (hϕ h) (λ g hg, exists_imp_exists (λ k hk, _) (hG g)), + rw [←hg, ←ϕ.map_pow, hk, ϕ.map_one], 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 +hG.of_surjective (quotient_group.mk' H) quotient.surjective_quotient_mk' + +lemma of_equiv {H : Type*} [group H] (ϕ : G ≃* H) : is_p_group p H := +hG.of_surjective ϕ.to_monoid_hom ϕ.surjective variables [hp : fact p.prime] @@ -107,7 +118,7 @@ lemma card_orbit (a : α) [fintype (orbit G a)] : ∃ n : ℕ, card (orbit G a) = p ^ n := begin let ϕ := orbit_equiv_quotient_stabilizer G a, - haveI := of_equiv (orbit G a) ϕ, + haveI := fintype.of_equiv (orbit G a) ϕ, rw [card_congr ϕ, ←subgroup.index_eq_card], exact hG.index (stabilizer G a), end