# mathlib3documentation

group_theory.finiteness

# Finitely generated monoids and groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

def add_submonoid.fg {M : Type u_1} [add_monoid M] (P : add_submonoid M) :
Prop

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

Equations
def submonoid.fg {M : Type u_1} [monoid M] (P : submonoid M) :
Prop

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

Equations
theorem submonoid.fg_iff {M : Type u_1} [monoid M] (P : submonoid M) :
P.fg (S : set M), S.finite

An equivalent expression of submonoid.fg in terms of set.finite instead of finset.

theorem add_submonoid.fg_iff {M : Type u_1} [add_monoid M] (P : add_submonoid M) :
P.fg (S : set M),

An equivalent expression of add_submonoid.fg in terms of set.finite instead of finset.

theorem submonoid.fg_iff_add_fg {M : Type u_1} [monoid M] (P : submonoid M) :
@[class]
structure monoid.fg (M : Type u_1) [monoid M] :
Prop

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

Instances of this typeclass
@[class]
structure add_monoid.fg (N : Type u_2) [add_monoid N] :
Prop

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

Instances of this typeclass
theorem monoid.fg_def {M : Type u_1} [monoid M] :
theorem add_monoid.fg_def {N : Type u_2} [add_monoid N] :
theorem monoid.fg_iff {M : Type u_1} [monoid M] :
(S : set M),

An equivalent expression of monoid.fg in terms of set.finite instead of finset.

theorem add_monoid.fg_iff {M : Type u_1} [add_monoid M] :
(S : set M),

An equivalent expression of add_monoid.fg in terms of set.finite instead of finset.

theorem monoid.fg_iff_add_fg {M : Type u_1} [monoid M] :
theorem add_monoid.fg_iff_mul_fg {N : Type u_2} [add_monoid N] :
@[protected, instance]
def add_monoid.fg_of_monoid_fg {M : Type u_1} [monoid M] [monoid.fg M] :
@[protected, instance]
@[protected, instance]
def monoid.fg_of_finite {M : Type u_1} [monoid M] [finite M] :
@[protected, instance]
def add_monoid.fg_of_finite {M : Type u_1} [add_monoid M] [finite M] :
theorem submonoid.fg.map {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] {P : submonoid M} (h : P.fg) (e : M →* M') :
P).fg
theorem add_submonoid.fg.map {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] {P : add_submonoid M} (h : P.fg) (e : M →+ M') :
P).fg
theorem add_submonoid.fg.map_injective {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] {P : add_submonoid M} (e : M →+ M') (he : function.injective e) (h : P).fg) :
P.fg
theorem submonoid.fg.map_injective {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] {P : submonoid M} (e : M →* M') (he : function.injective e) (h : P).fg) :
P.fg
@[simp]
@[simp]
theorem monoid.fg_iff_submonoid_fg {M : Type u_1} [monoid M] (N : submonoid M) :
N.fg
theorem add_monoid.fg_of_surjective {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] (f : M →+ M') (hf : function.surjective f) :
theorem monoid.fg_of_surjective {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] [monoid.fg M] (f : M →* M') (hf : function.surjective f) :
@[protected, instance]
def monoid.fg_range {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] [monoid.fg M] (f : M →* M') :
@[protected, instance]
def add_monoid.fg_range {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] (f : M →+ M') :
theorem submonoid.powers_fg {M : Type u_1} [monoid M] (r : M) :
theorem add_submonoid.multiples_fg {M : Type u_1} [add_monoid M] (r : M) :
@[protected, instance]
def add_monoid.multiples_fg {M : Type u_1} [add_monoid M] (r : M) :
@[protected, instance]
def monoid.powers_fg {M : Type u_1} [monoid M] (r : M) :
@[protected, instance]
def add_monoid.closure_finset_fg {M : Type u_1} [add_monoid M] (s : finset M) :
@[protected, instance]
def monoid.closure_finset_fg {M : Type u_1} [monoid M] (s : finset M) :
@[protected, instance]
def add_monoid.closure_finite_fg {M : Type u_1} [add_monoid M] (s : set M) [finite s] :
@[protected, instance]
def monoid.closure_finite_fg {M : Type u_1} [monoid M] (s : set M) [finite s] :

### Groups and subgroups #

def add_subgroup.fg {G : Type u_3} [add_group G] (P : add_subgroup G) :
Prop

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

Equations
def subgroup.fg {G : Type u_3} [group G] (P : subgroup G) :
Prop

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

Equations
theorem subgroup.fg_iff {G : Type u_3} [group G] (P : subgroup G) :
P.fg (S : set G), S.finite

An equivalent expression of subgroup.fg in terms of set.finite instead of finset.

theorem add_subgroup.fg_iff {G : Type u_3} [add_group G] (P : add_subgroup G) :
P.fg (S : set G), S.finite

An equivalent expression of add_subgroup.fg in terms of set.finite instead of finset.

theorem subgroup.fg_iff_submonoid_fg {G : Type u_3} [group G] (P : subgroup G) :

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

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

theorem subgroup.fg_iff_add_fg {G : Type u_3} [group G] (P : subgroup G) :
theorem add_subgroup.fg_iff_mul_fg {H : Type u_4} [add_group H] (P : add_subgroup H) :
@[class]
structure group.fg (G : Type u_3) [group G] :
Prop

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

Instances of this typeclass
@[class]
structure add_group.fg (H : Type u_4) [add_group H] :
Prop

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

Instances of this typeclass
theorem group.fg_def {G : Type u_3} [group G] :
theorem add_group.fg_def {H : Type u_4} [add_group H] :
theorem add_group.fg_iff {G : Type u_3} [add_group G] :
(S : set G),

An equivalent expression of add_group.fg in terms of set.finite instead of finset.

theorem group.fg_iff {G : Type u_3} [group G] :
(S : set G),

An equivalent expression of group.fg in terms of set.finite instead of finset.

theorem add_group.fg_iff' {G : Type u_3} [add_group G] :
(n : ) (S : finset G), S.card = n
theorem group.fg_iff' {G : Type u_3} [group G] :
(n : ) (S : finset G), S.card = n
theorem group.fg_iff_monoid.fg {G : Type u_3} [group G] :

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

theorem add_group.fg_iff_add_monoid.fg {G : Type u_3} [add_group G] :

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

theorem group_fg.iff_add_fg {G : Type u_3} [group G] :
theorem add_group.fg_iff_mul_fg {H : Type u_4} [add_group H] :
@[protected, instance]
def add_group.fg_of_group_fg {G : Type u_3} [group G] [group.fg G] :
@[protected, instance]
@[protected, instance]
def group.fg_of_finite {G : Type u_3} [group G] [finite G] :
@[protected, instance]
def add_group.fg_of_finite {G : Type u_3} [add_group G] [finite G] :
theorem add_group.fg_of_surjective {G : Type u_3} [add_group G] {G' : Type u_1} [add_group G'] [hG : add_group.fg G] {f : G →+ G'} (hf : function.surjective f) :
theorem group.fg_of_surjective {G : Type u_3} [group G] {G' : Type u_1} [group G'] [hG : group.fg G] {f : G →* G'} (hf : function.surjective f) :
@[protected, instance]
def add_group.fg_range {G : Type u_3} [add_group G] {G' : Type u_1} [add_group G'] [add_group.fg G] (f : G →+ G') :
@[protected, instance]
def group.fg_range {G : Type u_3} [group G] {G' : Type u_1} [group G'] [group.fg G] (f : G →* G') :
@[protected, instance]
def add_group.closure_finset_fg {G : Type u_3} [add_group G] (s : finset G) :
@[protected, instance]
def group.closure_finset_fg {G : Type u_3} [group G] (s : finset G) :
@[protected, instance]
def add_group.closure_finite_fg {G : Type u_3} [add_group G] (s : set G) [finite s] :
@[protected, instance]
def group.closure_finite_fg {G : Type u_3} [group G] (s : set G) [finite s] :
noncomputable def add_group.rank (G : Type u_3) [add_group G] [h : add_group.fg G] :

The minimum number of generators of an additive group

Equations
noncomputable def group.rank (G : Type u_3) [group G] [h : group.fg G] :

The minimum number of generators of a group.

Equations
theorem group.rank_spec (G : Type u_3) [group G] [h : group.fg G] :
(S : finset G), S.card =
theorem add_group.rank_spec (G : Type u_3) [add_group G] [h : add_group.fg G] :
(S : finset G),
theorem add_group.rank_le (G : Type u_3) [add_group G] [h : add_group.fg G] {S : finset G} (hS : = ) :
theorem group.rank_le (G : Type u_3) [group G] [h : group.fg G] {S : finset G} (hS : = ) :
theorem add_group.rank_le_of_surjective {G : Type u_3} [add_group G] {G' : Type u_5} [add_group G'] [add_group.fg G] [add_group.fg G'] (f : G →+ G') (hf : function.surjective f) :
theorem group.rank_le_of_surjective {G : Type u_3} [group G] {G' : Type u_5} [group G'] [group.fg G] [group.fg G'] (f : G →* G') (hf : function.surjective f) :
theorem group.rank_range_le {G : Type u_3} [group G] {G' : Type u_5} [group G'] [group.fg G] {f : G →* G'} :
theorem add_group.rank_range_le {G : Type u_3} [add_group G] {G' : Type u_5} [add_group G'] [add_group.fg G] {f : G →+ G'} :
theorem group.rank_congr {G : Type u_3} [group G] {G' : Type u_5} [group G'] [group.fg G] [group.fg G'] (f : G ≃* G') :
theorem add_group.rank_congr {G : Type u_3} [add_group G] {G' : Type u_5} [add_group G'] [add_group.fg G] [add_group.fg G'] (f : G ≃+ G') :
theorem subgroup.rank_congr {G : Type u_3} [group G] {H K : subgroup G} [group.fg H] [group.fg K] (h : H = K) :
theorem add_subgroup.rank_congr {G : Type u_3} [add_group G] {H K : add_subgroup G} (h : H = K) :
theorem subgroup.rank_closure_finset_le_card {G : Type u_3} [group G] (s : finset G) :
@[protected, instance]
def quotient_group.fg {G : Type u_3} [group G] [group.fg G] (N : subgroup G) [N.normal] :
@[protected, instance]