Group generators as data

Main definitions

• Group.Generators G ι: The generators of a group are given by a generating family indexed by ι and an assignment val : ι → G such that Subgroup.closure (Set.range val) = ⊤.

Main results

• Group.Generators.hom_ext: if two homomorphisms coincide on the elements of a generating family, then they are equal.
• Group.fg_iff_nonempty_finite_generators: a group is finitely generated if and only if it admits a finite generating family.

Implementation notes

• The index type ι is a parameter, not a field, following the pattern of Algebra.Generators.
• Unlike Algebra.Generators, this structure bundles no section of FreeGroup.lift val, it just bundles a proof of surjectivity.

References

• D. F. Holt, S. Rees, C. E. Röver, Groups, Languages and Automata, §1

Tags

group generators, generating set, finitely generated

structure AddGroup.Generators (G : Type u_5) [AddGroup G] (ι : Type u_6) : Type (max u_5 u_6)

The generators of an additive group are given by a generating family indexed by ι and an assignment val : ι → G such that AddSubgroup.closure (Set.range val) = ⊤.

• val : ι → G

  The generating family itself: val i is the element of G indexed by i : ι.

• closure_eq_top : AddSubgroup.closure (Set.range self.val) = ⊤

  The additive subgroup closure of the generators is the whole group.

structure Group.Generators (G : Type u_5) [Group G] (ι : Type u_6) : Type (max u_5 u_6)

The generators of a group are given by a generating family indexed by ι and an assignment val : ι → G such that Subgroup.closure (Set.range val) = ⊤.

• val : ι → G

  The generating family itself: val i is the element of G indexed by i : ι.

• closure_eq_top : Subgroup.closure (Set.range self.val) = ⊤

  The subgroup closure of the generators is the whole group.

@[reducible, inline]

abbrev Group.Generators.lift {G : Type u_1} {ι : Type u_3} [Group G] (P : Generators G ι) : FreeGroup ι →* G

The canonical surjection from the free group on the generators to G.

Equations

• P.lift = FreeGroup.lift P.val

@[reducible, inline]

abbrev AddGroup.Generators.lift {G : Type u_1} {ι : Type u_3} [AddGroup G] (P : Generators G ι) : FreeAddGroup ι →+ G

The canonical surjection from the free additive group on the generators to G.

Equations

• P.lift = FreeAddGroup.lift P.val

theorem Group.Generators.lift_surjective {G : Type u_1} {ι : Type u_3} [Group G] (P : Generators G ι) : Function.Surjective ⇑P.lift

theorem AddGroup.Generators.lift_surjective {G : Type u_1} {ι : Type u_3} [AddGroup G] (P : Generators G ι) : Function.Surjective ⇑P.lift

@[deprecated Group.Generators.lift_surjective (since := "2026-08-21")]

theorem Group.Generators.lift_val_surjective {G : Type u_1} {ι : Type u_3} [Group G] (P : Generators G ι) : Function.Surjective ⇑P.lift

Alias of Group.Generators.lift_surjective.

@[simp]

theorem Group.Generators.range_lift_eq_top {G : Type u_1} {ι : Type u_3} [Group G] (P : Generators G ι) : P.lift.range = ⊤

@[simp]

theorem AddGroup.Generators.range_lift_eq_top {G : Type u_1} {ι : Type u_3} [AddGroup G] (P : Generators G ι) : P.lift.range = ⊤

theorem Group.Generators.hom_ext {G : Type u_1} {ι : Type u_3} [Group G] (P : Generators G ι) {M : Type u_5} [Monoid M] (f g : G →* M) (h : ∀ (i : ι), f (P.val i) = g (P.val i)) : f = g

If two homomorphisms coincide on the elements of a generating family, then they are equal.

theorem AddGroup.Generators.hom_ext {G : Type u_1} {ι : Type u_3} [AddGroup G] (P : Generators G ι) {M : Type u_5} [AddMonoid M] (f g : G →+ M) (h : ∀ (i : ι), f (P.val i) = g (P.val i)) : f = g

If two additive homomorphisms coincide on the elements of a generating family, then they are equal.

def Group.Generators.ofSet {G : Type u_1} [Group G] {S : Set G} (h : Subgroup.closure S = ⊤) : Generators G ↑S

The generating family obtained using a generating set S : Set G.

Equations

• Group.Generators.ofSet h = { val := Subtype.val, closure_eq_top := ⋯ }

def AddGroup.Generators.ofSet {G : Type u_1} [AddGroup G] {S : Set G} (h : AddSubgroup.closure S = ⊤) : Generators G ↑S

The generating family obtained using a generating set S : Set G.

Equations

• AddGroup.Generators.ofSet h = { val := Subtype.val, closure_eq_top := ⋯ }

@[simp]

theorem Group.Generators.ofSet_val {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) : (ofSet hS).val = Subtype.val

@[simp]

theorem AddGroup.Generators.ofSet_val {G : Type u_1} [AddGroup G] {S : Set G} (hS : AddSubgroup.closure S = ⊤) : (ofSet hS).val = Subtype.val

def Group.Generators.ofFreeGroupHom {G : Type u_1} {ι : Type u_3} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) : Generators G ι

The generating family given by the canonical surjection from FreeGroup ι.

Equations

• Group.Generators.ofFreeGroupHom φ hφ = { val := ⇑φ ∘ FreeGroup.of, closure_eq_top := ⋯ }

def AddGroup.Generators.ofFreeAddGroupHom {G : Type u_1} {ι : Type u_3} [AddGroup G] (φ : FreeAddGroup ι →+ G) (hφ : Function.Surjective ⇑φ) : Generators G ι

The generating family given by the canonical surjection from FreeAddGroup ι.

Equations

• AddGroup.Generators.ofFreeAddGroupHom φ hφ = { val := ⇑φ ∘ FreeAddGroup.of, closure_eq_top := ⋯ }

@[simp]

theorem Group.Generators.ofFreeGroupHom_val {G : Type u_1} {ι : Type u_3} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) : (ofFreeGroupHom φ hφ).val = ⇑φ ∘ FreeGroup.of

@[simp]

theorem AddGroup.Generators.ofFreeAddGroupHom_val {G : Type u_1} {ι : Type u_3} [AddGroup G] (φ : FreeAddGroup ι →+ G) (hφ : Function.Surjective ⇑φ) : (ofFreeAddGroupHom φ hφ).val = ⇑φ ∘ FreeAddGroup.of

@[simp]

theorem Group.Generators.ofFreeGroupHom_lift {G : Type u_1} {ι : Type u_3} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) : (ofFreeGroupHom φ hφ).lift = φ

The canonical surjection attached to ofFreeGroupHom φ hφ is φ.

@[simp]

theorem AddGroup.Generators.ofFreeAddGroupHom_lift {G : Type u_1} {ι : Type u_3} [AddGroup G] (φ : FreeAddGroup ι →+ G) (hφ : Function.Surjective ⇑φ) : (ofFreeAddGroupHom φ hφ).lift = φ

The canonical surjection attached to ofFreeAddGroupHom φ hφ is φ.

def Group.Generators.map {G : Type u_1} {H : Type u_2} {ι : Type u_3} [Group G] [Group H] (P : Generators G ι) (f : G →* H) (hf : Function.Surjective ⇑f) : Generators H ι

The transport of a generating family along a surjective homomorphism.

Equations

• P.map f hf = { val := ⇑f ∘ P.val, closure_eq_top := ⋯ }

def AddGroup.Generators.map {G : Type u_1} {H : Type u_2} {ι : Type u_3} [AddGroup G] [AddGroup H] (P : Generators G ι) (f : G →+ H) (hf : Function.Surjective ⇑f) : Generators H ι

The transport of a generating family along a surjective additive homomorphism.

Equations

• P.map f hf = { val := ⇑f ∘ P.val, closure_eq_top := ⋯ }

@[simp]

theorem Group.Generators.map_val {G : Type u_1} {H : Type u_2} {ι : Type u_3} [Group G] [Group H] (P : Generators G ι) (f : G →* H) (hf : Function.Surjective ⇑f) : (P.map f hf).val = ⇑f ∘ P.val

@[simp]

theorem AddGroup.Generators.map_val {G : Type u_1} {H : Type u_2} {ι : Type u_3} [AddGroup G] [AddGroup H] (P : Generators G ι) (f : G →+ H) (hf : Function.Surjective ⇑f) : (P.map f hf).val = ⇑f ∘ P.val

def Group.Generators.reindex {G : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Group G] (P : Generators G ι) {e : ι' → ι} (he : Function.Surjective e) : Generators G ι'

The transport of a generating family along a surjection of index types.

Equations

• P.reindex he = { val := P.val ∘ e, closure_eq_top := ⋯ }

def AddGroup.Generators.reindex {G : Type u_1} {ι : Type u_3} {ι' : Type u_4} [AddGroup G] (P : Generators G ι) {e : ι' → ι} (he : Function.Surjective e) : Generators G ι'

The transport of a generating family along a surjection of index types.

Equations

• P.reindex he = { val := P.val ∘ e, closure_eq_top := ⋯ }

@[simp]

theorem Group.Generators.reindex_val {G : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Group G] (P : Generators G ι) {e : ι' → ι} (he : Function.Surjective e) : (P.reindex he).val = P.val ∘ e

@[simp]

theorem AddGroup.Generators.reindex_val {G : Type u_1} {ι : Type u_3} {ι' : Type u_4} [AddGroup G] (P : Generators G ι) {e : ι' → ι} (he : Function.Surjective e) : (P.reindex he).val = P.val ∘ e

theorem Group.Generators.fg {G : Type u_1} {ι : Type u_3} [Group G] [Finite ι] (P : Generators G ι) : FG G

If G has a finite generating family, then G is finitely generated.

theorem AddGroup.Generators.fg {G : Type u_1} {ι : Type u_3} [AddGroup G] [Finite ι] (P : Generators G ι) : FG G

If G has a finite generating family, then G is finitely generated.

theorem Group.fg_iff_nonempty_finite_generators {G : Type u_1} [Group G] : FG G ↔ ∃ (n : ℕ), Nonempty (Generators G (Fin n))

A group is finitely generated if and only if it admits a finite generating family.

theorem AddGroup.fg_iff_nonempty_finite_generators {G : Type u_1} [AddGroup G] : FG G ↔ ∃ (n : ℕ), Nonempty (Generators G (Fin n))

An additive group is finitely generated if and only if it admits a finite generating family.