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 #

Monoids and submonoids #

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

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

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

An additive submonoid of N 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), closure S = P S.Finite

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

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

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

theorem Submonoid.FG.exists_minimal_closure_eq {M : Type u_1} [Monoid M] {P : Submonoid M} (hP : P.FG) :
∃ (S : Finset M), Minimal (fun (x : Finset M) => closure x = P) S

A finitely generated submonoid has a minimal generating set.

theorem AddSubmonoid.FG.exists_minimal_closure_eq {M : Type u_1} [AddMonoid M] {P : AddSubmonoid M} (hP : P.FG) :
∃ (S : Finset M), Minimal (fun (x : Finset M) => closure x = P) S

A finitely generated submonoid has a minimal generating set.

theorem Submonoid.FG.prod {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {P : Submonoid M} {Q : Submonoid N} (hP : P.FG) (hQ : Q.FG) :
(P.prod Q).FG

The product of finitely generated submonoids is finitely generated.

theorem AddSubmonoid.FG.sum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] {P : AddSubmonoid M} {Q : AddSubmonoid N} (hP : P.FG) (hQ : Q.FG) :
(P.prod Q).FG

The product of finitely generated submonoids is finitely generated.

class AddMonoid.FG (M : Type u_3) [AddMonoid M] :

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

Instances
theorem AddMonoid.fG_iff (M : Type u_3) [AddMonoid M] :
class Monoid.FG (M : Type u_1) [Monoid M] :

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

Instances
theorem Monoid.fg_def {M : Type u_1} [Monoid M] :
theorem AddMonoid.fg_def {M : Type u_1} [AddMonoid M] :
theorem Monoid.fg_iff {M : Type u_1} [Monoid M] :
FG M ∃ (S : Set M), Submonoid.closure S = S.Finite

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

theorem AddMonoid.fg_iff {M : Type u_1} [AddMonoid M] :

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

theorem Submonoid.exists_minimal_closure_eq_top (M : Type u_1) [Monoid M] [Monoid.FG M] :
∃ (S : Finset M), Minimal (fun (x : Finset M) => closure x = ) S

A finitely generated monoid has a minimal generating set.

theorem AddSubmonoid.exists_minimal_closure_eq_top (M : Type u_1) [AddMonoid M] [AddMonoid.FG M] :
∃ (S : Finset M), Minimal (fun (x : Finset M) => closure x = ) S

A finitely generated monoid has a minimal generating set.

@[instance 100]
instance Monoid.fg_of_finite {M : Type u_1} [Monoid M] [Finite M] :
FG M
@[instance 100]
instance AddMonoid.fg_of_finite {M : Type u_1} [AddMonoid M] [Finite M] :
FG M
theorem Submonoid.FG.map {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') :
theorem AddSubmonoid.FG.map {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (h : P.FG) (e : M →+ M') :
theorem Submonoid.FG.map_injective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (e : M →* M') (he : Function.Injective e) (h : (Submonoid.map e P).FG) :
P.FG
theorem AddSubmonoid.FG.map_injective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (e : M →+ M') (he : Function.Injective e) (h : (AddSubmonoid.map e P).FG) :
P.FG
@[simp]
theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [Monoid M] (N : Submonoid M) :
FG N N.FG
@[simp]
theorem AddMonoid.fg_iff_addSubmonoid_fg {M : Type u_1} [AddMonoid M] (N : AddSubmonoid M) :
FG N N.FG
theorem Monoid.fg_of_surjective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [FG M] (f : M →* M') (hf : Function.Surjective f) :
FG M'
theorem AddMonoid.fg_of_surjective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [FG M] (f : M →+ M') (hf : Function.Surjective f) :
FG M'
instance Monoid.fg_range {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [FG M] (f : M →* M') :
instance AddMonoid.fg_range {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [FG M] (f : M →+ M') :
theorem Submonoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :
theorem AddSubmonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) :
instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :
instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) :
instance Monoid.closure_finite_fg {M : Type u_1} [Monoid M] (s : Set M) [Finite s] :
instance AddMonoid.closure_finite_fg {M : Type u_1} [AddMonoid M] (s : Set M) [Finite s] :

Groups and subgroups #

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

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

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

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

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

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

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

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

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

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) :
class AddGroup.FG (H : Type u_4) [AddGroup H] :

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

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

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

theorem AddGroup.fg_iff {G : Type u_3} [AddGroup G] :

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

theorem Group.fg_iff' {G : Type u_3} [Group G] :
FG G ∃ (n : ) (S : Finset G), S.card = n Subgroup.closure S =
theorem AddGroup.fg_iff' {G : Type u_3} [AddGroup G] :
FG G ∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S =
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.

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

@[simp]
theorem Group.fg_iff_subgroup_fg {G : Type u_3} [Group G] (H : Subgroup G) :
FG H H.FG
@[simp]
theorem AddGroup.fg_iff_addSubgroup_fg {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :
FG H H.FG
@[instance 100]
instance Group.fg_of_finite {G : Type u_3} [Group G] [Finite G] :
FG G
@[instance 100]
instance AddGroup.fg_of_finite {G : Type u_3} [AddGroup G] [Finite G] :
FG G
theorem Group.fg_of_surjective {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [hG : FG G] {f : G →* G'} (hf : Function.Surjective f) :
FG G'
theorem AddGroup.fg_of_surjective {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [hG : FG G] {f : G →+ G'} (hf : Function.Surjective f) :
FG G'
instance Group.fg_range {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [FG G] (f : G →* G') :
FG f.range
instance AddGroup.fg_range {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [FG G] (f : G →+ G') :
FG f.range
instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) :
instance Group.closure_finite_fg {G : Type u_3} [Group G] (s : Set G) [Finite s] :
instance AddGroup.closure_finite_fg {G : Type u_3} [AddGroup G] (s : Set G) [Finite s] :
instance QuotientGroup.fg {G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [N.Normal] :
instance QuotientAddGroup.fg {G : Type u_3} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [N.Normal] :
instance Prod.instMonoidFG {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [Monoid.FG M] [Monoid.FG N] :

The product of finitely generated monoids is finitely generated.

instance Prod.instAddMonoidFG {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] [AddMonoid.FG M] [AddMonoid.FG N] :

The product of finitely generated monoids is finitely generated.