feat(group_theory/finiteness): Add variants of rank_closure_le_card (…

…#16364)

This PR adds some more API lemmas for `group.rank`.

`rank_congr` is useful since `rw h` and `simp only [h]` have run into trouble.

src/group_theory/finiteness.lean

@@ -9,6 +9,7 @@ import data.finset
 import group_theory.quotient_group
 import group_theory.submonoid.operations
 import group_theory.subgroup.basic
+import set_theory.cardinal.finite
 
 /-!
 # Finitely generated monoids and groups
@@ -161,6 +162,20 @@ lemma submonoid.powers_fg (r : M) : (submonoid.powers r).fg :=
 instance monoid.powers_fg (r : M) : monoid.fg (submonoid.powers r) :=
 (monoid.fg_iff_submonoid_fg _).mpr (submonoid.powers_fg r)
 
+@[to_additive] instance monoid.closure_finset_fg (s : finset M) :
+  monoid.fg (submonoid.closure (s : set M)) :=
+begin
+  refine ⟨⟨s.preimage coe (subtype.coe_injective.inj_on _), _⟩⟩,
+  rw [finset.coe_preimage, submonoid.closure_closure_coe_preimage],
+end
+
+@[to_additive] instance monoid.closure_finite_fg (s : set M) [finite s] :
+  monoid.fg (submonoid.closure s) :=
+begin
+  haveI := fintype.of_finite s,
+  exact s.coe_to_finset ▸ monoid.closure_finset_fg s.to_finset,
+end
+
 /-! ### Groups and subgroups -/
 
 variables {G H : Type*} [group G] [add_group H]
@@ -278,6 +293,20 @@ group.fg_iff_monoid.fg.mpr $ @monoid.fg_of_surjective G _ G' _ (group.fg_iff_mon
 instance group.fg_range {G' : Type*} [group G'] [group.fg G] (f : G →* G') : group.fg f.range :=
 group.fg_of_surjective f.range_restrict_surjective
 
+@[to_additive] instance group.closure_finset_fg (s : finset G) :
+  group.fg (subgroup.closure (s : set G)) :=
+begin
+  refine ⟨⟨s.preimage coe (subtype.coe_injective.inj_on _), _⟩⟩,
+  rw [finset.coe_preimage, ←subgroup.coe_subtype, subgroup.closure_preimage_eq_top],
+end
+
+@[to_additive] instance group.closure_finite_fg (s : set G) [finite s] :
+  group.fg (subgroup.closure s) :=
+begin
+  haveI := fintype.of_finite s,
+  exact s.coe_to_finset ▸ group.closure_finset_fg s.to_finset,
+end
+
 variables (G)
 
 /-- The minimum number of generators of a group. -/
@@ -317,6 +346,36 @@ le_antisymm (group.rank_le_of_surjective f.symm f.symm.surjective)
 
 end group
 
+namespace subgroup
+
+@[to_additive] lemma rank_congr {H K : subgroup G} [group.fg H] [group.fg K] (h : H = K) :
+  group.rank H = group.rank K :=
+by unfreezingI { subst h }
+
+@[to_additive] lemma rank_closure_finset_le_card (s : finset G) :
+  group.rank (closure (s : set G)) ≤ s.card :=
+begin
+  classical,
+  let t : finset (closure (s : set G)) := s.preimage coe (subtype.coe_injective.inj_on _),
+  have ht : closure (t : set (closure (s : set G))) = ⊤,
+  { rw finset.coe_preimage,
+    exact closure_preimage_eq_top s },
+  apply (group.rank_le (closure (s : set G)) ht).trans,
+  rw [←finset.card_image_of_inj_on, finset.image_preimage],
+  { apply finset.card_filter_le },
+  { apply subtype.coe_injective.inj_on },
+end
+
+@[to_additive] lemma rank_closure_finite_le_nat_card (s : set G) [finite s] :
+  group.rank (closure s) ≤ nat.card s :=
+begin
+  haveI := fintype.of_finite s,
+  rw [nat.card_eq_fintype_card, ←s.to_finset_card, ←rank_congr (congr_arg _ s.coe_to_finset)],
+  exact rank_closure_finset_le_card s.to_finset,
+end
+
+end subgroup
+
 section quotient_group
 
 @[to_additive]

src/group_theory/subgroup/basic.lean

@@ -2387,6 +2387,16 @@ begin
   rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf,
 end
 
+@[to_additive] lemma closure_preimage_eq_top (s : set G) :
+  closure ((closure s).subtype ⁻¹' s) = ⊤ :=
+begin
+  apply map_injective (show function.injective (closure s).subtype, from subtype.coe_injective),
+  rwa [monoid_hom.map_closure, ←monoid_hom.range_eq_map, subtype_range,
+    set.image_preimage_eq_of_subset],
+  rw [coe_subtype, subtype.range_coe_subtype],
+  exact subset_closure,
+end
+
 @[to_additive] lemma comap_sup_eq_of_le_range
   {H K : subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
   comap f H ⊔ comap f K = comap f (H ⊔ K) :=