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 submonoidSis finitely generated.Monoid.FG M,AddMonoid.FG M: A typeclass indicating a typeMis finitely generated as a monoid.Subgroup.FG S,AddSubgroup.FG S: A subgroupSis finitely generated.Group.FG M,AddGroup.FG M: A typeclass indicating a typeMis 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
- AddSubmonoid.FG P = ∃ (S : Finset M), AddSubmonoid.closure ↑S = P
A submonoid of M is finitely generated if it is the closure of a finite subset of M.
Equations
- Submonoid.FG P = ∃ (S : Finset M), Submonoid.closure ↑S = P
abbrev
AddSubmonoid.fg_iff.match_1
{M : Type u_1}
[AddMonoid M]
(P : AddSubmonoid M)
(motive : AddSubmonoid.FG P → Prop)
:
∀ (x : AddSubmonoid.FG P), (∀ (S : Finset M) (hS : AddSubmonoid.closure ↑S = P), motive ⋯) → motive x
Equations
- ⋯ = ⋯
abbrev
AddSubmonoid.fg_iff.match_2
{M : Type u_1}
[AddMonoid M]
(P : AddSubmonoid M)
(motive : (∃ (S : Set M), AddSubmonoid.closure S = P ∧ Set.Finite S) → Prop)
:
∀ (x : ∃ (S : Set M), AddSubmonoid.closure S = P ∧ Set.Finite S),
(∀ (S : Set M) (hS : AddSubmonoid.closure S = P) (hf : Set.Finite S), motive ⋯) → motive x
Equations
- ⋯ = ⋯
theorem
AddSubmonoid.fg_iff
{M : Type u_1}
[AddMonoid M]
(P : AddSubmonoid M)
:
AddSubmonoid.FG P ↔ ∃ (S : Set M), AddSubmonoid.closure S = P ∧ Set.Finite S
An equivalent expression of AddSubmonoid.FG in terms of Set.Finite instead of
Finset.
theorem
Submonoid.fg_iff
{M : Type u_1}
[Monoid M]
(P : Submonoid M)
:
Submonoid.FG P ↔ ∃ (S : Set M), Submonoid.closure S = P ∧ Set.Finite S
An equivalent expression of Submonoid.FG in terms of Set.Finite instead of Finset.
theorem
Submonoid.fg_iff_add_fg
{M : Type u_1}
[Monoid M]
(P : Submonoid M)
:
Submonoid.FG P ↔ AddSubmonoid.FG (Submonoid.toAddSubmonoid P)
theorem
AddSubmonoid.fg_iff_mul_fg
{N : Type u_2}
[AddMonoid N]
(P : AddSubmonoid N)
:
AddSubmonoid.FG P ↔ Submonoid.FG (AddSubmonoid.toSubmonoid P)
A monoid is finitely generated if it is finitely generated as a submonoid of itself.
- out : Submonoid.FG ⊤
Instances
- Monoid.closure_finite_fg
- Monoid.closure_finset_fg
- Monoid.fg_of_addMonoid_fg
- Monoid.fg_of_finite
- Monoid.fg_range
- Monoid.powers_fg
- NumberField.Units.instFGUnitsSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringInstMonoid
An additive monoid is finitely generated if it is finitely generated as an additive submonoid of itself.
- out : AddSubmonoid.FG ⊤
theorem
AddMonoid.fg_iff
{M : Type u_1}
[AddMonoid M]
:
AddMonoid.FG M ↔ ∃ (S : Set M), AddSubmonoid.closure S = ⊤ ∧ Set.Finite S
An equivalent expression of AddMonoid.FG in terms of Set.Finite instead of Finset.
theorem
Monoid.fg_iff
{M : Type u_1}
[Monoid M]
:
Monoid.FG M ↔ ∃ (S : Set M), Submonoid.closure S = ⊤ ∧ Set.Finite S
An equivalent expression of Monoid.FG in terms of Set.Finite instead of Finset.
theorem
AddMonoid.fg_iff_mul_fg
{N : Type u_2}
[AddMonoid N]
:
AddMonoid.FG N ↔ Monoid.FG (Multiplicative N)
instance
AddMonoid.fg_of_monoid_fg
{M : Type u_1}
[Monoid M]
[Monoid.FG M]
:
AddMonoid.FG (Additive M)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
AddSubmonoid.FG.map
{M : Type u_1}
[AddMonoid M]
{M' : Type u_3}
[AddMonoid M']
{P : AddSubmonoid M}
(h : AddSubmonoid.FG P)
(e : M →+ M')
:
theorem
Submonoid.FG.map
{M : Type u_1}
[Monoid M]
{M' : Type u_3}
[Monoid M']
{P : Submonoid M}
(h : Submonoid.FG P)
(e : M →* M')
:
Submonoid.FG (Submonoid.map e P)
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.FG (AddSubmonoid.map e P))
:
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.FG (Submonoid.map e P))
:
@[simp]
theorem
AddMonoid.fg_iff_addSubmonoid_fg
{M : Type u_1}
[AddMonoid M]
(N : AddSubmonoid M)
:
AddMonoid.FG ↥N ↔ AddSubmonoid.FG N
@[simp]
theorem
Monoid.fg_iff_submonoid_fg
{M : Type u_1}
[Monoid M]
(N : Submonoid M)
:
Monoid.FG ↥N ↔ Submonoid.FG N
theorem
AddMonoid.fg_of_surjective
{M : Type u_1}
[AddMonoid M]
{M' : Type u_3}
[AddMonoid M']
[AddMonoid.FG M]
(f : M →+ M')
(hf : Function.Surjective ⇑f)
:
AddMonoid.FG M'
theorem
Monoid.fg_of_surjective
{M : Type u_1}
[Monoid M]
{M' : Type u_3}
[Monoid M']
[Monoid.FG M]
(f : M →* M')
(hf : Function.Surjective ⇑f)
:
Monoid.FG M'
instance
AddMonoid.fg_range
{M : Type u_1}
[AddMonoid M]
{M' : Type u_3}
[AddMonoid M']
[AddMonoid.FG M]
(f : M →+ M')
:
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
instance
Monoid.closure_finset_fg
{M : Type u_1}
[Monoid M]
(s : Finset M)
:
Monoid.FG ↥(Submonoid.closure ↑s)
Equations
- ⋯ = ⋯
Groups and subgroups #
An additive subgroup of H is finitely generated if it is the closure of a finite subset of
H.
Equations
- AddSubgroup.FG P = ∃ (S : Finset G), AddSubgroup.closure ↑S = P
A subgroup of G is finitely generated if it is the closure of a finite subset of G.
Equations
- Subgroup.FG P = ∃ (S : Finset G), Subgroup.closure ↑S = P
abbrev
AddSubgroup.fg_iff.match_1
{G : Type u_1}
[AddGroup G]
(P : AddSubgroup G)
(motive : AddSubgroup.FG P → Prop)
:
∀ (x : AddSubgroup.FG P), (∀ (S : Finset G) (hS : AddSubgroup.closure ↑S = P), motive ⋯) → motive x
Equations
- ⋯ = ⋯
abbrev
AddSubgroup.fg_iff.match_2
{G : Type u_1}
[AddGroup G]
(P : AddSubgroup G)
(motive : (∃ (S : Set G), AddSubgroup.closure S = P ∧ Set.Finite S) → Prop)
:
∀ (x : ∃ (S : Set G), AddSubgroup.closure S = P ∧ Set.Finite S),
(∀ (S : Set G) (hS : AddSubgroup.closure S = P) (hf : Set.Finite S), motive ⋯) → motive x
Equations
- ⋯ = ⋯
theorem
AddSubgroup.fg_iff
{G : Type u_3}
[AddGroup G]
(P : AddSubgroup G)
:
AddSubgroup.FG P ↔ ∃ (S : Set G), AddSubgroup.closure S = P ∧ Set.Finite S
An equivalent expression of AddSubgroup.fg in terms of Set.Finite instead of
Finset.
theorem
Subgroup.fg_iff
{G : Type u_3}
[Group G]
(P : Subgroup G)
:
Subgroup.FG P ↔ ∃ (S : Set G), Subgroup.closure S = P ∧ Set.Finite S
An equivalent expression of Subgroup.FG in terms of Set.Finite instead of Finset.
theorem
AddSubgroup.fg_iff_addSubmonoid_fg
{G : Type u_3}
[AddGroup G]
(P : AddSubgroup G)
:
AddSubgroup.FG P ↔ AddSubmonoid.FG P.toAddSubmonoid
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}
[Group G]
(P : Subgroup G)
:
Subgroup.FG P ↔ Submonoid.FG P.toSubmonoid
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}
[Group G]
(P : Subgroup G)
:
Subgroup.FG P ↔ AddSubgroup.FG (Subgroup.toAddSubgroup P)
theorem
AddSubgroup.fg_iff_mul_fg
{H : Type u_4}
[AddGroup H]
(P : AddSubgroup H)
:
AddSubgroup.FG P ↔ Subgroup.FG (AddSubgroup.toSubgroup P)
A group is finitely generated if it is finitely generated as a submonoid of itself.
- out : Subgroup.FG ⊤
An additive group is finitely generated if it is finitely generated as an additive submonoid of itself.
- out : AddSubgroup.FG ⊤
theorem
AddGroup.fg_iff
{G : Type u_3}
[AddGroup G]
:
AddGroup.FG G ↔ ∃ (S : Set G), AddSubgroup.closure S = ⊤ ∧ Set.Finite S
An equivalent expression of AddGroup.fg in terms of Set.Finite instead of Finset.
theorem
Group.fg_iff
{G : Type u_3}
[Group G]
:
Group.FG G ↔ ∃ (S : Set G), Subgroup.closure S = ⊤ ∧ Set.Finite S
An equivalent expression of Group.FG in terms of Set.Finite instead of Finset.
theorem
AddGroup.fg_iff'
{G : Type u_3}
[AddGroup G]
:
AddGroup.FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ AddSubgroup.closure ↑S = ⊤
abbrev
AddGroup.fg_iff'.match_1
{G : Type u_1}
[AddGroup G]
(motive : AddSubgroup.FG ⊤ → Prop)
:
∀ (x : AddSubgroup.FG ⊤), (∀ (S : Finset G) (hS : AddSubgroup.closure ↑S = ⊤), motive ⋯) → motive x
Equations
- ⋯ = ⋯
An additive group is finitely generated if and only if it is finitely generated as an additive monoid.
@[simp]
theorem
AddGroup.fg_iff_addSubgroup_fg
{G : Type u_3}
[AddGroup G]
(H : AddSubgroup G)
:
AddGroup.FG ↥H ↔ AddSubgroup.FG H
@[simp]
theorem
Group.fg_iff_subgroup_fg
{G : Type u_3}
[Group G]
(H : Subgroup G)
:
Group.FG ↥H ↔ Subgroup.FG H
theorem
AddGroup.fg_iff_mul_fg
{H : Type u_4}
[AddGroup H]
:
AddGroup.FG H ↔ Group.FG (Multiplicative H)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
AddGroup.fg_of_surjective
{G : Type u_3}
[AddGroup G]
{G' : Type u_5}
[AddGroup G']
[hG : AddGroup.FG G]
{f : G →+ G'}
(hf : Function.Surjective ⇑f)
:
AddGroup.FG G'
theorem
Group.fg_of_surjective
{G : Type u_3}
[Group G]
{G' : Type u_5}
[Group G']
[hG : Group.FG G]
{f : G →* G'}
(hf : Function.Surjective ⇑f)
:
Group.FG G'
instance
AddGroup.fg_range
{G : Type u_3}
[AddGroup G]
{G' : Type u_5}
[AddGroup G']
[AddGroup.FG G]
(f : G →+ G')
:
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
instance
Group.closure_finset_fg
{G : Type u_3}
[Group G]
(s : Finset G)
:
Group.FG ↥(Subgroup.closure ↑s)
Equations
- ⋯ = ⋯
instance
Group.closure_finite_fg
{G : Type u_3}
[Group G]
(s : Set G)
[Finite ↑s]
:
Group.FG ↥(Subgroup.closure s)
Equations
- ⋯ = ⋯
The minimum number of generators of an additive group
Equations
- AddGroup.rank G = Nat.find ⋯
The minimum number of generators of a group.
Equations
- Group.rank G = Nat.find ⋯
theorem
AddGroup.rank_spec
(G : Type u_3)
[AddGroup G]
[h : AddGroup.FG G]
:
∃ (S : Finset G), S.card = AddGroup.rank G ∧ AddSubgroup.closure ↑S = ⊤
theorem
Group.rank_spec
(G : Type u_3)
[Group G]
[h : Group.FG G]
:
∃ (S : Finset G), S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
theorem
AddGroup.rank_le
(G : Type u_3)
[AddGroup G]
[h : AddGroup.FG G]
{S : Finset G}
(hS : AddSubgroup.closure ↑S = ⊤)
:
AddGroup.rank G ≤ S.card
theorem
Group.rank_le
(G : Type u_3)
[Group G]
[h : Group.FG G]
{S : Finset G}
(hS : Subgroup.closure ↑S = ⊤)
:
Group.rank G ≤ S.card
theorem
AddGroup.rank_le_of_surjective
{G : Type u_3}
[AddGroup G]
{G' : Type u_5}
[AddGroup G']
[AddGroup.FG G]
[AddGroup.FG G']
(f : G →+ G')
(hf : Function.Surjective ⇑f)
:
AddGroup.rank G' ≤ AddGroup.rank G
theorem
Group.rank_le_of_surjective
{G : Type u_3}
[Group G]
{G' : Type u_5}
[Group G']
[Group.FG G]
[Group.FG G']
(f : G →* G')
(hf : Function.Surjective ⇑f)
:
Group.rank G' ≤ Group.rank G
theorem
AddGroup.rank_range_le
{G : Type u_3}
[AddGroup G]
{G' : Type u_5}
[AddGroup G']
[AddGroup.FG G]
{f : G →+ G'}
:
theorem
Group.rank_range_le
{G : Type u_3}
[Group G]
{G' : Type u_5}
[Group G']
[Group.FG G]
{f : G →* G'}
:
Group.rank ↥(MonoidHom.range f) ≤ Group.rank G
theorem
AddGroup.rank_congr
{G : Type u_3}
[AddGroup G]
{G' : Type u_5}
[AddGroup G']
[AddGroup.FG G]
[AddGroup.FG G']
(f : G ≃+ G')
:
AddGroup.rank G = AddGroup.rank G'
theorem
Group.rank_congr
{G : Type u_3}
[Group G]
{G' : Type u_5}
[Group G']
[Group.FG G]
[Group.FG G']
(f : G ≃* G')
:
Group.rank G = Group.rank G'
theorem
AddSubgroup.rank_congr
{G : Type u_3}
[AddGroup G]
{H : AddSubgroup G}
{K : AddSubgroup G}
[AddGroup.FG ↥H]
[AddGroup.FG ↥K]
(h : H = K)
:
AddGroup.rank ↥H = AddGroup.rank ↥K
theorem
Subgroup.rank_congr
{G : Type u_3}
[Group G]
{H : Subgroup G}
{K : Subgroup G}
[Group.FG ↥H]
[Group.FG ↥K]
(h : H = K)
:
Group.rank ↥H = Group.rank ↥K
theorem
AddSubgroup.rank_closure_finset_le_card
{G : Type u_3}
[AddGroup G]
(s : Finset G)
:
AddGroup.rank ↥(AddSubgroup.closure ↑s) ≤ s.card
theorem
Subgroup.rank_closure_finset_le_card
{G : Type u_3}
[Group G]
(s : Finset G)
:
Group.rank ↥(Subgroup.closure ↑s) ≤ s.card
theorem
AddSubgroup.rank_closure_finite_le_nat_card
{G : Type u_3}
[AddGroup G]
(s : Set G)
[Finite ↑s]
:
AddGroup.rank ↥(AddSubgroup.closure s) ≤ Nat.card ↑s
theorem
Subgroup.rank_closure_finite_le_nat_card
{G : Type u_3}
[Group G]
(s : Set G)
[Finite ↑s]
:
Group.rank ↥(Subgroup.closure s) ≤ Nat.card ↑s
instance
QuotientAddGroup.fg
{G : Type u_3}
[AddGroup G]
[AddGroup.FG G]
(N : AddSubgroup G)
[AddSubgroup.Normal N]
:
AddGroup.FG (G ⧸ N)
Equations
- ⋯ = ⋯
instance
QuotientGroup.fg
{G : Type u_3}
[Group G]
[Group.FG G]
(N : Subgroup G)
[Subgroup.Normal N]
:
Equations
- ⋯ = ⋯