mathlib documentation

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

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), submonoid.closure S = P 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), add_submonoid.closure S = P S.finite

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

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

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

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] :
@[instance]
@[instance]

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.

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), subgroup.closure S = P 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), add_subgroup.closure S = P 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) :
@[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
@[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
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] :

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

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

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.

theorem group_fg.iff_add_fg {G : Type u_3} [group G] :
@[instance]
def add_group.fg_of_group_fg {G : Type u_3} [group G] [group.fg G] :
@[instance]