Defining a group given by generators and relations

Given a subset rels of relations of the free group on a type α, this file constructs the group given by generators x : α and relations r ∈ rels.

Main definitions

• PresentedGroup rels: the quotient group of the free group on a type α by a subset rels of relations of the free group on α.
• of: The canonical map from α to a presented group with generators α.
• toGroup f: the canonical group homomorphism PresentedGroup rels → G, given a function f : α → G from a type α to a group G which satisfies the relations rels.

Tags

generators, relations, group presentations

def PresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) : Type u_1

Given a set of relations, rels, over a type α, PresentedGroup constructs the group with generators x : α and relations rels as a quotient of FreeGroup α.

instance PresentedGroup.instGroupPresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) : Group (PresentedGroup rels)

def PresentedGroup.of {α : Type u_1} {rels : Set (FreeGroup α)} (x : α) : PresentedGroup rels

of is the canonical map from α to a presented group with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeGroup α.

theorem PresentedGroup.closure_rels_subset_ker {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1) : Subgroup.normalClosure rels ≤ MonoidHom.ker (↑FreeGroup.lift f)

theorem PresentedGroup.to_group_eq_one_of_mem_closure {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1) (x : FreeGroup α) : x ∈ Subgroup.normalClosure rels → ↑(↑FreeGroup.lift f) x = 1

def PresentedGroup.toGroup {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1) : PresentedGroup rels →* G

The extension of a map f : α → G that satisfies the given relations to a group homomorphism from PresentedGroup rels → G.

@[simp]

theorem PresentedGroup.toGroup.of {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1) {x : α} : ↑(PresentedGroup.toGroup h) (PresentedGroup.of x) = f x

theorem PresentedGroup.toGroup.unique {α : Type u_1} {G : Type u_2} [Group G] {f : α → G} {rels : Set (FreeGroup α)} (h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1) (g : PresentedGroup rels →* G) (hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x) {x : PresentedGroup rels} : ↑g x = ↑(PresentedGroup.toGroup h) x

instance PresentedGroup.instInhabitedPresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) : Inhabited (PresentedGroup rels)