# Documentation

Mathlib.GroupTheory.Finiteness

# 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, AddSubmonoid.FG S : A submonoid S is finitely generated.
• Monoid.FG M, AddMonoid.FG M : A typeclass indicating a type M is finitely generated as a monoid.
• Subgroup.FG S, AddSubgroup.FG S : A subgroup S is finitely generated.
• Group.FG M, AddGroup.FG M : A typeclass indicating a type M is finitely generated as a group.

### Monoids and submonoids #

def AddSubmonoid.FG {M : Type u_1} [] (P : ) :

An additive submonoid of N is finitely generated if it is the closure of a finite subset of M.

Instances For
def Submonoid.FG {M : Type u_1} [] (P : ) :

A submonoid of M is finitely generated if it is the closure of a finite subset of M.

Instances For
abbrev AddSubmonoid.fg_iff.match_1 {M : Type u_1} [] (P : ) (motive : ) :
(x : ) → ((S : ) → (hS : ) → motive (_ : S, )) → motive x
Instances For
theorem AddSubmonoid.fg_iff {M : Type u_1} [] (P : ) :
S,

An equivalent expression of AddSubmonoid.FG in terms of Set.Finite instead of Finset.

abbrev AddSubmonoid.fg_iff.match_2 {M : Type u_1} [] (P : ) (motive : (S, ) → Prop) :
(x : S, ) → ((S : Set M) → (hS : ) → (hf : ) → motive (_ : S, )) → motive x
Instances For
theorem Submonoid.fg_iff {M : Type u_1} [] (P : ) :
S,

An equivalent expression of Submonoid.FG in terms of Set.Finite instead of Finset.

theorem Submonoid.fg_iff_add_fg {M : Type u_1} [] (P : ) :
theorem AddSubmonoid.fg_iff_mul_fg {N : Type u_2} [] (P : ) :
class Monoid.FG (M : Type u_1) [] :
• out :

A monoid is finitely generated if it is finitely generated as a submonoid of itself.

Instances
class AddMonoid.FG (N : Type u_2) [] :
• out :

An additive monoid is finitely generated if it is finitely generated as an additive submonoid of itself.

Instances
theorem Monoid.fg_def {M : Type u_1} [] :
theorem AddMonoid.fg_def {N : Type u_2} [] :
theorem AddMonoid.fg_iff {M : Type u_1} [] :
S,

An equivalent expression of AddMonoid.FG in terms of Set.Finite instead of Finset.

theorem Monoid.fg_iff {M : Type u_1} [] :
S,

An equivalent expression of Monoid.FG in terms of Set.Finite instead of Finset.

theorem Monoid.fg_iff_add_fg {M : Type u_1} [] :
theorem AddMonoid.fg_iff_mul_fg {N : Type u_2} [] :
instance AddMonoid.fg_of_monoid_fg {M : Type u_1} [] [] :
instance Monoid.fg_of_addMonoid_fg {N : Type u_2} [] [] :
theorem AddMonoid.fg_of_finite.proof_1 {M : Type u_1} [] [] :
instance AddMonoid.fg_of_finite {M : Type u_1} [] [] :
instance Monoid.fg_of_finite {M : Type u_1} [] [] :
theorem AddSubmonoid.FG.map {M : Type u_1} [] {M' : Type u_3} [] {P : } (h : ) (e : M →+ M') :
theorem Submonoid.FG.map {M : Type u_1} [] {M' : Type u_3} [Monoid M'] {P : } (h : ) (e : M →* M') :
theorem AddSubmonoid.FG.map_injective {M : Type u_1} [] {M' : Type u_3} [] {P : } (e : M →+ M') (he : ) (h : ) :
theorem Submonoid.FG.map_injective {M : Type u_1} [] {M' : Type u_3} [Monoid M'] {P : } (e : M →* M') (he : ) (h : ) :
@[simp]
AddMonoid.FG { x // x N }
@[simp]
theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [] (N : ) :
Monoid.FG { x // x N }
theorem AddMonoid.fg_of_surjective {M : Type u_1} [] {M' : Type u_3} [] [] (f : M →+ M') (hf : ) :
theorem Monoid.fg_of_surjective {M : Type u_1} [] {M' : Type u_3} [Monoid M'] [] (f : M →* M') (hf : ) :
instance AddMonoid.fg_range {M : Type u_1} [] {M' : Type u_3} [] [] (f : M →+ M') :
theorem AddMonoid.fg_range.proof_1 {M : Type u_1} [] {M' : Type u_2} [] [] (f : M →+ M') :
instance Monoid.fg_range {M : Type u_1} [] {M' : Type u_3} [Monoid M'] [] (f : M →* M') :
Monoid.FG { x // }
theorem AddSubmonoid.multiples_fg {M : Type u_1} [] (r : M) :
theorem Submonoid.powers_fg {M : Type u_1} [] (r : M) :
instance AddMonoid.multiples_fg {M : Type u_1} [] (r : M) :
theorem AddMonoid.multiples_fg.proof_1 {M : Type u_1} [] (r : M) :
instance Monoid.powers_fg {M : Type u_1} [] (r : M) :
Monoid.FG { x // }
theorem AddMonoid.closure_finset_fg.proof_1 {M : Type u_1} [] (s : ) :
instance AddMonoid.closure_finset_fg {M : Type u_1} [] (s : ) :
instance Monoid.closure_finset_fg {M : Type u_1} [] (s : ) :
Monoid.FG { x // }
instance AddMonoid.closure_finite_fg {M : Type u_1} [] (s : Set M) [Finite s] :
theorem AddMonoid.closure_finite_fg.proof_1 {M : Type u_1} [] (s : Set M) [Finite s] :
instance Monoid.closure_finite_fg {M : Type u_1} [] (s : Set M) [Finite s] :
Monoid.FG { x // }

### Groups and subgroups #

def AddSubgroup.FG {G : Type u_3} [] (P : ) :

An additive subgroup of H is finitely generated if it is the closure of a finite subset of H.

Instances For
def Subgroup.FG {G : Type u_3} [] (P : ) :

A subgroup of G is finitely generated if it is the closure of a finite subset of G.

Instances For
abbrev AddSubgroup.fg_iff.match_1 {G : Type u_1} [] (P : ) (motive : ) :
(x : ) → ((S : ) → (hS : ) → motive (_ : S, )) → motive x
Instances For
theorem AddSubgroup.fg_iff {G : Type u_3} [] (P : ) :
S,

An equivalent expression of AddSubgroup.fg in terms of Set.Finite instead of Finset.

abbrev AddSubgroup.fg_iff.match_2 {G : Type u_1} [] (P : ) (motive : (S, ) → Prop) :
(x : S, ) → ((S : Set G) → (hS : ) → (hf : ) → motive (_ : S, )) → motive x
Instances For
theorem Subgroup.fg_iff {G : Type u_3} [] (P : ) :
S,

An equivalent expression of Subgroup.FG in terms of Set.Finite instead of Finset.

An additive subgroup is finitely generated if and only if it is finitely generated as an additive submonoid.

theorem Subgroup.fg_iff_submonoid_fg {G : Type u_3} [] (P : ) :
Submonoid.FG P.toSubmonoid

A subgroup is finitely generated if and only if it is finitely generated as a submonoid.

theorem Subgroup.fg_iff_add_fg {G : Type u_3} [] (P : ) :
theorem AddSubgroup.fg_iff_mul_fg {H : Type u_4} [] (P : ) :
class Group.FG (G : Type u_3) [] :
• out :

A group is finitely generated if it is finitely generated as a submonoid of itself.

Instances
class AddGroup.FG (H : Type u_4) [] :
• out :

An additive group is finitely generated if it is finitely generated as an additive submonoid of itself.

Instances
theorem Group.fg_def {G : Type u_3} [] :
theorem AddGroup.fg_def {H : Type u_4} [] :
theorem AddGroup.fg_iff {G : Type u_3} [] :
S,

An equivalent expression of AddGroup.fg in terms of Set.Finite instead of Finset.

theorem Group.fg_iff {G : Type u_3} [] :
S,

An equivalent expression of Group.FG in terms of Set.Finite instead of Finset.

abbrev AddGroup.fg_iff'.match_1 {G : Type u_1} [] (motive : ) :
(x : ) → ((S : ) → (hS : ) → motive (_ : S, )) → motive x
Instances For
theorem AddGroup.fg_iff' {G : Type u_3} [] :
n S, = n
abbrev AddGroup.fg_iff'.match_2 {G : Type u_1} [] (motive : (n S, = n ) → Prop) :
(x : n S, = n ) → ((_n : ) → (S : ) → (_hn : = _n) → (hS : ) → motive (_ : n S, = n )) → motive x
Instances For
theorem Group.fg_iff' {G : Type u_3} [] :
n S, = n

An additive group is finitely generated if and only if it is finitely generated as an additive monoid.

theorem Group.fg_iff_monoid_fg {G : Type u_3} [] :

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

@[simp]
AddGroup.FG { x // x H }
@[simp]
theorem Group.fg_iff_subgroup_fg {G : Type u_3} [] (H : ) :
Group.FG { x // x H }
theorem GroupFG.iff_add_fg {G : Type u_3} [] :
theorem AddGroup.fg_iff_mul_fg {H : Type u_4} [] :
instance AddGroup.fg_of_group_fg {G : Type u_3} [] [] :
instance Group.fg_of_mul_group_fg {H : Type u_4} [] [] :
theorem AddGroup.fg_of_finite.proof_1 {G : Type u_1} [] [] :
instance AddGroup.fg_of_finite {G : Type u_3} [] [] :
instance Group.fg_of_finite {G : Type u_3} [] [] :
theorem AddGroup.fg_of_surjective {G : Type u_3} [] {G' : Type u_5} [AddGroup G'] [hG : ] {f : G →+ G'} (hf : ) :
theorem Group.fg_of_surjective {G : Type u_3} [] {G' : Type u_5} [Group G'] [hG : ] {f : G →* G'} (hf : ) :
instance AddGroup.fg_range {G : Type u_3} [] {G' : Type u_5} [AddGroup G'] [] (f : G →+ G') :
theorem AddGroup.fg_range.proof_1 {G : Type u_1} [] {G' : Type u_2} [AddGroup G'] [] (f : G →+ G') :
instance Group.fg_range {G : Type u_3} [] {G' : Type u_5} [Group G'] [] (f : G →* G') :
Group.FG { x // }
instance AddGroup.closure_finset_fg {G : Type u_3} [] (s : ) :
theorem AddGroup.closure_finset_fg.proof_1 {G : Type u_1} [] (s : ) :
instance Group.closure_finset_fg {G : Type u_3} [] (s : ) :
Group.FG { x // }
instance AddGroup.closure_finite_fg {G : Type u_3} [] (s : Set G) [Finite s] :
theorem AddGroup.closure_finite_fg.proof_1 {G : Type u_1} [] (s : Set G) [Finite s] :
instance Group.closure_finite_fg {G : Type u_3} [] (s : Set G) [Finite s] :
Group.FG { x // }
noncomputable def AddGroup.rank (G : Type u_3) [] [h : ] :

The minimum number of generators of an additive group

Instances For
theorem AddGroup.rank.proof_1 (G : Type u_1) [] [h : ] :
n S, = n
noncomputable def Group.rank (G : Type u_3) [] [h : ] :

The minimum number of generators of a group.

Instances For
theorem AddGroup.rank_spec (G : Type u_3) [] [h : ] :
S,
theorem Group.rank_spec (G : Type u_3) [] [h : ] :
S,
theorem AddGroup.rank_le (G : Type u_3) [] [h : ] {S : } (hS : ) :
theorem Group.rank_le (G : Type u_3) [] [h : ] {S : } (hS : ) :
theorem AddGroup.rank_le_of_surjective {G : Type u_3} [] {G' : Type u_5} [AddGroup G'] [] [] (f : G →+ G') (hf : ) :
theorem Group.rank_le_of_surjective {G : Type u_3} [] {G' : Type u_5} [Group G'] [] [Group.FG G'] (f : G →* G') (hf : ) :
theorem AddGroup.rank_range_le {G : Type u_3} [] {G' : Type u_5} [AddGroup G'] [] {f : G →+ G'} :
theorem Group.rank_range_le {G : Type u_3} [] {G' : Type u_5} [Group G'] [] {f : G →* G'} :
Group.rank { x // }
theorem AddGroup.rank_congr {G : Type u_3} [] {G' : Type u_5} [AddGroup G'] [] [] (f : G ≃+ G') :
theorem Group.rank_congr {G : Type u_3} [] {G' : Type u_5} [Group G'] [] [Group.FG G'] (f : G ≃* G') :
theorem AddSubgroup.rank_congr {G : Type u_3} [] {H : } {K : } [AddGroup.FG { x // x H }] [AddGroup.FG { x // x K }] (h : H = K) :
AddGroup.rank { x // x H } = AddGroup.rank { x // x K }
theorem Subgroup.rank_congr {G : Type u_3} [] {H : } {K : } [Group.FG { x // x H }] [Group.FG { x // x K }] (h : H = K) :
Group.rank { x // x H } = Group.rank { x // x K }
theorem Subgroup.rank_closure_finset_le_card {G : Type u_3} [] (s : ) :
Group.rank { x // }
theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_3} [] (s : Set G) [Finite s] :
Group.rank { x // } Nat.card s
theorem QuotientAddGroup.fg.proof_1 {G : Type u_1} [] [] (N : ) :
instance QuotientAddGroup.fg {G : Type u_3} [] [] (N : ) :
instance QuotientGroup.fg {G : Type u_3} [] [] (N : ) [] :