feat(group_theory/finiteness): add group.fg (#7338)

Basic facts about finitely generated groups.

- [x] depends on: #7279

src/algebra/module/submodule.lean

@@ -204,6 +204,9 @@ include module_M
 theorem to_add_subgroup_injective : injective (to_add_subgroup : submodule R M → add_subgroup M)
 | p q h := set_like.ext (set_like.ext_iff.1 h : _)
 
+@[simp] theorem to_add_subgroup_eq : p.to_add_subgroup = p'.to_add_subgroup ↔ p = p' :=
+to_add_subgroup_injective.eq_iff
+
 @[mono] lemma to_add_subgroup_strict_mono :
   strict_mono (to_add_subgroup : submodule R M → add_subgroup M) := λ _ _, id
 

src/algebra/pointwise.lean

@@ -254,6 +254,9 @@ lemma inv_subset_inv [group α] {s t : set α} : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :
 @[to_additive] lemma inv_subset [group α] {s t : set α} : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹ :=
 by { rw [← inv_subset_inv, set.inv_inv] }
 
+@[to_additive] lemma finite.inv [group α] {s : set α} (hs : finite s) : finite s⁻¹ :=
+hs.preimage $ inv_injective.inj_on _
+
 /-! ### Properties about scalar multiplication -/
 
 /-- Scaling a set: multiplying every element by a scalar. -/

src/group_theory/finiteness.lean

@@ -6,21 +6,27 @@ Authors: Riccardo Brasca
 
 import data.set.finite
 import group_theory.submonoid.operations
+import group_theory.subgroup
 
 /-!
-# Finitely generated monoid.
+# Finitely generated monoids and groups
 
-We define finitely generated monoids. See also `submodule.fg` and `module.finite` for
+We define finitely generated monoids and groups. See also `submodule.fg` and `module.finite` for
 finitely-generated modules.
 
 ## Main definition
 
 * `submonoid.fg S`, `add_submonoid.fg S` : A submonoid `S` is finitely generated.
-* `monoid.fg M`, `add_submonoid.fg M` : A typeclass indicating a type `M` is finitely generated as
-a monoid.
+* `monoid.fg M`, `add_monoid.fg M` : A typeclass indicating a type `M` is finitely generated as a
+monoid.
+* `subgroup.fg S`, `add_subgroup.fg S` : A subgroup `S` is finitely generated.
+* `group.fg M`, `add_group.fg M` : A typeclass indicating a type `M` is finitely generated as a
+group.
 
 -/
 
+/-! ### Monoids and submonoids -/
+
 variables {M N : Type*} [monoid M] [add_monoid N]
 
 section submonoid
@@ -93,3 +99,104 @@ instance monoid.fg_of_add_monoid_fg [add_monoid.fg N] : monoid.fg (multiplicativ
 add_monoid.fg_iff_mul_fg.1 ‹_›
 
 end monoid
+
+/-! ### Groups and subgroups -/
+
+variables {G H : Type*} [group G] [add_group H]
+
+section subgroup
+
+/-- A subgroup of `G` is finitely generated if it is the closure of a finite subset of `G`. -/
+@[to_additive]
+def subgroup.fg (P : subgroup G) : Prop := ∃ S : finset G, subgroup.closure ↑S = P
+
+/-- An additive subgroup of `H` is finitely generated if it is the closure of a finite subset of
+`H`. -/
+add_decl_doc add_subgroup.fg
+
+/-- An equivalent expression of `subgroup.fg` in terms of `set.finite` instead of `finset`. -/
+@[to_additive "An equivalent expression of `add_subgroup.fg` in terms of `set.finite` instead of
+`finset`."]
+lemma subgroup.fg_iff (P : subgroup G) : subgroup.fg P ↔
+  ∃ S : set G, subgroup.closure S = P ∧ S.finite :=
+⟨λ⟨S, hS⟩, ⟨S, hS, finset.finite_to_set S⟩, λ⟨S, hS, hf⟩, ⟨set.finite.to_finset hf, by simp [hS]⟩⟩
+
+/-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid. -/
+@[to_additive add_subgroup.fg_iff_add_submonoid.fg "An additive subgroup is finitely generated if
+and only if it is finitely generated as an additive submonoid."]
+lemma subgroup.fg_iff_submonoid_fg (P : subgroup G) : P.fg ↔ P.to_submonoid.fg :=
+begin
+  split,
+  { rintro ⟨S, rfl⟩,
+    rw submonoid.fg_iff,
+    refine ⟨S ∪ S⁻¹, _, S.finite_to_set.union S.finite_to_set.inv⟩,
+    exact (subgroup.closure_to_submonoid _).symm },
+  { rintro ⟨S, hS⟩,
+    refine ⟨S, le_antisymm _ _⟩,
+    { rw [subgroup.closure_le, ←subgroup.coe_to_submonoid, ←hS],
+      exact submonoid.subset_closure },
+    { rw [← subgroup.to_submonoid_le, ← hS, submonoid.closure_le],
+      exact subgroup.subset_closure } }
+end
+
+lemma subgroup.fg_iff_add_fg (P : subgroup G) : P.fg ↔ P.to_add_subgroup.fg :=
+begin
+  rw [subgroup.fg_iff_submonoid_fg, add_subgroup.fg_iff_add_submonoid.fg],
+  exact (subgroup.to_submonoid P).fg_iff_add_fg
+end
+
+lemma add_subgroup.fg_iff_mul_fg (P : add_subgroup H) :
+  P.fg ↔ P.to_subgroup.fg :=
+begin
+  rw [add_subgroup.fg_iff_add_submonoid.fg, subgroup.fg_iff_submonoid_fg],
+  exact add_submonoid.fg_iff_mul_fg (add_subgroup.to_add_submonoid P)
+end
+
+end subgroup
+
+section group
+
+variables (G H)
+
+/-- A group is finitely generated if it is finitely generated as a submonoid of itself. -/
+class group.fg : Prop := (out : (⊤ : subgroup G).fg)
+
+/-- An additive group is finitely generated if it is finitely generated as an additive submonoid of
+itself. -/
+class add_group.fg : Prop := (out : (⊤ : add_subgroup H).fg)
+
+attribute [to_additive] group.fg
+
+variables {G H}
+
+lemma group.fg_def : group.fg G ↔ (⊤ : subgroup G).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩
+
+lemma add_group.fg_def : add_group.fg H ↔ (⊤ : add_subgroup H).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩
+
+/-- An equivalent expression of `group.fg` in terms of `set.finite` instead of `finset`. -/
+@[to_additive "An equivalent expression of `add_group.fg` in terms of `set.finite` instead of
+`finset`."]
+lemma group.fg_iff : group.fg G ↔
+  ∃ S : set G, subgroup.closure S = (⊤ : subgroup G) ∧ S.finite :=
+⟨λ h, (subgroup.fg_iff ⊤).1 h.out, λ h, ⟨(subgroup.fg_iff ⊤).2 h⟩⟩
+
+/-- A group is finitely generated if and only if it is finitely generated as a monoid. -/
+@[to_additive add_group.fg_iff_add_monoid.fg "An additive group is finitely generated if and only
+if it is finitely generated as an additive monoid."]
+lemma group.fg_iff_monoid.fg : group.fg G ↔ monoid.fg G :=
+⟨λ h, monoid.fg_def.2 $ (subgroup.fg_iff_submonoid_fg ⊤).1 (group.fg_def.1 h),
+    λ h, group.fg_def.2 $ (subgroup.fg_iff_submonoid_fg ⊤).2 (monoid.fg_def.1 h)⟩
+
+lemma group_fg.iff_add_fg : group.fg G ↔ add_group.fg (additive G) :=
+⟨λ h, ⟨(subgroup.fg_iff_add_fg ⊤).1 h.out⟩, λ h, ⟨(subgroup.fg_iff_add_fg ⊤).2 h.out⟩⟩
+
+lemma add_group.fg_iff_mul_fg : add_group.fg H ↔ group.fg (multiplicative H) :=
+⟨λ h, ⟨(add_subgroup.fg_iff_mul_fg ⊤).1 h.out⟩, λ h, ⟨(add_subgroup.fg_iff_mul_fg ⊤).2 h.out⟩⟩
+
+instance add_group.fg_of_group_fg [group.fg G] : add_group.fg (additive G) :=
+group_fg.iff_add_fg.1 ‹_›
+
+instance group.fg_of_mul_group_fg [add_group.fg H] : group.fg (multiplicative H) :=
+add_group.fg_iff_mul_fg.1 ‹_›
+
+end group

src/group_theory/subgroup.lean

@@ -133,6 +133,26 @@ lemma mem_to_submonoid (K : subgroup G) (x : G) : x ∈ K.to_submonoid ↔ x ∈
 instance (K : subgroup G) [d : decidable_pred (∈ K)] [fintype G] : fintype K :=
 show fintype {g : G // g ∈ K}, from infer_instance
 
+@[to_additive]
+theorem to_submonoid_injective :
+  function.injective (to_submonoid : subgroup G → submonoid G) :=
+λ p q h, set_like.ext'_iff.2 (show _, from set_like.ext'_iff.1 h)
+
+@[simp, to_additive]
+theorem to_submonoid_eq {p q : subgroup G} : p.to_submonoid = q.to_submonoid ↔ p = q :=
+to_submonoid_injective.eq_iff
+
+@[mono, to_additive] lemma to_submonoid_strict_mono :
+  strict_mono (to_submonoid : subgroup G → submonoid G) := λ _ _, id
+
+@[mono, to_additive]
+lemma to_submonoid_mono : monotone (to_submonoid : subgroup G → submonoid G) :=
+to_submonoid_strict_mono.monotone
+
+@[simp, to_additive]
+lemma to_submonoid_le {p q : subgroup G} : p.to_submonoid ≤ q.to_submonoid ↔ p ≤ q :=
+iff.rfl
+
 end subgroup
 
 /-!

src/ring_theory/finiteness.lean

@@ -35,7 +35,8 @@ variables [add_comm_group M] [module R M]
 variables [add_comm_group N] [module R N]
 
 /-- A module over a commutative ring is `finite` if it is finitely generated as a module. -/
-class module.finite : Prop := (out : (⊤ : submodule R M).fg)
+class module.finite (R : Type*) (M : Type*) [comm_semiring R] [add_comm_monoid M] [module R M] :
+  Prop := (out : (⊤ : submodule R M).fg)
 
 /-- An algebra over a commutative ring is of `finite_type` if it is finitely generated
 over the base ring as algebra. -/
@@ -49,9 +50,8 @@ def algebra.finite_presentation : Prop :=
 
 namespace module
 
-variables {R M N}
-lemma finite_def : finite R M ↔ (⊤ : submodule R M).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩
-variables (R M N)
+lemma finite_def {R : Type*} {M : Type*} [comm_semiring R] [add_comm_monoid M] [module R M] :
+  finite R M ↔ (⊤ : submodule R M).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩
 
 @[priority 100] -- see Note [lower instance priority]
 instance is_noetherian.finite [is_noetherian R M] : finite R M :=
@@ -60,6 +60,14 @@ instance is_noetherian.finite [is_noetherian R M] : finite R M :=
 namespace finite
 open submodule set
 
+lemma iff_add_monoid_fg {M : Type*} [add_comm_monoid M] : module.finite ℕ M ↔ add_monoid.fg M :=
+⟨λ h, add_monoid.fg_def.2 $ (fg_iff_add_submonoid_fg ⊤).1 (finite_def.1 h),
+  λ h, finite_def.2 $ (fg_iff_add_submonoid_fg ⊤).2 (add_monoid.fg_def.1 h)⟩
+
+lemma iff_add_group_fg {G : Type*} [add_comm_group G] : module.finite ℤ G ↔ add_group.fg G :=
+⟨λ h, add_group.fg_def.2 $ (fg_iff_add_subgroup_fg ⊤).1 (finite_def.1 h),
+  λ h, finite_def.2 $ (fg_iff_add_subgroup_fg ⊤).2 (add_group.fg_def.1 h)⟩
+
 variables {R M N}
 
 lemma exists_fin [finite R M] : ∃ (n : ℕ) (s : fin n → M), span R (range s) = ⊤ :=

src/ring_theory/noetherian.lean

@@ -75,6 +75,11 @@ lemma fg_iff_add_submonoid_fg (P : submodule ℕ M) :
 ⟨λ ⟨S, hS⟩, ⟨S, by simpa [← span_nat_eq_add_submonoid_closure] using hS⟩,
   λ ⟨S, hS⟩, ⟨S, by simpa [← span_nat_eq_add_submonoid_closure] using hS⟩⟩
 
+lemma fg_iff_add_subgroup_fg {G : Type*} [add_comm_group G] (P : submodule ℤ G) :
+  P.fg ↔ P.to_add_subgroup.fg :=
+⟨λ ⟨S, hS⟩, ⟨S, by simpa [← span_int_eq_add_subgroup_closure] using hS⟩,
+  λ ⟨S, hS⟩, ⟨S, by simpa [← span_int_eq_add_subgroup_closure] using hS⟩⟩
+
 lemma fg_iff_exists_fin_generating_family {N : submodule R M} :
   N.fg ↔ ∃ (n : ℕ) (s : fin n → M), span R (range s) = N :=
 begin