# 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

Given a set of relations, `rels`

, over a type `α`

, `PresentedGroup`

constructs the group with
generators `x : α`

and relations `rels`

as a quotient of `FreeGroup α`

.

## Instances For

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

Group (PresentedGroup rels)

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)

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`

.

## Instances For

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