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 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.

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

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.

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 := ⋯ }

@[simp]

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

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 := ⋯ }

@[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

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

The transport of a generating family along an equivalence of index types.

Equations

• P.reindex e = { 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 : ι' ≃ ι) : (P.reindex e).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 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.