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

• IsAddFG: A type with addition is finitely generated if there is a finite subset such that every element of the type can be written as a finite sum of elements from this finite subset.
• IsMulFG: A type with multiplication is finitely generated if there is a finite subset such that every element of the type can be written as a finite product of elements from this finite subset.
• 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.

TODO

The declarations Group.FG, Subgroup.FG, Monoid.FG and Submonoid.FG are all special cases of the newly added IsMulFG. The plan is to deprecate all four of these definitions in favor of the more general IsMulFG.

Previously the subobject predicates Submonoid.FG and Subgroup.FG were used to define the more general Monoid.FG and Group.FG, but the new IsMulFG defines the general predicate directly.

class IsAddFG (M : Type u_1) [Add M] : Prop

A type with addition is finitely generated if there is a finite subset such that every element of the type can be written as a finite sum of elements from this finite subset.

This generalizes and will eventually replace the four existing definitions AddSubmonoid.FG, AddMonoid.FG, AddSubgroup.FG, and AddGroup.FG.

• out : ∃ (S : Finset M), AddSubsemigroup.closure ↑S = ⊤

class IsMulFG (M : Type u_3) [Mul M] : Prop

A type with multiplication is finitely generated if there is a finite subset such that every element of the type can be written as a finite product of elements from this finite subset.

This generalizes and will eventually replace the four existing definitions Submonoid.FG, Monoid.FG, Subgroup.FG, and Group.FG.

• out : ∃ (S : Finset M), Subsemigroup.closure ↑S = ⊤

@[instance 100]

instance instIsMulFGOfFinite {M : Type u_1} [Mul M] [Finite M] : IsMulFG M

@[instance 100]

instance instIsAddFGOfFinite {M : Type u_1} [Add M] [Finite M] : IsAddFG M

theorem IsMulFG.of_surjective {M : Type u_1} {M' : Type u_2} [Mul M] [Mul M'] {F : Type u_3} [FunLike F M M'] [MulHomClass F M M'] (f : F) (hf : Function.Surjective ⇑f) [IsMulFG M] : IsMulFG M'

theorem IsAddFG.of_surjective {M : Type u_1} {M' : Type u_2} [Add M] [Add M'] {F : Type u_3} [FunLike F M M'] [AddHomClass F M M'] (f : F) (hf : Function.Surjective ⇑f) [IsAddFG M] : IsAddFG M'

theorem isMulFG_congr {M : Type u_1} {M' : Type u_2} [Mul M] [Mul M'] {F : Type u_3} [EquivLike F M M'] [MulEquivClass F M M'] (f : F) : IsMulFG M ↔ IsMulFG M'

theorem isAddFG_congr {M : Type u_1} {M' : Type u_2} [Add M] [Add M'] {F : Type u_3} [EquivLike F M M'] [AddEquivClass F M M'] (f : F) : IsAddFG M ↔ IsAddFG M'

@[simp]

theorem isMulFG_multiplicative_iff {M : Type u_3} [Add M] : IsMulFG (Multiplicative M) ↔ IsAddFG M

@[simp]

theorem isAddFG_additive_iff {M : Type u_1} [Mul M] : IsAddFG (Additive M) ↔ IsMulFG M

instance instIsAddFGAdditiveOfIsMulFG {M : Type u_1} [Mul M] [IsMulFG M] : IsAddFG (Additive M)

instance instIsMulFGMultiplicativeOfIsAddFG {M : Type u_3} [Add M] [IsAddFG M] : IsMulFG (Multiplicative M)

theorem Semigroup.isMulFG_iff {M : Type u_1} [Mul M] : IsMulFG M ↔ ∃ (S : Finset M), Subsemigroup.closure ↑S = ⊤

theorem AddSemigroup.isAddFG_iff {M : Type u_1} [Add M] : IsAddFG M ↔ ∃ (S : Finset M), AddSubsemigroup.closure ↑S = ⊤

theorem Semigroup.exists_of_isMulFG (M : Type u_1) [Mul M] [IsMulFG M] : ∃ (S : Finset M), Subsemigroup.closure ↑S = ⊤

theorem AddSemigroup.exists_of_isAddFG (M : Type u_1) [Add M] [IsAddFG M] : ∃ (S : Finset M), AddSubsemigroup.closure ↑S = ⊤

theorem Semigroup.isMulFG_iff_finite {M : Type u_1} [Mul M] : IsMulFG M ↔ ∃ (S : Set M), S.Finite ∧ Subsemigroup.closure S = ⊤

theorem AddSemigroup.isAddFG_iff_finite {M : Type u_1} [Add M] : IsAddFG M ↔ ∃ (S : Set M), S.Finite ∧ AddSubsemigroup.closure S = ⊤

theorem Semigroup.exists_finite_of_isMulFG (M : Type u_1) [Mul M] [IsMulFG M] : ∃ (S : Set M), S.Finite ∧ Subsemigroup.closure S = ⊤

theorem AddSemigroup.exists_finite_of_isAddFG (M : Type u_1) [Add M] [IsAddFG M] : ∃ (S : Set M), S.Finite ∧ AddSubsemigroup.closure S = ⊤

theorem Monoid.isMulFG_iff {M : Type u_1} [MulOneClass M] : IsMulFG M ↔ ∃ (S : Finset M), Submonoid.closure ↑S = ⊤

theorem AddMonoid.isAddFG_iff {M : Type u_1} [AddZeroClass M] : IsAddFG M ↔ ∃ (S : Finset M), AddSubmonoid.closure ↑S = ⊤

theorem Monoid.exists_of_isMulFG (M : Type u_1) [MulOneClass M] [IsMulFG M] : ∃ (S : Finset M), Submonoid.closure ↑S = ⊤

theorem AddMonoid.exists_of_isAddFG (M : Type u_1) [AddZeroClass M] [IsAddFG M] : ∃ (S : Finset M), AddSubmonoid.closure ↑S = ⊤

theorem Monoid.isMulFG_iff_finite {M : Type u_1} [MulOneClass M] : IsMulFG M ↔ ∃ (S : Set M), S.Finite ∧ Submonoid.closure S = ⊤

theorem AddMonoid.isAddFG_iff_finite {M : Type u_1} [AddZeroClass M] : IsAddFG M ↔ ∃ (S : Set M), S.Finite ∧ AddSubmonoid.closure S = ⊤

theorem Monoid.exists_finite_of_isMulFG (M : Type u_1) [MulOneClass M] [IsMulFG M] : ∃ (S : Set M), S.Finite ∧ Submonoid.closure S = ⊤

theorem AddMonoid.exists_finite_of_isAddFG (M : Type u_1) [AddZeroClass M] [IsAddFG M] : ∃ (S : Set M), S.Finite ∧ AddSubmonoid.closure S = ⊤

instance Monoid.instIsMulFGSubtypeMemSubmonoidMrangeMonoidHom {M : Type u_1} {M' : Type u_2} [MulOneClass M] [MulOneClass M'] (f : M →* M') [IsMulFG M] : IsMulFG ↥(MonoidHom.mrange f)

instance AddMonoid.instIsAddFGSubtypeMemAddSubmonoidMrangeAddMonoidHom {M : Type u_1} {M' : Type u_2} [AddZeroClass M] [AddZeroClass M'] (f : M →+ M') [IsAddFG M] : IsAddFG ↥(AddMonoidHom.mrange f)

instance Monoid.instIsMulFGProd {M : Type u_1} {M' : Type u_2} [MulOneClass M] [MulOneClass M'] [IsMulFG M] [IsMulFG M'] : IsMulFG (M × M')

instance AddMonoid.instIsAddFGProd {M : Type u_1} {M' : Type u_2} [AddZeroClass M] [AddZeroClass M'] [IsAddFG M] [IsAddFG M'] : IsAddFG (M × M')

theorem Submonoid.iSup_map_mulSingle {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)} [DecidableEq ι] : ⨆ (i : ι), map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

theorem AddSubmonoid.iSup_map_single {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)} [DecidableEq ι] : ⨆ (i : ι), map (AddMonoidHom.single M i) (P i) = pi Set.univ P

instance Monoid.instIsMulFGForall {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → Monoid (M i)] [h : ∀ (i : ι), IsMulFG (M i)] : IsMulFG ((i : ι) → M i)

instance AddMonoid.instIsAddFGForall {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → AddMonoid (M i)] [h : ∀ (i : ι), IsAddFG (M i)] : IsAddFG ((i : ι) → M i)

theorem Group.isMulFG_iff {G : Type u_1} [Group G] : IsMulFG G ↔ ∃ (S : Finset G), Subgroup.closure ↑S = ⊤

theorem AddGroup.isAddFG_iff {G : Type u_1} [AddGroup G] : IsAddFG G ↔ ∃ (S : Finset G), AddSubgroup.closure ↑S = ⊤

theorem Group.exists_of_isMulFG (G : Type u_1) [Group G] [IsMulFG G] : ∃ (S : Finset G), Subgroup.closure ↑S = ⊤

theorem AddGroup.exists_of_isAddFG (G : Type u_1) [AddGroup G] [IsAddFG G] : ∃ (S : Finset G), AddSubgroup.closure ↑S = ⊤

theorem Group.isMulFG_iff_finite {G : Type u_1} [Group G] : IsMulFG G ↔ ∃ (S : Set G), S.Finite ∧ Subgroup.closure S = ⊤

theorem AddGroup.isAddFG_iff_finite {G : Type u_1} [AddGroup G] : IsAddFG G ↔ ∃ (S : Set G), S.Finite ∧ AddSubgroup.closure S = ⊤

theorem Group.exists_finite_of_isMulFG (G : Type u_1) [Group G] [IsMulFG G] : ∃ (S : Set G), S.Finite ∧ Subgroup.closure S = ⊤

theorem AddGroup.exists_finite_of_isAddFG (G : Type u_1) [AddGroup G] [IsAddFG G] : ∃ (S : Set G), S.Finite ∧ AddSubgroup.closure S = ⊤

instance Group.instIsMulFGSubtypeMemSubgroupRange {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') [IsMulFG G] : IsMulFG ↥f.range

instance AddGroup.instIsAddFGSubtypeMemAddSubgroupRange {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') [IsAddFG G] : IsAddFG ↥f.range

theorem Subsemigroup.isMulFG_iff {M : Type u_1} [Mul M] {P : Subsemigroup M} : IsMulFG ↥P ↔ ∃ (S : Finset M), closure ↑S = P

theorem AddSubsemigroup.isAddFG_iff {M : Type u_1} [Add M] {P : AddSubsemigroup M} : IsAddFG ↥P ↔ ∃ (S : Finset M), closure ↑S = P

theorem Subsemigroup.exists_of_isMulFG {M : Type u_1} [Mul M] (P : Subsemigroup M) [IsMulFG ↥P] : ∃ (S : Finset M), closure ↑S = P

theorem AddSubsemigroup.exists_of_isAddFG {M : Type u_1} [Add M] (P : AddSubsemigroup M) [IsAddFG ↥P] : ∃ (S : Finset M), closure ↑S = P

theorem Subsemigroup.isMulFG_iff_finite {M : Type u_1} [Mul M] {P : Subsemigroup M} : IsMulFG ↥P ↔ ∃ (S : Set M), S.Finite ∧ closure S = P

theorem AddSubsemigroup.isAddFG_iff_finite {M : Type u_1} [Add M] {P : AddSubsemigroup M} : IsAddFG ↥P ↔ ∃ (S : Set M), S.Finite ∧ closure S = P

theorem Subsemigroup.exists_finite_of_isMulFG {M : Type u_1} [Mul M] (P : Subsemigroup M) [IsMulFG ↥P] : ∃ (S : Set M), S.Finite ∧ closure S = P

theorem AddSubsemigroup.exists_finite_of_isAddFG {M : Type u_1} [Add M] (P : AddSubsemigroup M) [IsAddFG ↥P] : ∃ (S : Set M), S.Finite ∧ closure S = P

@[simp]

theorem Subsemigroup.isMulFG_top_iff {M : Type u_1} [Mul M] : IsMulFG ↥⊤ ↔ IsMulFG M

@[simp]

theorem AddSubsemigroup.isAddFG_top_iff {M : Type u_1} [Add M] : IsAddFG ↥⊤ ↔ IsAddFG M

instance Subsemigroup.instIsMulFGSubtypeMemTop {M : Type u_1} [Mul M] [IsMulFG M] : IsMulFG ↥⊤

instance AddSubsemigroup.instIsAddFGSubtypeMemTop {M : Type u_1} [Add M] [IsAddFG M] : IsAddFG ↥⊤

instance Subsemigroup.instIsMulFGSubtypeMemMap {M : Type u_1} {M' : Type u_2} [Mul M] [Mul M'] {P : Subsemigroup M} (f : M →ₙ* M') [IsMulFG ↥P] : IsMulFG ↥(map f P)

instance AddSubsemigroup.instIsAddFGSubtypeMemMap {M : Type u_1} {M' : Type u_2} [Add M] [Add M'] {P : AddSubsemigroup M} (f : M →ₙ+ M') [IsAddFG ↥P] : IsAddFG ↥(map f P)

theorem Submonoid.isMulFG_iff {M : Type u_1} [MulOneClass M] {P : Submonoid M} : IsMulFG ↥P ↔ ∃ (S : Finset M), closure ↑S = P

theorem AddSubmonoid.isAddFG_iff {M : Type u_1} [AddZeroClass M] {P : AddSubmonoid M} : IsAddFG ↥P ↔ ∃ (S : Finset M), closure ↑S = P

theorem Submonoid.exists_of_isMulFG {M : Type u_1} [MulOneClass M] (P : Submonoid M) [IsMulFG ↥P] : ∃ (S : Finset M), closure ↑S = P

theorem AddSubmonoid.exists_of_isAddFG {M : Type u_1} [AddZeroClass M] (P : AddSubmonoid M) [IsAddFG ↥P] : ∃ (S : Finset M), closure ↑S = P

theorem Submonoid.isMulFG_iff_finite {M : Type u_1} [MulOneClass M] {P : Submonoid M} : IsMulFG ↥P ↔ ∃ (S : Set M), S.Finite ∧ closure S = P

theorem AddSubmonoid.isAddFG_iff_finite {M : Type u_1} [AddZeroClass M] {P : AddSubmonoid M} : IsAddFG ↥P ↔ ∃ (S : Set M), S.Finite ∧ closure S = P

theorem Submonoid.exists_finite_of_isMulFG {M : Type u_1} [MulOneClass M] (P : Submonoid M) [IsMulFG ↥P] : ∃ (S : Set M), S.Finite ∧ closure S = P

theorem AddSubmonoid.exists_finite_of_isAddFG {M : Type u_1} [AddZeroClass M] (P : AddSubmonoid M) [IsAddFG ↥P] : ∃ (S : Set M), S.Finite ∧ closure S = P

@[simp]

theorem Submonoid.isMulFG_top_iff {M : Type u_1} [MulOneClass M] : IsMulFG ↥⊤ ↔ IsMulFG M

@[simp]

theorem AddSubmonoid.isAddFG_top_iff {M : Type u_1} [AddZeroClass M] : IsAddFG ↥⊤ ↔ IsAddFG M

instance Submonoid.instIsMulFGSubtypeMemTop {M : Type u_1} [MulOneClass M] [IsMulFG M] : IsMulFG ↥⊤

instance AddSubmonoid.instIsAddFGSubtypeMemTop {M : Type u_1} [AddZeroClass M] [IsAddFG M] : IsAddFG ↥⊤

instance Submonoid.instIsMulFGSubtypeMemMapMonoidHom {M : Type u_1} {M' : Type u_2} [MulOneClass M] [MulOneClass M'] {P : Submonoid M} (f : M →* M') [IsMulFG ↥P] : IsMulFG ↥(map f P)

instance AddSubmonoid.instIsAddFGSubtypeMemMapAddMonoidHom {M : Type u_1} {M' : Type u_2} [AddZeroClass M] [AddZeroClass M'] {P : AddSubmonoid M} (f : M →+ M') [IsAddFG ↥P] : IsAddFG ↥(map f P)

instance Submonoid.instIsMulFGSubtypeProdMemProd {M : Type u_1} {M' : Type u_2} [MulOneClass M] [MulOneClass M'] {P : Submonoid M} {P' : Submonoid M'} [IsMulFG ↥P] [IsMulFG ↥P'] : IsMulFG ↥(P.prod P')

instance AddSubmonoid.instIsAddFGSubtypeSumMemSum {M : Type u_1} {M' : Type u_2} [AddZeroClass M] [AddZeroClass M'] {P : AddSubmonoid M} {P' : AddSubmonoid M'} [IsAddFG ↥P] [IsAddFG ↥P'] : IsAddFG ↥(P.prod P')

theorem Subgroup.isMulFG_iff {G : Type u_1} [Group G] {H : Subgroup G} : IsMulFG ↥H ↔ ∃ (S : Finset G), closure ↑S = H

theorem AddSubgroup.isAddFG_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : IsAddFG ↥H ↔ ∃ (S : Finset G), closure ↑S = H

theorem Subgroup.exists_of_isMulFG {G : Type u_1} [Group G] (H : Subgroup G) [IsMulFG ↥H] : ∃ (S : Finset G), closure ↑S = H

theorem AddSubgroup.exists_of_isAddFG {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddFG ↥H] : ∃ (S : Finset G), closure ↑S = H

theorem Subgroup.isMulFG_iff_finite {G : Type u_1} [Group G] {H : Subgroup G} : IsMulFG ↥H ↔ ∃ (S : Set G), S.Finite ∧ closure S = H

theorem AddSubgroup.isAddFG_iff_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : IsAddFG ↥H ↔ ∃ (S : Set G), S.Finite ∧ closure S = H

theorem Subgroup.exists_finite_of_isMulFG {G : Type u_1} [Group G] (H : Subgroup G) [IsMulFG ↥H] : ∃ (S : Set G), S.Finite ∧ closure S = H

theorem AddSubgroup.exists_finite_of_isAddFG {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddFG ↥H] : ∃ (S : Set G), S.Finite ∧ closure S = H

@[simp]

theorem Subgroup.isMulFG_top_iff {G : Type u_1} [Group G] : IsMulFG ↥⊤ ↔ IsMulFG G

@[simp]

theorem AddSubgroup.isAddFG_top_iff {G : Type u_1} [AddGroup G] : IsAddFG ↥⊤ ↔ IsAddFG G

instance Subgroup.instIsMulFGSubtypeMemTop {G : Type u_1} [Group G] [IsMulFG G] : IsMulFG ↥⊤

instance AddSubgroup.instIsAddFGSubtypeMemTop {G : Type u_1} [AddGroup G] [IsAddFG G] : IsAddFG ↥⊤

instance Subgroup.instIsMulFGSubtypeMemMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H : Subgroup G} (f : G →* G') [IsMulFG ↥H] : IsMulFG ↥(map f H)

instance AddSubgroup.instIsAddFGSubtypeMemMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {H : AddSubgroup G} (f : G →+ G') [IsAddFG ↥H] : IsAddFG ↥(map f H)

instance Subgroup.instIsMulFGSubtypeProdMemProd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H : Subgroup G} {H' : Subgroup G'} [IsMulFG ↥H] [IsMulFG ↥H'] : IsMulFG ↥(H.prod H')

instance AddSubgroup.instIsAddFGSubtypeSumMemSum {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {H : AddSubgroup G} {H' : AddSubgroup G'} [IsAddFG ↥H] [IsAddFG ↥H'] : IsAddFG ↥(H.prod H')

Monoids and submonoids

@[reducible, inline]

abbrev 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

• P.FG = IsMulFG ↥P

@[reducible, inline]

abbrev AddSubmonoid.FG {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) : Prop

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

Equations

• P.FG = IsAddFG ↥P

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 (S : Finset M) => closure ↑S = 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 (S : Finset M) => closure ↑S = P) S

A finitely generated submonoid has a minimal generating set.

theorem Submonoid.fg_iff_add_fg {M : Type u_1} [Monoid M] (P : Submonoid M) : P.FG ↔ (toAddSubmonoid P).FG

theorem AddSubmonoid.fg_iff_mul_fg {M : Type u_3} [AddMonoid M] (P : AddSubmonoid M) : P.FG ↔ (toSubmonoid P).FG

theorem Submonoid.FG.bot {M : Type u_1} [Monoid M] : ⊥.FG

theorem AddSubmonoid.FG.bot {M : Type u_1} [AddMonoid M] : ⊥.FG

theorem Submonoid.FG.sup {M : Type u_1} [Monoid M] {P Q : Submonoid M} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem AddSubmonoid.FG.sup {M : Type u_1} [AddMonoid M] {P Q : AddSubmonoid M} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem Submonoid.FG.finset_sup {M : Type u_1} [Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem AddSubmonoid.FG.finset_sup {M : Type u_1} [AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem Submonoid.FG.biSup_finset {M : Type u_1} [Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubmonoid.FG.biSup_finset {M : Type u_1} [AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Submonoid.FG.biSup {M : Type u_1} [Monoid M] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubmonoid.FG.biSup {M : Type u_1} [AddMonoid M] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Submonoid.FG.iSup {M : Type u_1} [Monoid M] {ι : Sort u_3} [Finite ι] (P : ι → Submonoid M) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem AddSubmonoid.FG.iSup {M : Type u_1} [AddMonoid M] {ι : Sort u_3} [Finite ι] (P : ι → AddSubmonoid M) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

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 two finitely generated submonoids is finitely generated.

theorem AddSubmonoid.FG.prod {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 two finitely generated additive submonoids is finitely generated.

theorem Submonoid.FG.pi {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)} (hP : ∀ (i : ι), (P i).FG) : (Submonoid.pi Set.univ P).FG

Finite product of finitely generated submonoids is finitely generated.

theorem AddSubmonoid.FG.pi {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)} (hP : ∀ (i : ι), (P i).FG) : (AddSubmonoid.pi Set.univ P).FG

Finite product of finitely generated additive submonoids is finitely generated.

@[reducible, inline]

abbrev Monoid.FG (M : Type u_1) [Monoid M] : Prop

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

Equations

• Monoid.FG M = IsMulFG M

@[reducible, inline]

abbrev AddMonoid.FG (M : Type u_1) [AddMonoid M] : Prop

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

Equations

• AddMonoid.FG M = IsAddFG M

theorem Monoid.fg_def {M : Type u_1} [Monoid M] : FG M ↔ ⊤.FG

theorem AddMonoid.fg_def {M : Type u_1} [AddMonoid M] : FG M ↔ ⊤.FG

theorem Monoid.FG.fg_top {M : Type u_1} [Monoid M] [FG M] : ⊤.FG

theorem AddMonoid.FG.fg_top {M : Type u_1} [AddMonoid M] [FG M] : ⊤.FG

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] : FG M ↔ ∃ (S : Set M), AddSubmonoid.closure S = ⊤ ∧ S.Finite

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 (S : Finset M) => closure ↑S = ⊤) 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 (S : Finset M) => closure ↑S = ⊤) S

A finitely generated monoid has a minimal generating set.

theorem Monoid.fg_iff_add_fg {M : Type u_1} [Monoid M] : FG M ↔ AddMonoid.FG (Additive M)

theorem AddMonoid.fg_iff_mul_fg {M : Type u_3} [AddMonoid M] : FG M ↔ Monoid.FG (Multiplicative M)

theorem Monoid.fg_of_finite {M : Type u_1} [Monoid M] [Finite M] : FG M

theorem 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') : (Submonoid.map e P).FG

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') : (AddSubmonoid.map e P).FG

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 instFGFreeMonoidOfFinite (α : Type u_3) [Finite α] : Monoid.FG (FreeMonoid α)

instance instFGFreeAddMonoidOfFinite (α : Type u_3) [Finite α] : AddMonoid.FG (FreeAddMonoid α)

theorem Monoid.fg_iff_exists_freeMonoid_hom_surjective {M : Type u_1} [Monoid M] : FG M ↔ ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid ↑S →* M), Function.Surjective ⇑φ

A monoid is finitely generated iff there exists a surjective homomorphism from a FreeMonoid on finitely many generators.

theorem AddMonoid.fg_iff_exists_freeAddMonoid_hom_surjective {M : Type u_1} [AddMonoid M] : FG M ↔ ∃ (S : Set M) (_ : S.Finite) (φ : FreeAddMonoid ↑S →+ M), Function.Surjective ⇑φ

An additive monoid is finitely generated iff there exists a surjective homomorphism from a FreeAddMonoid on finitely many generators.

theorem Monoid.fg_iff_exists_freeGroup_hom_surjective_finite {M : Type u_1} [Monoid M] : FG M ↔ ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M), Function.Surjective ⇑φ

A monoid if finitely generated if and only if there exists a surjective homomorphism from a FreeMonoid on an arbitrary finite type α to the monoid.

theorem AddMonoid.fg_iff_exists_freeAddGroup_hom_surjective_finite {M : Type u_1} [AddMonoid M] : FG M ↔ ∃ (α : Type) (_ : Finite α) (φ : FreeAddMonoid α →+ M), Function.Surjective ⇑φ

An additive monoid is finitely generated iff there exists a surjective homomorphism from a FreeAddMonoid on an arbitrary finite type α to the monoid.

theorem Submonoid.powers_fg {M : Type u_1} [Monoid M] (r : M) : (powers r).FG

theorem AddSubmonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) : (multiples r).FG

instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) : FG ↥(Submonoid.powers r)

instance AddMonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) : FG ↥(AddSubmonoid.multiples r)

instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) : FG ↥(Submonoid.closure ↑s)

instance AddMonoid.closure_finset_fg {M : Type u_1} [AddMonoid M] (s : Finset M) : FG ↥(AddSubmonoid.closure ↑s)

instance Monoid.closure_finite_fg {M : Type u_1} [Monoid M] (s : Set M) [Finite ↑s] : FG ↥(Submonoid.closure s)

instance AddMonoid.closure_finite_fg {M : Type u_1} [AddMonoid M] (s : Set M) [Finite ↑s] : FG ↥(AddSubmonoid.closure s)

Groups and subgroups

@[reducible, inline]

abbrev 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

• P.FG = IsMulFG ↥P

@[reducible, inline]

abbrev AddSubgroup.FG {G : Type u_3} [AddGroup G] (P : AddSubgroup G) : Prop

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

Equations

• P.FG = IsAddFG ↥P

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.

theorem AddSubgroup.fg_iff_addSubmonoid_fg {G : Type u_3} [AddGroup G] (P : AddSubgroup G) : 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_add_fg {G : Type u_3} [Group G] (P : Subgroup G) : P.FG ↔ (toAddSubgroup P).FG

theorem AddSubgroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] (P : AddSubgroup H) : P.FG ↔ (toSubgroup P).FG

theorem Subgroup.FG.bot {G : Type u_3} [Group G] : ⊥.FG

theorem AddSubgroup.FG.bot {G : Type u_3} [AddGroup G] : ⊥.FG

theorem Subgroup.FG.sup {G : Type u_3} [Group G] {P Q : Subgroup G} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem AddSubgroup.FG.sup {G : Type u_3} [AddGroup G] {P Q : AddSubgroup G} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem Subgroup.FG.finset_sup {G : Type u_3} [Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem AddSubgroup.FG.finset_sup {G : Type u_3} [AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem Subgroup.FG.biSup_finset {G : Type u_3} [Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubgroup.FG.biSup_finset {G : Type u_3} [AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Subgroup.FG.biSup {G : Type u_3} [Group G] {ι : Type u_5} {s : Set ι} (hs : s.Finite) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubgroup.FG.biSup {G : Type u_3} [AddGroup G] {ι : Type u_5} {s : Set ι} (hs : s.Finite) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Subgroup.FG.iSup {G : Type u_3} [Group G] {ι : Sort u_5} [Finite ι] (P : ι → Subgroup G) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem AddSubgroup.FG.iSup {G : Type u_3} [AddGroup G] {ι : Sort u_5} [Finite ι] (P : ι → AddSubgroup G) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem Subgroup.FG.prod {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] {P : Subgroup G} {Q : Subgroup G'} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated subgroups is finitely generated.

theorem AddSubgroup.FG.prod {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] {P : AddSubgroup G} {Q : AddSubgroup G'} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated additive subgroups is finitely generated.

theorem Subgroup.FG.pi {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → Group (G i)] {P : (i : ι) → Subgroup (G i)} (hP : ∀ (i : ι), (P i).FG) : (Subgroup.pi Set.univ P).FG

Finite product of finitely generated subgroups is finitely generated.

theorem AddSubgroup.FG.pi {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → AddGroup (G i)] {P : (i : ι) → AddSubgroup (G i)} (hP : ∀ (i : ι), (P i).FG) : (AddSubgroup.pi Set.univ P).FG

Finite product of finitely generated additive subgroups is finitely generated.

@[reducible, inline]

abbrev Group.FG (G : Type u_3) [Group G] : Prop

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

Equations

• Group.FG G = IsMulFG G

@[reducible, inline]

abbrev AddGroup.FG (G : Type u_3) [AddGroup G] : Prop

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

Equations

• AddGroup.FG G = IsAddFG G

theorem Group.fg_def {G : Type u_3} [Group G] : FG G ↔ ⊤.FG

theorem AddGroup.fg_def {G : Type u_3} [AddGroup G] : FG G ↔ ⊤.FG

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] : FG G ↔ ∃ (S : Set G), AddSubgroup.closure S = ⊤ ∧ S.Finite

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] : FG G ↔ Monoid.FG G

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

theorem AddGroup.fg_iff_addMonoid_fg {G : Type u_3} [AddGroup G] : FG G ↔ AddMonoid.FG G

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

theorem GroupFG.iff_add_fg {G : Type u_3} [Group G] : Group.FG G ↔ AddGroup.FG (Additive G)

theorem AddGroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] : FG H ↔ Group.FG (Multiplicative H)

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 instFGFreeGroupOfFinite (α : Type u_5) [Finite α] : Group.FG (FreeGroup α)

instance instFGFreeAddGroupOfFinite (α : Type u_5) [Finite α] : AddGroup.FG (FreeAddGroup α)

theorem Group.fg_iff_exists_freeGroup_hom_surjective {G : Type u_3} [Group G] : FG G ↔ ∃ (S : Set G) (_ : S.Finite) (φ : FreeGroup ↑S →* G), Function.Surjective ⇑φ

A group is finitely generated iff there exists a surjective homomorphism from a FreeGroup on finitely many generators.

theorem AddGroup.fg_iff_exists_freeAddGroup_hom_surjective {G : Type u_3} [AddGroup G] : FG G ↔ ∃ (S : Set G) (_ : S.Finite) (φ : FreeAddGroup ↑S →+ G), Function.Surjective ⇑φ

An additive group is finitely generated iff there exists a surjective homomorphism from a FreeAddGroup on finitely many generators.

theorem Group.fg_iff_exists_freeGroup_hom_surjective_finite {G : Type u_3} [Group G] : FG G ↔ ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G), Function.Surjective ⇑φ

A group if finitely generated if and only if there exists a surjective homomorphism from a FreeGroup on an arbitrary finite type α to the group.

theorem AddGroup.fg_iff_exists_freeAddGroup_hom_surjective_finite {G : Type u_3} [AddGroup G] : FG G ↔ ∃ (α : Type) (_ : Finite α) (φ : FreeAddGroup α →+ G), Function.Surjective ⇑φ

An additive group is finitely generated iff there exists a surjective homomorphism from a FreeAddGroup on an arbitrary finite type α to the group.

instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) : FG ↥(Subgroup.closure ↑s)

instance AddGroup.closure_finset_fg {G : Type u_3} [AddGroup G] (s : Finset G) : FG ↥(AddSubgroup.closure ↑s)

instance Group.closure_finite_fg {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] : FG ↥(Subgroup.closure s)

instance AddGroup.closure_finite_fg {G : Type u_3} [AddGroup G] (s : Set G) [Finite ↑s] : FG ↥(AddSubgroup.closure s)

instance QuotientGroup.fg {G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [N.Normal] : Group.FG (G ⧸ N)

instance QuotientAddGroup.fg {G : Type u_3} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [N.Normal] : AddGroup.FG (G ⧸ N)

instance AddMonoid.instFGNat : FG ℕ

instance AddGroup.instFGInt : FG ℤ

theorem Submonoid.fg_of_divisive {M : Type u_5} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] {P : Submonoid M} (hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P) : P.FG

In a canonically ordered and well-quasi-ordered monoid, any divisive submonoid is finitely generated.

theorem AddSubmonoid.fg_of_subtractive {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] {P : AddSubmonoid M} (hP : ∀ x ∈ P, ∀ (y : M), x + y ∈ P → y ∈ P) : P.FG

In a canonically ordered and well-quasi-ordered additive monoid (typical example is ℕ ^ k), any subtractive submonoid is finitely generated.

theorem CommMonoid.fg_of_wellQuasiOrderedLE {M : Type u_5} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] : Monoid.FG M

A canonically ordered and well-quasi-ordered monoid must be finitely generated.

theorem AddCommMonoid.fg_of_wellQuasiOrderedLE {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] : AddMonoid.FG M

A canonically ordered and well-quasi-ordered additive monoid must be finitely generated.

theorem Submonoid.fg_eqLocusM {M : Type u_5} {N : Type u_6} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] [Monoid N] [IsCancelMul N] (f g : M →* N) : (f.eqLocusM g).FG

If f g are homomorphisms from a canonically ordered and well-quasi-ordered monoid M to a cancellative monoid N, the submonoid of M on which f and g agree is finitely generated.

theorem AddSubmonoid.fg_eqLocusM {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] [AddMonoid N] [IsCancelAdd N] (f g : M →+ N) : (f.eqLocusM g).FG

If f g are homomorphisms from a canonically ordered and well-quasi-ordered additive monoid M to a cancellative additive monoid N, the submonoid of M on which f and g agree is finitely generated. When M and N are ℕ ^ k, this is also known as a version of Gordan's lemma.