From 1b771af7cb2cac078411bfc8b32422d5aa5ddaeb Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Mon, 2 Aug 2021 08:51:21 +0000 Subject: [PATCH] feat(group_theory/coset): card_dvd_of_injective (#8485) --- src/group_theory/coset.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean index 4d0c85fd7aee2..c9629e74782b1 100644 --- a/src/group_theory/coset.lean +++ b/src/group_theory/coset.lean @@ -362,6 +362,28 @@ lemma card_quotient_dvd_card [fintype α] (s : subgroup α) [decidable_pred (λ [fintype s] : fintype.card (quotient s) ∣ fintype.card α := by simp [card_eq_card_quotient_mul_card_subgroup s] +open fintype + +variables {H : Type*} [group H] + +lemma card_dvd_of_injective [fintype α] [fintype H] (f : α →* H) (hf : function.injective f) : + card α ∣ card H := +by classical; +calc card α = card (f.range : subgroup H) : card_congr (equiv.of_injective f hf) +...∣ card H : card_subgroup_dvd_card _ + +lemma card_dvd_of_le {H K : subgroup α} [fintype H] [fintype K] (hHK : H ≤ K) : card H ∣ card K := +card_dvd_of_injective (inclusion hHK) (inclusion_injective hHK) + +lemma card_comap_dvd_of_injective (K : subgroup H) [fintype K] + (f : α →* H) [fintype (K.comap f)] (hf : function.injective f) : + fintype.card (K.comap f) ∣ fintype.card K := +by haveI : fintype ((K.comap f).map f) := + fintype.of_equiv _ (equiv_map_of_injective _ _ hf).to_equiv; +calc fintype.card (K.comap f) = fintype.card ((K.comap f).map f) : + fintype.card_congr (equiv_map_of_injective _ _ hf).to_equiv +... ∣ fintype.card K : card_dvd_of_le (map_comap_le _ _) + end subgroup namespace quotient_group