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 submonoidS
is finitely generated.Monoid.FG M
,AddMonoid.FG M
: A typeclass indicating a typeM
is finitely generated as a monoid.Subgroup.FG S
,AddSubgroup.FG S
: A subgroupS
is finitely generated.Group.FG M
,AddGroup.FG M
: A typeclass indicating a typeM
is finitely generated as a group.
Monoids and submonoids #
An additive submonoid of N
is finitely generated if it is the closure of a finite subset of
M
.
Equations
- P.FG = ∃ (S : Finset M), AddSubmonoid.closure ↑S = P
An equivalent expression of Submonoid.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddSubmonoid.FG
in terms of Set.Finite
instead of
Finset
.
The product of finitely generated submonoids is finitely generated.
An additive monoid is finitely generated if it is finitely generated as an additive submonoid of itself.
A monoid is finitely generated if it is finitely generated as a submonoid of itself.
An equivalent expression of Monoid.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddMonoid.FG
in terms of Set.Finite
instead of Finset
.
Groups and subgroups #
An additive subgroup of H
is finitely generated if it is the closure of a finite subset of
H
.
Equations
- P.FG = ∃ (S : Finset G), AddSubgroup.closure ↑S = P
An equivalent expression of Subgroup.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddSubgroup.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.
A group is finitely generated if it is finitely generated as a subgroup of itself.
An additive group is finitely generated if it is finitely generated as an additive subgroup of itself.
An equivalent expression of Group.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddGroup.fg
in terms of Set.Finite
instead of Finset
.
An additive group is finitely generated if and only if it is finitely generated as an additive monoid.
The product of finitely generated monoids is finitely generated.