<commit_before>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/

import data.set.finite
import group_theory.submonoid.operations
import group_theory.subgroup.basic

/-!
# Finitely generated monoids and groups

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_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 -/

open_locale pointwise
variables {M N : Type*} [monoid M] [add_monoid N]

section submonoid

/-- A submonoid of `M` is finitely generated if it is the closure of a finite subset of `M`. -/
@[to_additive]
def submonoid.fg (P : submonoid M) : Prop := ∃ S : finset M, submonoid.closure ↑S = P

/-- An additive submonoid of `N` is finitely generated if it is the closure of a finite subset of
`M`. -/
add_decl_doc add_submonoid.fg

/-- An equivalent expression of `submonoid.fg` in terms of `set.finite` instead of `finset`. -/
@[to_additive "An equivalent expression of `add_submonoid.fg` in terms of `set.finite` instead of
`finset`."]
lemma submonoid.fg_iff (P : submonoid M) : submonoid.fg P ↔
  ∃ S : set M, submonoid.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]⟩⟩

lemma submonoid.fg_iff_add_fg (P : submonoid M) : P.fg ↔ P.to_add_submonoid.fg :=
⟨λ h, let ⟨S, hS, hf⟩ := (submonoid.fg_iff _).1 h in (add_submonoid.fg_iff _).mpr
  ⟨additive.to_mul ⁻¹' S, by simp [← submonoid.to_add_submonoid_closure, hS], hf⟩,
 λ h, let ⟨T, hT, hf⟩ := (add_submonoid.fg_iff _).1 h in (submonoid.fg_iff _).mpr
  ⟨multiplicative.of_add ⁻¹' T, by simp [← add_submonoid.to_submonoid'_closure, hT], hf⟩⟩

lemma add_submonoid.fg_iff_mul_fg (P : add_submonoid N) : P.fg ↔ P.to_submonoid.fg :=
begin
  convert (submonoid.fg_iff_add_fg P.to_submonoid).symm,
  exact set_like.ext' rfl
end

end submonoid

section monoid

variables (M N)

/-- A monoid is finitely generated if it is finitely generated as a submonoid of itself. -/
class monoid.fg : Prop := (out : (⊤ : submonoid M).fg)

/-- An additive monoid is finitely generated if it is finitely generated as an additive submonoid of
itself. -/
class add_monoid.fg : Prop := (out : (⊤ : add_submonoid N).fg)

attribute [to_additive] monoid.fg

variables {M N}

lemma monoid.fg_def : monoid.fg M ↔ (⊤ : submonoid M).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩

lemma add_monoid.fg_def : add_monoid.fg N ↔ (⊤ : add_submonoid N).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩

/-- An equivalent expression of `monoid.fg` in terms of `set.finite` instead of `finset`. -/
@[to_additive "An equivalent expression of `add_monoid.fg` in terms of `set.finite` instead of
`finset`."]
lemma monoid.fg_iff : monoid.fg M ↔
  ∃ S : set M, submonoid.closure S = (⊤ : submonoid M) ∧ S.finite :=
⟨λ h, (submonoid.fg_iff ⊤).1 h.out, λ h, ⟨(submonoid.fg_iff ⊤).2 h⟩⟩

lemma monoid.fg_iff_add_fg : monoid.fg M ↔ add_monoid.fg (additive M) :=
⟨λ h, ⟨(submonoid.fg_iff_add_fg ⊤).1 h.out⟩, λ h, ⟨(submonoid.fg_iff_add_fg ⊤).2 h.out⟩⟩

lemma add_monoid.fg_iff_mul_fg : add_monoid.fg N ↔ monoid.fg (multiplicative N) :=
⟨λ h, ⟨(add_submonoid.fg_iff_mul_fg ⊤).1 h.out⟩, λ h, ⟨(add_submonoid.fg_iff_mul_fg ⊤).2 h.out⟩⟩

instance add_monoid.fg_of_monoid_fg [monoid.fg M] : add_monoid.fg (additive M) :=
monoid.fg_iff_add_fg.1 ‹_›

instance monoid.fg_of_add_monoid_fg [add_monoid.fg N] : monoid.fg (multiplicative N) :=
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<commit_msg>feat(group_theory/finiteness): Lemmas about finitely generated submonoids (#10681)<commit_after>/-
Copyright (c) 2021 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/

import data.set.finite
import data.finset
import group_theory.submonoid.operations
import group_theory.subgroup.basic

/-!
# Finitely generated monoids and groups

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_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 -/

open_locale pointwise
variables {M N : Type*} [monoid M] [add_monoid N]

section submonoid

/-- A submonoid of `M` is finitely generated if it is the closure of a finite subset of `M`. -/
@[to_additive]
def submonoid.fg (P : submonoid M) : Prop := ∃ S : finset M, submonoid.closure ↑S = P

/-- An additive submonoid of `N` is finitely generated if it is the closure of a finite subset of
`M`. -/
add_decl_doc add_submonoid.fg

/-- An equivalent expression of `submonoid.fg` in terms of `set.finite` instead of `finset`. -/
@[to_additive "An equivalent expression of `add_submonoid.fg` in terms of `set.finite` instead of
`finset`."]
lemma submonoid.fg_iff (P : submonoid M) : submonoid.fg P ↔
  ∃ S : set M, submonoid.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]⟩⟩

lemma submonoid.fg_iff_add_fg (P : submonoid M) : P.fg ↔ P.to_add_submonoid.fg :=
⟨λ h, let ⟨S, hS, hf⟩ := (submonoid.fg_iff _).1 h in (add_submonoid.fg_iff _).mpr
  ⟨additive.to_mul ⁻¹' S, by simp [← submonoid.to_add_submonoid_closure, hS], hf⟩,
 λ h, let ⟨T, hT, hf⟩ := (add_submonoid.fg_iff _).1 h in (submonoid.fg_iff _).mpr
  ⟨multiplicative.of_add ⁻¹' T, by simp [← add_submonoid.to_submonoid'_closure, hT], hf⟩⟩

lemma add_submonoid.fg_iff_mul_fg (P : add_submonoid N) : P.fg ↔ P.to_submonoid.fg :=
begin
  convert (submonoid.fg_iff_add_fg P.to_submonoid).symm,
  exact set_like.ext' rfl
end

end submonoid

section monoid

variables (M N)

/-- A monoid is finitely generated if it is finitely generated as a submonoid of itself. -/
class monoid.fg : Prop := (out : (⊤ : submonoid M).fg)

/-- An additive monoid is finitely generated if it is finitely generated as an additive submonoid of
itself. -/
class add_monoid.fg : Prop := (out : (⊤ : add_submonoid N).fg)

attribute [to_additive] monoid.fg

variables {M N}

lemma monoid.fg_def : monoid.fg M ↔ (⊤ : submonoid M).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩

lemma add_monoid.fg_def : add_monoid.fg N ↔ (⊤ : add_submonoid N).fg := ⟨λ h, h.1, λ h, ⟨h⟩⟩

/-- An equivalent expression of `monoid.fg` in terms of `set.finite` instead of `finset`. -/
@[to_additive "An equivalent expression of `add_monoid.fg` in terms of `set.finite` instead of
`finset`."]
lemma monoid.fg_iff : monoid.fg M ↔
  ∃ S : set M, submonoid.closure S = (⊤ : submonoid M) ∧ S.finite :=
⟨λ h, (submonoid.fg_iff ⊤).1 h.out, λ h, ⟨(submonoid.fg_iff ⊤).2 h⟩⟩

lemma monoid.fg_iff_add_fg : monoid.fg M ↔ add_monoid.fg (additive M) :=
⟨λ h, ⟨(submonoid.fg_iff_add_fg ⊤).1 h.out⟩, λ h, ⟨(submonoid.fg_iff_add_fg ⊤).2 h.out⟩⟩

lemma add_monoid.fg_iff_mul_fg : add_monoid.fg N ↔ monoid.fg (multiplicative N) :=
⟨λ h, ⟨(add_submonoid.fg_iff_mul_fg ⊤).1 h.out⟩, λ h, ⟨(add_submonoid.fg_iff_mul_fg ⊤).2 h.out⟩⟩

instance add_monoid.fg_of_monoid_fg [monoid.fg M] : add_monoid.fg (additive M) :=
monoid.fg_iff_add_fg.1 ‹_›

instance monoid.fg_of_add_monoid_fg [add_monoid.fg N] : monoid.fg (multiplicative N) :=
add_monoid.fg_iff_mul_fg.1 ‹_›

end monoid

@[to_additive]
lemma submonoid.fg.map {M' : Type*} [monoid M'] {P : submonoid M} (h : P.fg) (e : M →* M') :
  (P.map e).fg :=
begin
  classical,
  obtain ⟨s, rfl⟩ := h,
  exact ⟨s.image e, by rw [finset.coe_image, monoid_hom.map_mclosure]⟩
end

@[to_additive]
lemma submonoid.fg.map_injective {M' : Type*} [monoid M'] {P : submonoid M}
  (e : M →* M') (he : function.injective e) (h : (P.map e).fg) : P.fg :=
begin
  obtain ⟨s, hs⟩ := h,
  use s.preimage e (he.inj_on _),
  apply submonoid.map_injective_of_injective he,
  rw [← hs, e.map_mclosure, finset.coe_preimage],
  congr,
  rw [set.image_preimage_eq_iff, ← e.coe_mrange, ← submonoid.closure_le, hs, e.mrange_eq_map],
  exact submonoid.monotone_map le_top
end

@[simp, to_additive]
lemma monoid.fg_iff_submonoid_fg (N : submonoid M) : monoid.fg N ↔ N.fg :=
begin
  conv_rhs { rw [← N.range_subtype, monoid_hom.mrange_eq_map] },
  exact ⟨λ h, h.out.map N.subtype, λ h, ⟨h.map_injective N.subtype subtype.coe_injective⟩⟩
end

@[to_additive]
lemma monoid.fg_of_surjective {M' : Type*} [monoid M'] [monoid.fg M]
  (f : M →* M') (hf : function.surjective f) : monoid.fg M' :=
begin
  classical,
  obtain ⟨s, hs⟩ := monoid.fg_def.mp ‹_›,
  use s.image f,
  rwa [finset.coe_image, ← monoid_hom.map_mclosure, hs, ← monoid_hom.mrange_eq_map,
    monoid_hom.mrange_top_iff_surjective],
end

@[to_additive]
lemma submonoid.powers_fg (r : M) : (submonoid.powers r).fg :=
⟨{r}, (finset.coe_singleton r).symm ▸ (submonoid.powers_eq_closure r).symm⟩

@[to_additive]
instance (r : M) : monoid.fg (submonoid.powers r) :=
(monoid.fg_iff_submonoid_fg _).mpr (submonoid.powers_fg r)

/-! ### 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
{'fraction_non_alphanumeric': 0.13904892100380822, 'fraction_numerical': 0.00400351528171077, 'mean_word_length': 3.9863680623174296, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6518388', 'n_tokens_mistral': 4380, 'n_tokens_neox': 4393, 'n_words': 1279}