Mathlib.GroupTheory.Finiteness

Submonoid.FG definition

(P : Submonoid M) : Prop

Full source

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

Finitely generated submonoid

Informal description

A submonoid $ P $ of a monoid $ M $ is called finitely generated if there exists a finite subset $ S $ of $ M $ such that the submonoid generated by $ S $ is equal to $ P $.

Submonoid.fg_iff theorem

(P : Submonoid M) : Submonoid.FG P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite

Full source

/-- An equivalent expression of `Submonoid.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive "An equivalent expression of `AddSubmonoid.FG` in terms of `Set.Finite` instead of
`Finset`."]
theorem Submonoid.fg_iff (P : Submonoid M) :
    Submonoid.FGSubmonoid.FG P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
  ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
    ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩

Characterization of Finitely Generated Submonoids via Finite Generating Sets

Informal description

A submonoid $P$ of a monoid $M$ is finitely generated if and only if there exists a finite subset $S \subseteq M$ such that the submonoid generated by $S$ equals $P$.

Submonoid.fg_iff_add_fg theorem

(P : Submonoid M) : P.FG ↔ P.toAddSubmonoid.FG

Full source

theorem Submonoid.fg_iff_add_fg (P : Submonoid M) : P.FG ↔ P.toAddSubmonoid.FG :=
  ⟨fun h =>
    let ⟨S, hS, hf⟩ := (Submonoid.fg_iff _).1 h
    (AddSubmonoid.fg_iff _).mpr
      ⟨Additive.toMul ⁻¹' S, by simp [← Submonoid.toAddSubmonoid_closure, hS], hf⟩,
    fun h =>
    let ⟨T, hT, hf⟩ := (AddSubmonoid.fg_iff _).1 h
    (Submonoid.fg_iff _).mpr
      ⟨Additive.ofMul ⁻¹' T, by simp [← AddSubmonoid.toSubmonoid'_closure, hT], hf⟩⟩

Finitely Generated Submonoid iff Corresponding Additive Submonoid is Finitely Generated

Informal description

A submonoid $P$ of a monoid $M$ is finitely generated if and only if its corresponding additive submonoid $P.toAddSubmonoid$ is finitely generated.

AddSubmonoid.fg_iff_mul_fg theorem

{M : Type*} [AddMonoid M] (P : AddSubmonoid M) : P.FG ↔ P.toSubmonoid.FG

Full source

theorem AddSubmonoid.fg_iff_mul_fg {M : Type*} [AddMonoid M] (P : AddSubmonoid M) :
    P.FG ↔ P.toSubmonoid.FG := by
  convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

Finitely Generated Additive Submonoid iff Corresponding Multiplicative Submonoid is Finitely Generated

Informal description

For any additive submonoid $P$ of an additive monoid $M$, $P$ is finitely generated if and only if its corresponding multiplicative submonoid $P.toSubmonoid$ is finitely generated.

Submonoid.FG.prod theorem

(hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

Full source

/-- The product of finitely generated submonoids is finitely generated. -/
@[to_additive "The product of finitely generated submonoids is finitely generated."]
lemma Submonoid.FG.prod (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG := by
  classical
  obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [Submonoid.closure_union, hbM, hbN]

Product of Finitely Generated Submonoids is Finitely Generated

Informal description

Let $P$ and $Q$ be submonoids of monoids $M$ and $N$ respectively. If $P$ is finitely generated and $Q$ is finitely generated, then the product submonoid $P \times Q$ is also finitely generated.

AddMonoid.FG structure

(M : Type*) [AddMonoid M]

Full source

/-- An additive monoid is finitely generated if it is finitely generated as an additive submonoid of
itself. -/
@[mk_iff]
class AddMonoid.FG (M : Type*) [AddMonoid M] : Prop where
  fg_top : (⊤ : AddSubmonoid M).FG

Finitely generated additive monoid

Informal description

An additive monoid $M$ is finitely generated if it is finitely generated as an additive submonoid of itself. This means there exists a finite subset $S \subseteq M$ such that every element of $M$ can be expressed as a finite sum of elements from $S$.

Monoid.FG structure

Full source

/-- A monoid is finitely generated if it is finitely generated as a submonoid of itself. -/
@[to_additive]
class Monoid.FG : Prop where
  fg_top : (⊤ : Submonoid M).FG

Finitely generated monoid

Informal description

A monoid $ M $ is finitely generated if the submonoid generated by $ M $ itself (i.e., the top submonoid) is finitely generated. This is equivalent to the existence of a finite subset $ S \subseteq M $ such that the submonoid closure of $ S $ is equal to the entire monoid $ M $.

Monoid.fg_def theorem

: Monoid.FG M ↔ (⊤ : Submonoid M).FG

Full source

@[to_additive]
theorem Monoid.fg_def : Monoid.FGMonoid.FG M ↔ (⊤ : Submonoid M).FG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Characterization of Finitely Generated Monoids via Top Submonoid

Informal description

A monoid $M$ is finitely generated if and only if the top submonoid (i.e., $M$ itself) is finitely generated as a submonoid.

Monoid.fg_iff theorem

: Monoid.FG M ↔ ∃ S : Set M, Submonoid.closure S = (⊤ : Submonoid M) ∧ S.Finite

Full source

/-- An equivalent expression of `Monoid.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive
      "An equivalent expression of `AddMonoid.FG` in terms of `Set.Finite` instead of `Finset`."]
theorem Monoid.fg_iff :
    Monoid.FGMonoid.FG M ↔ ∃ S : Set M, Submonoid.closure S = (⊤ : Submonoid M) ∧ S.Finite :=
  ⟨fun _ => (Submonoid.fg_iff ⊤).1 FG.fg_top, fun h => ⟨(Submonoid.fg_iff ⊤).2 h⟩⟩

Characterization of Finitely Generated Monoids via Finite Generating Sets

Informal description

A monoid $M$ is finitely generated if and only if there exists a finite subset $S \subseteq M$ such that the submonoid generated by $S$ equals $M$ (i.e., $\text{closure}(S) = \top$ as a submonoid of $M$).

Monoid.fg_iff_add_fg theorem

: Monoid.FG M ↔ AddMonoid.FG (Additive M)

Full source

theorem Monoid.fg_iff_add_fg : Monoid.FGMonoid.FG M ↔ AddMonoid.FG (Additive M) where
  mp _ := ⟨(Submonoid.fg_iff_add_fg ⊤).1 FG.fg_top⟩
  mpr h := ⟨(Submonoid.fg_iff_add_fg ⊤).2 h.fg_top⟩

Finitely Generated Monoid iff Additive Version is Finitely Generated

Informal description

A monoid $M$ is finitely generated if and only if its additive counterpart $\text{Additive}\, M$ is finitely generated as an additive monoid.

AddMonoid.fg_iff_mul_fg theorem

{M : Type*} [AddMonoid M] : AddMonoid.FG M ↔ Monoid.FG (Multiplicative M)

Full source

theorem AddMonoid.fg_iff_mul_fg {M : Type*} [AddMonoid M] :
    AddMonoid.FGAddMonoid.FG M ↔ Monoid.FG (Multiplicative M) where
  mp _ := ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).1 FG.fg_top⟩
  mpr h := ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).2 h.fg_top⟩

Finitely Generated Additive Monoid iff Multiplicative Version is Finitely Generated

Informal description

An additive monoid $M$ is finitely generated if and only if its multiplicative counterpart $\text{Multiplicative}\, M$ is finitely generated as a monoid.

AddMonoid.fg_of_monoid_fg instance

[Monoid.FG M] : AddMonoid.FG (Additive M)

Full source

instance AddMonoid.fg_of_monoid_fg [Monoid.FG M] : AddMonoid.FG (Additive M) :=
  Monoid.fg_iff_add_fg.1 ‹_›

Finitely Generated Monoid Implies Finitely Generated Additive Monoid

Informal description

If a monoid $M$ is finitely generated, then its additive counterpart $\text{Additive}\, M$ is also finitely generated as an additive monoid.

Monoid.fg_of_addMonoid_fg instance

{M : Type*} [AddMonoid M] [AddMonoid.FG M] : Monoid.FG (Multiplicative M)

Full source

instance Monoid.fg_of_addMonoid_fg {M : Type*} [AddMonoid M] [AddMonoid.FG M] :
    Monoid.FG (Multiplicative M) :=
  AddMonoid.fg_iff_mul_fg.1 ‹_›

Finitely Generated Additive Monoid Implies Finitely Generated Multiplicative Monoid

Informal description

For any additive monoid $M$ that is finitely generated, its multiplicative counterpart $\text{Multiplicative}\, M$ is also finitely generated as a monoid.

Monoid.fg_of_finite instance

[Finite M] : Monoid.FG M

Full source

@[to_additive]
instance (priority := 100) Monoid.fg_of_finite [Finite M] : Monoid.FG M := by
  cases nonempty_fintype M
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩

Finite monoids are finitely generated

Informal description

Every finite monoid $M$ is finitely generated.

Submonoid.FG.map theorem

{M' : Type*} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') : (P.map e).FG

Full source

@[to_additive]
theorem Submonoid.FG.map {M' : Type*} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') :
    (P.map e).FG := by
  classical
    obtain ⟨s, rfl⟩ := h
    exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

Image of a Finitely Generated Submonoid under a Homomorphism is Finitely Generated

Informal description

Let $M'$ be a monoid, $P$ a submonoid of a monoid $M$, and $e \colon M \to M'$ a monoid homomorphism. If $P$ is finitely generated, then the image submonoid $e(P)$ is also finitely generated.

Submonoid.FG.map_injective theorem

{M' : Type*} [Monoid M'] {P : Submonoid M} (e : M →* M') (he : Function.Injective e) (h : (P.map e).FG) : P.FG

Full source

@[to_additive]
theorem 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 := by
  obtain ⟨s, hs⟩ := h
  use s.preimage e he.injOn
  apply Submonoid.map_injective_of_injective he
  rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
  congr
  rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]
  exact Submonoid.monotone_map le_top

Injective Homomorphism Preserves Finite Generation of Submonoids

Informal description

Let $M$ and $M'$ be monoids, $P$ a submonoid of $M$, and $e \colon M \to M'$ an injective monoid homomorphism. If the image submonoid $e(P)$ is finitely generated, then $P$ is also finitely generated.

Monoid.fg_iff_submonoid_fg theorem

(N : Submonoid M) : Monoid.FG N ↔ N.FG

Full source

@[to_additive (attr := simp)]
theorem Monoid.fg_iff_submonoid_fg (N : Submonoid M) : Monoid.FGMonoid.FG N ↔ N.FG := by
  conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
  exact ⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

Finite Generation of Submonoid as Monoid vs. Submonoid

Informal description

A submonoid $N$ of a monoid $M$ is finitely generated as a monoid if and only if $N$ is finitely generated as a submonoid of $M$.

Monoid.fg_of_surjective theorem

{M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') (hf : Function.Surjective f) : Monoid.FG M'

Full source

@[to_additive]
theorem Monoid.fg_of_surjective {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M')
    (hf : Function.Surjective f) : Monoid.FG M' := by
  classical
    obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

Surjective homomorphism preserves finite generation of monoids

Informal description

Let $M$ and $M'$ be monoids, with $M$ finitely generated. If $f \colon M \to M'$ is a surjective monoid homomorphism, then $M'$ is also finitely generated.

Monoid.fg_range instance

{M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') : Monoid.FG (MonoidHom.mrange f)

Full source

@[to_additive]
instance Monoid.fg_range {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') :
    Monoid.FG (MonoidHom.mrange f) :=
  Monoid.fg_of_surjective f.mrangeRestrict f.mrangeRestrict_surjective

Finite Generation of the Range of a Monoid Homomorphism

Informal description

For any monoids $M$ and $M'$ with $M$ finitely generated, and any monoid homomorphism $f \colon M \to M'$, the range of $f$ is a finitely generated monoid.

Submonoid.powers_fg theorem

(r : M) : (Submonoid.powers r).FG

Full source

@[to_additive]
theorem Submonoid.powers_fg (r : M) : (Submonoid.powers r).FG :=
  ⟨{r}, (Finset.coe_singleton r).symm ▸ (Submonoid.powers_eq_closure r).symm⟩

Finitely Generated Powers Submonoid

Informal description

For any element $r$ in a monoid $M$, the submonoid generated by the powers of $r$ is finitely generated.

Monoid.powers_fg instance

(r : M) : Monoid.FG (Submonoid.powers r)

Full source

@[to_additive]
instance Monoid.powers_fg (r : M) : Monoid.FG (Submonoid.powers r) :=
  (Monoid.fg_iff_submonoid_fg _).mpr (Submonoid.powers_fg r)

Finite Generation of Powers Submonoid

Informal description

For any element $r$ in a monoid $M$, the submonoid generated by the powers of $r$ is finitely generated as a monoid.

Monoid.closure_finset_fg instance

(s : Finset M) : Monoid.FG (Submonoid.closure (s : Set M))

Full source

@[to_additive]
instance Monoid.closure_finset_fg (s : Finset M) : Monoid.FG (Submonoid.closure (s : Set M)) := by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]

Finite Subsets Generate Finitely Generated Submonoids

Informal description

For any finite subset $s$ of a monoid $M$, the submonoid generated by $s$ is finitely generated.

Monoid.closure_finite_fg instance

(s : Set M) [Finite s] : Monoid.FG (Submonoid.closure s)

Full source

@[to_additive]
instance Monoid.closure_finite_fg (s : Set M) [Finite s] : Monoid.FG (Submonoid.closure s) :=
  haveI := Fintype.ofFinite s
  s.coe_toFinset ▸ Monoid.closure_finset_fg s.toFinset

Finite Subsets Generate Finitely Generated Submonoids

Informal description

For any finite subset $s$ of a monoid $M$, the submonoid generated by $s$ is finitely generated.

Subgroup.FG definition

(P : Subgroup G) : Prop

Full source

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

Finitely generated subgroup

Informal description

A subgroup $ P $ of a group $ G $ is finitely generated if there exists a finite subset $ S $ of $ G $ such that the subgroup generated by $ S $ is equal to $ P $.

Subgroup.fg_iff theorem

(P : Subgroup G) : Subgroup.FG P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite

Full source

/-- An equivalent expression of `Subgroup.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive "An equivalent expression of `AddSubgroup.fg` in terms of `Set.Finite` instead of
`Finset`."]
theorem Subgroup.fg_iff (P : Subgroup G) :
    Subgroup.FGSubgroup.FG P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite :=
  ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
    ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩

Characterization of Finitely Generated Subgroups via Finite Generating Sets

Informal description

A subgroup $ P $ of a group $ G $ is finitely generated if and only if there exists a finite subset $ S \subseteq G $ such that the subgroup generated by $ S $ equals $ P $. In other words: \[ \text{Subgroup.FG } P \iff \exists S \subseteq G, \text{Subgroup.closure } S = P \land S \text{ is finite.} \]

Subgroup.fg_iff_submonoid_fg theorem

(P : Subgroup G) : P.FG ↔ P.toSubmonoid.FG

Full source

/-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid. -/
@[to_additive "An additive subgroup is finitely generated if
and only if it is finitely generated as an additive submonoid."]
theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.FG ↔ P.toSubmonoid.FG := by
  constructor
  · rintro ⟨S, rfl⟩
    rw [Submonoid.fg_iff]
    refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩
    exact (Subgroup.closure_toSubmonoid _).symm
  · rintro ⟨S, hS⟩
    refine ⟨S, le_antisymm ?_ ?_⟩
    · rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
      exact Submonoid.subset_closure
    · rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
      exact Subgroup.subset_closure

Subgroup Finitely Generated iff Submonoid Finitely Generated

Informal description

For any subgroup $P$ of a group $G$, $P$ is finitely generated as a subgroup if and only if $P$ is finitely generated as a submonoid (when viewed as a submonoid of $G$).

Subgroup.fg_iff_add_fg theorem

(P : Subgroup G) : P.FG ↔ P.toAddSubgroup.FG

Full source

theorem Subgroup.fg_iff_add_fg (P : Subgroup G) : P.FG ↔ P.toAddSubgroup.FG := by
  rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
  exact (Subgroup.toSubmonoid P).fg_iff_add_fg

Subgroup Finitely Generated iff Additive Subgroup Finitely Generated

Informal description

For any subgroup $P$ of a group $G$, $P$ is finitely generated as a subgroup if and only if its corresponding additive subgroup $P.toAddSubgroup$ is finitely generated.

AddSubgroup.fg_iff_mul_fg theorem

(P : AddSubgroup H) : P.FG ↔ P.toSubgroup.FG

Full source

theorem AddSubgroup.fg_iff_mul_fg (P : AddSubgroup H) : P.FG ↔ P.toSubgroup.FG := by
  rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
  exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

Finitely Generated Additive Subgroup iff Corresponding Multiplicative Subgroup is Finitely Generated

Informal description

For any additive subgroup $P$ of an additive group $H$, $P$ is finitely generated if and only if its corresponding multiplicative subgroup $P.toSubgroup$ is finitely generated.

Group.FG structure

Full source

/-- A group is finitely generated if it is finitely generated as a subgroup of itself. -/
class Group.FG : Prop where
  out : (⊤ : Subgroup G).FG

Finitely generated group

Informal description

A group $G$ is finitely generated if it is finitely generated as a group, meaning there exists a finite subset $S \subseteq G$ such that the subgroup generated by $S$ is equal to $G$ itself.

AddGroup.FG structure

Full source

/-- An additive group is finitely generated if it is finitely generated as an additive subgroup of
itself. -/
class AddGroup.FG : Prop where
  out : (⊤ : AddSubgroup H).FG

Finitely generated additive group

Informal description

An additive group $H$ is finitely generated if the trivial subgroup $\top$ of $H$ is finitely generated as an additive subgroup. In other words, there exists a finite subset $S \subseteq H$ such that every element of $H$ can be expressed as a finite sum of elements from $S$ and their inverses.

Group.fg_def theorem

: Group.FG G ↔ (⊤ : Subgroup G).FG

Full source

theorem Group.fg_def : Group.FGGroup.FG G ↔ (⊤ : Subgroup G).FG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Characterization of Finitely Generated Groups via Trivial Subgroup

Informal description

A group $G$ is finitely generated if and only if the trivial subgroup $\top$ of $G$ is finitely generated as a subgroup.

AddGroup.fg_def theorem

: AddGroup.FG H ↔ (⊤ : AddSubgroup H).FG

Full source

theorem AddGroup.fg_def : AddGroup.FGAddGroup.FG H ↔ (⊤ : AddSubgroup H).FG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Characterization of Finitely Generated Additive Groups via Trivial Subgroup

Informal description

An additive group $H$ is finitely generated if and only if the trivial subgroup $\top$ of $H$ is finitely generated as an additive subgroup.

Group.fg_iff theorem

: Group.FG G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite

Full source

/-- An equivalent expression of `Group.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive
      "An equivalent expression of `AddGroup.fg` in terms of `Set.Finite` instead of `Finset`."]
theorem Group.fg_iff : Group.FGGroup.FG G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite :=
  ⟨fun h => (Subgroup.fg_iff ⊤).1 h.out, fun h => ⟨(Subgroup.fg_iff ⊤).2 h⟩⟩

Characterization of finitely generated groups via finite generating sets

Informal description

A group $G$ is finitely generated if and only if there exists a finite subset $S \subseteq G$ such that the subgroup generated by $S$ is equal to $G$ itself.

Group.fg_iff' theorem

: Group.FG G ↔ ∃ (n : _) (S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤

Full source

@[to_additive]
theorem Group.fg_iff' :
    Group.FGGroup.FG G ↔ ∃ (n : _) (S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤ :=
  Group.fg_def.trans ⟨fun ⟨S, hS⟩ => ⟨S.card, S, rfl, hS⟩, fun ⟨_n, S, _hn, hS⟩ => ⟨S, hS⟩⟩

Characterization of Finitely Generated Groups via Finite Cardinality Generating Sets

Informal description

A group $G$ is finitely generated if and only if there exists a natural number $n$ and a finite subset $S \subseteq G$ with $|S| = n$ such that the subgroup generated by $S$ is equal to $G$ itself.

Group.fg_iff_monoid_fg theorem

: Group.FG G ↔ Monoid.FG G

Full source

/-- A group is finitely generated if and only if it is finitely generated as a monoid. -/
@[to_additive "An additive group is finitely generated if and only
if it is finitely generated as an additive monoid."]
theorem Group.fg_iff_monoid_fg : Group.FGGroup.FG G ↔ Monoid.FG G :=
  ⟨fun h => Monoid.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).1 (Group.fg_def.1 h), fun h =>
    Group.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).2 (Monoid.fg_def.1 h)⟩

Finitely Generated Group iff Finitely Generated as Monoid

Informal description

A group $G$ is finitely generated if and only if it is finitely generated as a monoid.

Group.fg_iff_subgroup_fg theorem

(H : Subgroup G) : Group.FG H ↔ H.FG

Full source

@[to_additive (attr := simp)]
theorem Group.fg_iff_subgroup_fg (H : Subgroup G) : Group.FGGroup.FG H ↔ H.FG :=
  (fg_iff_monoid_fg.trans (Monoid.fg_iff_submonoid_fg _)).trans
    (Subgroup.fg_iff_submonoid_fg _).symm

Finitely Generated Group vs. Finitely Generated Subgroup

Informal description

For any subgroup $H$ of a group $G$, $H$ is finitely generated as a group if and only if $H$ is finitely generated as a subgroup of $G$.

GroupFG.iff_add_fg theorem

: Group.FG G ↔ AddGroup.FG (Additive G)

Full source

theorem GroupFG.iff_add_fg : Group.FGGroup.FG G ↔ AddGroup.FG (Additive G) :=
  ⟨fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).1 h.out⟩, fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).2 h.out⟩⟩

Finitely Generated Group iff Additive Version Finitely Generated

Informal description

A group $G$ is finitely generated if and only if its additive counterpart $\text{Additive}(G)$ is finitely generated as an additive group.

AddGroup.fg_iff_mul_fg theorem

: AddGroup.FG H ↔ Group.FG (Multiplicative H)

Full source

theorem AddGroup.fg_iff_mul_fg : AddGroup.FGAddGroup.FG H ↔ Group.FG (Multiplicative H) :=
  ⟨fun h => ⟨(AddSubgroup.fg_iff_mul_fg ⊤).1 h.out⟩, fun h =>
    ⟨(AddSubgroup.fg_iff_mul_fg ⊤).2 h.out⟩⟩

Finitely Generated Additive Group iff Multiplicative Version Finitely Generated

Informal description

An additive group $H$ is finitely generated if and only if its multiplicative counterpart $\text{Multiplicative}(H)$ is finitely generated as a group.

AddGroup.fg_of_group_fg instance

[Group.FG G] : AddGroup.FG (Additive G)

Full source

instance AddGroup.fg_of_group_fg [Group.FG G] : AddGroup.FG (Additive G) :=
  GroupFG.iff_add_fg.1 ‹_›

Finitely Generated Groups Imply Finitely Generated Additive Groups

Informal description

For any finitely generated group $G$, its additive counterpart $\text{Additive}(G)$ is also finitely generated as an additive group.

Group.fg_of_mul_group_fg instance

[AddGroup.FG H] : Group.FG (Multiplicative H)

Full source

instance Group.fg_of_mul_group_fg [AddGroup.FG H] : Group.FG (Multiplicative H) :=
  AddGroup.fg_iff_mul_fg.1 ‹_›

Finitely Generated Additive Groups Imply Finitely Generated Multiplicative Groups

Informal description

For any finitely generated additive group $H$, the multiplicative group $\text{Multiplicative}(H)$ is also finitely generated.

Group.fg_of_finite instance

[Finite G] : Group.FG G

Full source

@[to_additive]
instance (priority := 100) Group.fg_of_finite [Finite G] : Group.FG G := by
  cases nonempty_fintype G
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Subgroup.closure_univ⟩⟩

Finite Groups are Finitely Generated

Informal description

Every finite group $G$ is finitely generated.

Group.fg_of_surjective theorem

{G' : Type*} [Group G'] [hG : Group.FG G] {f : G →* G'} (hf : Function.Surjective f) : Group.FG G'

Full source

@[to_additive]
theorem Group.fg_of_surjective {G' : Type*} [Group G'] [hG : Group.FG G] {f : G →* G'}
    (hf : Function.Surjective f) : Group.FG G' :=
  Group.fg_iff_monoid_fg.mpr <|
    @Monoid.fg_of_surjective G _ G' _ (Group.fg_iff_monoid_fg.mp hG) f hf

Surjective homomorphism preserves finite generation of groups

Informal description

Let $G$ and $G'$ be groups, with $G$ finitely generated. If $f \colon G \to G'$ is a surjective group homomorphism, then $G'$ is also finitely generated.

Group.fg_range instance

{G' : Type*} [Group G'] [Group.FG G] (f : G →* G') : Group.FG f.range

Full source

@[to_additive]
instance Group.fg_range {G' : Type*} [Group G'] [Group.FG G] (f : G →* G') : Group.FG f.range :=
  Group.fg_of_surjective f.rangeRestrict_surjective

Range of a Homomorphism from a Finitely Generated Group is Finitely Generated

Informal description

For any finitely generated group $G$ and group homomorphism $f \colon G \to G'$, the range of $f$ is a finitely generated group.

Group.closure_finset_fg instance

(s : Finset G) : Group.FG (Subgroup.closure (s : Set G))

Full source

@[to_additive]
instance Group.closure_finset_fg (s : Finset G) : Group.FG (Subgroup.closure (s : Set G)) := by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]

Finite Subsets Generate Finitely Generated Subgroups

Informal description

For any finite subset $s$ of a group $G$, the subgroup generated by $s$ is finitely generated.

Group.closure_finite_fg instance

(s : Set G) [Finite s] : Group.FG (Subgroup.closure s)

Full source

@[to_additive]
instance Group.closure_finite_fg (s : Set G) [Finite s] : Group.FG (Subgroup.closure s) :=
  haveI := Fintype.ofFinite s
  s.coe_toFinset ▸ Group.closure_finset_fg s.toFinset

Finite Subsets Generate Finitely Generated Subgroups

Informal description

For any finite subset $s$ of a group $G$, the subgroup generated by $s$ is finitely generated.

QuotientGroup.fg instance

[Group.FG G] (N : Subgroup G) [Subgroup.Normal N] : Group.FG <| G ⧸ N

Full source

@[to_additive]
instance QuotientGroup.fg [Group.FG G] (N : Subgroup G) [Subgroup.Normal N] : Group.FG <| G ⧸ N :=
  Group.fg_of_surjective <| QuotientGroup.mk'_surjective N

Finite Generation of Quotient Groups

Informal description

For any finitely generated group $G$ and normal subgroup $N$ of $G$, the quotient group $G/N$ is also finitely generated.

Prod.instMonoidFG instance

[FG M] [FG N] : FG (M × N)

Full source

/-- The product of finitely generated monoids is finitely generated. -/
@[to_additive "The product of finitely generated monoids is finitely generated."]
instance instMonoidFG [FG M] [FG N] : FG (M × N) where
  fg_top := by rw [← Submonoid.top_prod_top]; exact .prod ‹FG M›.fg_top ‹FG N›.fg_top

Product of Finitely Generated Monoids is Finitely Generated

Informal description

For any finitely generated monoids $M$ and $N$, the product monoid $M \times N$ is also finitely generated.

Main definition