group_theory.finiteness

source

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.

Equations

P.fg = ∃ (S : finset M), add_submonoid.closure ↑S = P

source

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

P.fg = ∃ (S : finset M), submonoid.closure ↑S = P

source

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.

source

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.

source

theorem submonoid.fg_iff_add_fg {M : Type u_1} [monoid M] (P : submonoid M) :

P.fg ↔ (⇑submonoid.to_add_submonoid P).fg

source

theorem add_submonoid.fg_iff_mul_fg {N : Type u_2} [add_monoid N] (P : add_submonoid N) :

P.fg ↔ (⇑add_submonoid.to_submonoid P).fg

source

@[class]

structure monoid.fg (M : Type u_1) [monoid M] :

Prop

out : ⊤.fg

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

Instances

source

@[class]

structure add_monoid.fg (N : Type u_2) [add_monoid N] :

Prop

out : ⊤.fg

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

Instances

source

theorem monoid.fg_def {M : Type u_1} [monoid M] :

monoid.fg M ↔ ⊤.fg

source

theorem add_monoid.fg_def {N : Type u_2} [add_monoid N] :

add_monoid.fg N ↔ ⊤.fg

source

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

monoid.fg M ↔ ∃ (S : set M), submonoid.closure S = ⊤ ∧ S.finite

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

source

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

add_monoid.fg M ↔ ∃ (S : set M), add_submonoid.closure S = ⊤ ∧ S.finite

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

source

theorem monoid.fg_iff_add_fg {M : Type u_1} [monoid M] :

monoid.fg M ↔ add_monoid.fg (additive M)

source

theorem add_monoid.fg_iff_mul_fg {N : Type u_2} [add_monoid N] :

add_monoid.fg N ↔ monoid.fg (multiplicative N)

source

@[protected, instance]

def add_monoid.fg_of_monoid_fg {M : Type u_1} [monoid M] [monoid.fg M] :

add_monoid.fg (additive M)

source

@[protected, instance]

def monoid.fg_of_add_monoid_fg {N : Type u_2} [add_monoid N] [add_monoid.fg N] :

monoid.fg (multiplicative N)

source

theorem submonoid.fg.map {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] {P : submonoid M} (h : P.fg) (e : M →* M') :

(submonoid.map e P).fg

source

theorem add_submonoid.fg.map {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] {P : add_submonoid M} (h : P.fg) (e : M →+ M') :

(add_submonoid.map e P).fg

source

theorem add_submonoid.fg.map_injective {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] {P : add_submonoid M} (e : M →+ M') (he : function.injective ⇑e) (h : (add_submonoid.map e P).fg) :

P.fg

source

theorem submonoid.fg.map_injective {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] {P : submonoid M} (e : M →* M') (he : function.injective ⇑e) (h : (submonoid.map e P).fg) :

P.fg

source

@[simp]

theorem add_monoid.fg_iff_add_submonoid_fg {M : Type u_1} [add_monoid M] (N : add_submonoid M) :

add_monoid.fg ↥N ↔ N.fg

source

@[simp]

theorem monoid.fg_iff_submonoid_fg {M : Type u_1} [monoid M] (N : submonoid M) :

monoid.fg ↥N ↔ N.fg

source

theorem add_monoid.fg_of_surjective {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] [add_monoid.fg M] (f : M →+ M') (hf : function.surjective ⇑f) :

add_monoid.fg M'

source

theorem monoid.fg_of_surjective {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] [monoid.fg M] (f : M →* M') (hf : function.surjective ⇑f) :

monoid.fg M'

source

@[protected, instance]

def monoid.fg_range {M : Type u_1} [monoid M] {M' : Type u_2} [monoid M'] [monoid.fg M] (f : M →* M') :

monoid.fg ↥(f.mrange)

source

@[protected, instance]

def add_monoid.fg_range {M : Type u_1} [add_monoid M] {M' : Type u_2} [add_monoid M'] [add_monoid.fg M] (f : M →+ M') :

add_monoid.fg ↥(f.mrange)

source

theorem submonoid.powers_fg {M : Type u_1} [monoid M] (r : M) :

(submonoid.powers r).fg

source

theorem add_submonoid.multiples_fg {M : Type u_1} [add_monoid M] (r : M) :

(add_submonoid.multiples r).fg

source

@[protected, instance]

def add_monoid.multiples_fg {M : Type u_1} [add_monoid M] (r : M) :

add_monoid.fg ↥(add_submonoid.multiples r)

source

@[protected, instance]

def monoid.powers_fg {M : Type u_1} [monoid M] (r : M) :

monoid.fg ↥(submonoid.powers r)

source

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.

Equations

P.fg = ∃ (S : finset G), add_subgroup.closure ↑S = P

source

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

P.fg = ∃ (S : finset G), subgroup.closure ↑S = P

source

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.

source

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.

source

theorem subgroup.fg_iff_submonoid_fg {G : Type u_3} [group G] (P : subgroup G) :

P.fg ↔ P.to_submonoid.fg

A subgroup is finitely generated if and only if it is finitely generated as a submonoid.

source

theorem add_subgroup.fg_iff_add_submonoid.fg {G : Type u_3} [add_group G] (P : add_subgroup G) :

P.fg ↔ P.to_add_submonoid.fg

An additive subgroup is finitely generated if and only if it is finitely generated as an additive submonoid.

source

theorem subgroup.fg_iff_add_fg {G : Type u_3} [group G] (P : subgroup G) :

P.fg ↔ (⇑subgroup.to_add_subgroup P).fg

source

theorem add_subgroup.fg_iff_mul_fg {H : Type u_4} [add_group H] (P : add_subgroup H) :

P.fg ↔ (⇑add_subgroup.to_subgroup P).fg

source

@[class]

structure group.fg (G : Type u_3) [group G] :

Prop

out : ⊤.fg

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

Instances

source

@[class]

structure add_group.fg (H : Type u_4) [add_group H] :

Prop

out : ⊤.fg

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

Instances

source

theorem group.fg_def {G : Type u_3} [group G] :

group.fg G ↔ ⊤.fg

source

theorem add_group.fg_def {H : Type u_4} [add_group H] :

add_group.fg H ↔ ⊤.fg

source

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

add_group.fg G ↔ ∃ (S : set G), add_subgroup.closure S = ⊤ ∧ S.finite

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

source

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

group.fg G ↔ ∃ (S : set G), subgroup.closure S = ⊤ ∧ S.finite

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

source

theorem add_group.fg_iff' {G : Type u_3} [add_group G] :

add_group.fg G ↔ ∃ (n : ℕ) (S : finset G), S.card = n ∧ add_subgroup.closure ↑S = ⊤

source

theorem group.fg_iff' {G : Type u_3} [group G] :

group.fg G ↔ ∃ (n : ℕ) (S : finset G), S.card = n ∧ subgroup.closure ↑S = ⊤

source

theorem group.fg_iff_monoid.fg {G : Type u_3} [group G] :

group.fg G ↔ monoid.fg G

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

source

theorem add_group.fg_iff_add_monoid.fg {G : Type u_3} [add_group G] :

add_group.fg G ↔ add_monoid.fg G

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

source

theorem group_fg.iff_add_fg {G : Type u_3} [group G] :

group.fg G ↔ add_group.fg (additive G)

source

theorem add_group.fg_iff_mul_fg {H : Type u_4} [add_group H] :

add_group.fg H ↔ group.fg (multiplicative H)

source

@[protected, instance]

def add_group.fg_of_group_fg {G : Type u_3} [group G] [group.fg G] :

add_group.fg (additive G)

source

@[protected, instance]

def group.fg_of_mul_group_fg {H : Type u_4} [add_group H] [add_group.fg H] :

group.fg (multiplicative H)

source

theorem add_group.fg_of_surjective {G : Type u_3} [add_group G] {G' : Type u_1} [add_group G'] [hG : add_group.fg G] {f : G →+ G'} (hf : function.surjective ⇑f) :

add_group.fg G'

source

theorem group.fg_of_surjective {G : Type u_3} [group G] {G' : Type u_1} [group G'] [hG : group.fg G] {f : G →* G'} (hf : function.surjective ⇑f) :

group.fg G'

source

@[protected, instance]

def add_group.fg_range {G : Type u_3} [add_group G] {G' : Type u_1} [add_group G'] [add_group.fg G] (f : G →+ G') :

add_group.fg ↥(f.range)

source

@[protected, instance]

def group.fg_range {G : Type u_3} [group G] {G' : Type u_1} [group G'] [group.fg G] (f : G →* G') :

group.fg ↥(f.range)

source

def add_group.rank (G : Type u_3) [add_group G] [h : add_group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ add_subgroup.closure ↑S = ⊤)] :

ℕ

The minimum number of generators of an additive group

Equations

add_group.rank G = nat.find _

source

def group.rank (G : Type u_3) [group G] [h : group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ subgroup.closure ↑S = ⊤)] :

ℕ

The minimum number of generators of a group.

Equations

group.rank G = nat.find _

source

theorem group.rank_spec (G : Type u_3) [group G] [h : group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ subgroup.closure ↑S = ⊤)] :

∃ (S : finset G), S.card = group.rank G ∧ subgroup.closure ↑S = ⊤

source

theorem add_group.rank_spec (G : Type u_3) [add_group G] [h : add_group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ add_subgroup.closure ↑S = ⊤)] :

∃ (S : finset G), S.card = add_group.rank G ∧ add_subgroup.closure ↑S = ⊤

source

theorem add_group.rank_le (G : Type u_3) [add_group G] [add_group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ add_subgroup.closure ↑S = ⊤)] {S : finset G} (hS : add_subgroup.closure ↑S = ⊤) :

add_group.rank G ≤ S.card

source

theorem group.rank_le (G : Type u_3) [group G] [group.fg G] [decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ subgroup.closure ↑S = ⊤)] {S : finset G} (hS : subgroup.closure ↑S = ⊤) :

group.rank G ≤ S.card

source

@[protected, instance]

def quotient_group.fg {G : Type u_3} [group G] [group.fg G] (N : subgroup G) [N.normal] :

group.fg (G ⧸ N)

source

@[protected, instance]

def quotient_add_group.fg {G : Type u_3} [add_group G] [add_group.fg G] (N : add_subgroup G) [N.normal] :

add_group.fg (G ⧸ N)

mathlib documentation

Finitely generated monoids and groups #

Main definition #

Monoids and submonoids #

Groups and subgroups #