Group presentations as data

Group.Presentation extends Group.Generators with a set of relators to form a group presentation as data.

Main definitions

• Group.Presentation G ι: a presentation ⟨ι | rel⟩ of G, extending Group.Generators G ι.

Main results

• Group.Presentation.lift_rel_eq_one: a relator maps to the identity under the canonical surjection.
• Group.isFinitelyPresented_iff_exists_finite_presentation: A group is finitely presented if and only if it admits a presentation with finitely many generators and finitely many relators.

Implementation notes

• Relators are a Set because (Subgroup.normalClosure, PresentedGroup) take a set as input.
• The kernel condition lift_ker_eq_normalClosure uses toGenerators.lift as in with Algebra.Presentation.

References

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

Tags

group presentation, generators and relations

structure Group.Presentation (G : Type u_3) (ι : Type u_4) [Group G] extends Group.Generators G ι : Type (max u_3 u_4)

A group presentation is given by a generating family (val : ι → G) and a set of relators (rel : Set (FreeGroup ι)) such that the normal subgroup generated by the relators is exactly the kernel of the canonical lift from the free group on the generators to G.

• val : ι → G
• closure_eq_top : Subgroup.closure (Set.range self.val) = ⊤
• rel : Set (FreeGroup ι)

  The set of relators, as words in the free group; each r ∈ rel is read as r = 1 in G.

• lift_ker_eq_normalClosure : self.lift.ker = Subgroup.normalClosure self.rel

  The kernel of the canonical surjection is equal to the normal closure of the relators.

def Group.Presentation.ofFreeGroupHom {G : Type u_1} {ι : Type u_2} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) (rel : Set (FreeGroup ι)) (hrel : φ.ker = Subgroup.normalClosure rel) : Presentation G ι

The presentation given by a surjective homomorphism φ : FreeGroup ι →* G, together with a set of relators whose normal closure is the kernel of φ.

Equations

• Group.Presentation.ofFreeGroupHom φ hφ rel hrel = { toGenerators := Group.Generators.ofFreeGroupHom φ hφ, rel := rel, lift_ker_eq_normalClosure := ⋯ }

@[simp]

theorem Group.Presentation.ofFreeGroupHom_rel {G : Type u_1} {ι : Type u_2} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) (rel : Set (FreeGroup ι)) (hrel : φ.ker = Subgroup.normalClosure rel) : (ofFreeGroupHom φ hφ rel hrel).rel = rel

@[simp]

theorem Group.Presentation.ofFreeGroupHom_val {G : Type u_1} {ι : Type u_2} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) (rel : Set (FreeGroup ι)) (hrel : φ.ker = Subgroup.normalClosure rel) (a✝ : ι) : (ofFreeGroupHom φ hφ rel hrel).val a✝ = φ (FreeGroup.of a✝)

@[simp]

theorem Group.Presentation.ofFreeGroupHom_toGenerators {G : Type u_1} {ι : Type u_2} [Group G] (φ : FreeGroup ι →* G) (hφ : Function.Surjective ⇑φ) (rel : Set (FreeGroup ι)) (hrel : φ.ker = Subgroup.normalClosure rel) : (ofFreeGroupHom φ hφ rel hrel).toGenerators = Generators.ofFreeGroupHom φ hφ

theorem Group.Presentation.ker_lift {G : Type u_1} {ι : Type u_2} [Group G] (P : Presentation G ι) : P.lift.ker = Subgroup.normalClosure P.rel

@[simp]

theorem Group.Presentation.lift_rel_eq_one {G : Type u_1} {ι : Type u_2} [Group G] (P : Presentation G ι) {r : FreeGroup ι} (hr : r ∈ P.rel) : P.lift r = 1

A relator as a free group element always maps to the identity under the canonical surjection.

theorem Group.Presentation.isFinitelyNormallyGenerated_ker_lift {G : Type u_1} {ι : Type u_2} [Group G] (P : Presentation G ι) (hrel : P.rel.Finite) : P.lift.ker.IsFinitelyNormallyGenerated

noncomputable def Group.Presentation.presentedGroupEquiv {G : Type u_1} {ι : Type u_2} [Group G] (P : Presentation G ι) : PresentedGroup P.rel ≃* G

G, with presentation P, is isomorphic to the PresentedGroup given by P.rel.

Equations

• P.presentedGroupEquiv = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective P.lift ⋯)

theorem Group.Presentation.isFinitelyPresented {G : Type u_1} {ι : Type u_2} [Group G] (P : Presentation G ι) [Finite ι] (hrel : P.rel.Finite) : IsFinitelyPresented G

A group with a finite presentation is finitely presented.

theorem Group.Presentation.isFinitelyPresented_iff_exists_finite_presentation {G : Type u_1} [Group G] : IsFinitelyPresented G ↔ ∃ (n : ℕ) (P : Presentation G (Fin n)), P.rel.Finite

A group is finitely presented if and only if it admits a presentation with finitely many generators and finitely many relators.