# mathlib3documentation

group_theory.presented_group

# Defining a group given by generators and relations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• presented_group 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 α.
• to_group f: the canonical group homomorphism presented_group 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 presented_group {α : Type u_1} (rels : set (free_group α)) :
Type u_1

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

Equations
Instances for presented_group
@[protected, instance]
def presented_group.group {α : Type u_1} (rels : set (free_group α)) :
Equations
def presented_group.of {α : Type u_1} {rels : set (free_group α)} (x : α) :

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

Equations
theorem presented_group.closure_rels_subset_ker {α : Type u_1} {G : Type u_2} [group G] {f : α G} {rels : set (free_group α)} (h : (r : , r rels r = 1) :
theorem presented_group.to_group_eq_one_of_mem_closure {α : Type u_1} {G : Type u_2} [group G] {f : α G} {rels : set (free_group α)} (h : (r : , r rels r = 1) (x : free_group α) (H : x ) :
x = 1
def presented_group.to_group {α : Type u_1} {G : Type u_2} [group G] {f : α G} {rels : set (free_group α)} (h : (r : , r rels r = 1) :

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

Equations
@[simp]
theorem presented_group.to_group.of {α : Type u_1} {G : Type u_2} [group G] {f : α G} {rels : set (free_group α)} (h : (r : , r rels r = 1) {x : α} :
= f x
theorem presented_group.to_group.unique {α : Type u_1} {G : Type u_2} [group G] {f : α G} {rels : set (free_group α)} (h : (r : , r rels r = 1) (g : presented_group rels →* G) (hg : (x : α), g = f x) {x : presented_group rels} :
g x =
@[protected, instance]
def presented_group.inhabited {α : Type u_1} (rels : set (free_group α)) :
Equations