# 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.

Equations
• P.FG = ∃ (S : ),
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.

Equations
• P.FG = ∃ (S : ),
Instances For
abbrev AddSubmonoid.fg_iff.match_1 {M : Type u_1} [] (P : ) (motive : P.FGProp) :
∀ (x : P.FG), (∀ (S : ) (hS : ), motive )motive x
Equations
• =
Instances For
abbrev AddSubmonoid.fg_iff.match_2 {M : Type u_1} [] (P : ) (motive : (∃ (S : Set M), S.Finite)Prop) :
∀ (x : ∃ (S : Set M), S.Finite), (∀ (S : Set M) (hS : ) (hf : S.Finite), motive )motive x
Equations
• =
Instances For
theorem AddSubmonoid.fg_iff {M : Type u_1} [] (P : ) :
P.FG ∃ (S : Set M), S.Finite

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

theorem Submonoid.fg_iff {M : Type u_1} [] (P : ) :
P.FG ∃ (S : Set M), S.Finite

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) [] :

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

Instances
theorem Monoid.FG.out {M : Type u_1} [] [self : ] :
.FG
class AddMonoid.FG (N : Type u_2) [] :

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

Instances
theorem AddMonoid.FG.out {N : Type u_2} [] [self : ] :
.FG
theorem Monoid.fg_def {M : Type u_1} [] :
.FG
theorem AddMonoid.fg_def {N : Type u_2} [] :
.FG
theorem AddMonoid.fg_iff {M : Type u_1} [] :
∃ (S : Set M), S.Finite

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

theorem Monoid.fg_iff {M : Type u_1} [] :
∃ (S : Set M), S.Finite

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} [] [] :
Equations
• =
instance Monoid.fg_of_addMonoid_fg {N : Type u_2} [] [] :
Equations
• =
@[instance 100]
instance AddMonoid.fg_of_finite {M : Type u_1} [] [] :
Equations
• =
@[instance 100]
instance Monoid.fg_of_finite {M : Type u_1} [] [] :
Equations
• =
theorem AddSubmonoid.FG.map {M : Type u_1} [] {M' : Type u_3} [] {P : } (h : P.FG) (e : M →+ M') :
().FG
theorem Submonoid.FG.map {M : Type u_1} [] {M' : Type u_3} [Monoid M'] {P : } (h : P.FG) (e : M →* M') :
().FG
theorem AddSubmonoid.FG.map_injective {M : Type u_1} [] {M' : Type u_3} [] {P : } (e : M →+ M') (he : ) (h : ().FG) :
P.FG
theorem Submonoid.FG.map_injective {M : Type u_1} [] {M' : Type u_3} [Monoid M'] {P : } (e : M →* M') (he : ) (h : ().FG) :
P.FG
@[simp]
theorem AddMonoid.fg_iff_addSubmonoid_fg {M : Type u_1} [] (N : ) :
N.FG
@[simp]
theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [] (N : ) :
N.FG
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') :
Equations
• =
instance Monoid.fg_range {M : Type u_1} [] {M' : Type u_3} [Monoid M'] [] (f : M →* M') :
Equations
• =
theorem AddSubmonoid.multiples_fg {M : Type u_1} [] (r : M) :
.FG
theorem Submonoid.powers_fg {M : Type u_1} [] (r : M) :
().FG
instance AddMonoid.multiples_fg {M : Type u_1} [] (r : M) :
Equations
• =
instance Monoid.powers_fg {M : Type u_1} [] (r : M) :
Equations
• =
instance AddMonoid.closure_finset_fg {M : Type u_1} [] (s : ) :
Equations
• =
instance Monoid.closure_finset_fg {M : Type u_1} [] (s : ) :
Equations
• =
instance AddMonoid.closure_finite_fg {M : Type u_1} [] (s : Set M) [Finite s] :
Equations
• =
instance Monoid.closure_finite_fg {M : Type u_1} [] (s : Set M) [Finite s] :
Equations
• =

### 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.

Equations
• P.FG = ∃ (S : ),
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.

Equations
• P.FG = ∃ (S : ),
Instances For
abbrev AddSubgroup.fg_iff.match_1 {G : Type u_1} [] (P : ) (motive : P.FGProp) :
∀ (x : P.FG), (∀ (S : ) (hS : ), motive )motive x
Equations
• =
Instances For
abbrev AddSubgroup.fg_iff.match_2 {G : Type u_1} [] (P : ) (motive : (∃ (S : Set G), S.Finite)Prop) :
∀ (x : ∃ (S : Set G), S.Finite), (∀ (S : Set G) (hS : ) (hf : S.Finite), motive )motive x
Equations
• =
Instances For
theorem AddSubgroup.fg_iff {G : Type u_3} [] (P : ) :
P.FG ∃ (S : Set G), S.Finite

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

theorem Subgroup.fg_iff {G : Type u_3} [] (P : ) :
P.FG ∃ (S : Set G), S.Finite

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

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

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 : ) :
P.FG P.FG

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) [] :

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

Instances
theorem Group.FG.out {G : Type u_3} [] [self : ] :
.FG
class AddGroup.FG (H : Type u_4) [] :

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

Instances
theorem AddGroup.FG.out {H : Type u_4} [] [self : ] :
.FG
theorem Group.fg_def {G : Type u_3} [] :
.FG
theorem AddGroup.fg_def {H : Type u_4} [] :
.FG
theorem AddGroup.fg_iff {G : Type u_3} [] :
∃ (S : Set G), S.Finite

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

theorem Group.fg_iff {G : Type u_3} [] :
∃ (S : Set G), S.Finite

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

theorem AddGroup.fg_iff' {G : Type u_3} [] :
∃ (n : ) (S : ), S.card = n
abbrev AddGroup.fg_iff'.match_1 {G : Type u_1} [] (motive : .FGProp) :
∀ (x : .FG), (∀ (S : ) (hS : ), motive )motive x
Equations
• =
Instances For
abbrev AddGroup.fg_iff'.match_2 {G : Type u_1} [] (motive : (∃ (n : ) (S : ), S.card = n )Prop) :
∀ (x : ∃ (n : ) (S : ), S.card = n ), (∀ (_n : ) (S : ) (_hn : S.card = _n) (hS : ), motive )motive x
Equations
• =
Instances For
theorem Group.fg_iff' {G : Type u_3} [] :
∃ (n : ) (S : ), S.card = n
theorem AddGroup.fg_iff_addMonoid_fg {G : Type u_3} [] :

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]
theorem AddGroup.fg_iff_addSubgroup_fg {G : Type u_3} [] (H : ) :
H.FG
@[simp]
theorem Group.fg_iff_subgroup_fg {G : Type u_3} [] (H : ) :
Group.FG H H.FG
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} [] [] :
Equations
• =
instance Group.fg_of_mul_group_fg {H : Type u_4} [] [] :
Equations
• =
@[instance 100]
instance AddGroup.fg_of_finite {G : Type u_3} [] [] :
Equations
• =
@[instance 100]
instance Group.fg_of_finite {G : Type u_3} [] [] :
Equations
• =
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') :
Equations
• =
instance Group.fg_range {G : Type u_3} [] {G' : Type u_5} [Group G'] [] (f : G →* G') :
Group.FG f.range
Equations
• =
instance AddGroup.closure_finset_fg {G : Type u_3} [] (s : ) :
Equations
• =
instance Group.closure_finset_fg {G : Type u_3} [] (s : ) :
Group.FG ()
Equations
• =
instance AddGroup.closure_finite_fg {G : Type u_3} [] (s : Set G) [Finite s] :
Equations
• =
instance Group.closure_finite_fg {G : Type u_3} [] (s : Set G) [Finite s] :
Equations
• =
theorem AddGroup.rank.proof_1 (G : Type u_1) [] [h : ] :
∃ (n : ) (S : ), S.card = n
noncomputable def AddGroup.rank (G : Type u_3) [] [h : ] :

The minimum number of generators of an additive group

Equations
Instances For
noncomputable def Group.rank (G : Type u_3) [] [h : ] :

The minimum number of generators of a group.

Equations
Instances For
theorem AddGroup.rank_spec (G : Type u_3) [] [h : ] :
∃ (S : ), S.card =
theorem Group.rank_spec (G : Type u_3) [] [h : ] :
∃ (S : ), S.card =
theorem AddGroup.rank_le (G : Type u_3) [] [h : ] {S : } (hS : ) :
S.card
theorem Group.rank_le (G : Type u_3) [] [h : ] {S : } (hS : ) :
S.card
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 f.range
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 : } [] [] (h : H = K) :
theorem Subgroup.rank_congr {G : Type u_3} [] {H : } {K : } [Group.FG H] [Group.FG K] (h : H = K) :
=
theorem AddSubgroup.rank_closure_finset_le_card {G : Type u_3} [] (s : ) :
s.card
theorem Subgroup.rank_closure_finset_le_card {G : Type u_3} [] (s : ) :
s.card
theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_3} [] (s : Set G) [Finite s] :
instance QuotientAddGroup.fg {G : Type u_3} [] [] (N : ) [N.Normal] :
Equations
• =
instance QuotientGroup.fg {G : Type u_3} [] [] (N : ) [N.Normal] :
Equations
• =