# 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 α`

.

## Equations

- PresentedGroup rels = (FreeGroup α ⧸ Subgroup.normalClosure rels)

## Instances For

## Equations

`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 α`

.

## Equations

- PresentedGroup.of x = ↑(FreeGroup.of x)

## Instances For

The generators of a presented group generate the presented group. That is, the subgroup closure
of the set of generators equals `⊤`

.

The extension of a map `f : α → G`

that satisfies the given relations to a group homomorphism
from `PresentedGroup rels → G`

.

## Equations

- PresentedGroup.toGroup h = QuotientGroup.lift (Subgroup.normalClosure rels) (FreeGroup.lift f) ⋯

## Instances For

Presented groups of isomorphic types are isomorphic.

## Equations

- PresentedGroup.equivPresentedGroup rels e = QuotientGroup.congr (Subgroup.normalClosure rels) (Subgroup.normalClosure (⇑(FreeGroup.freeGroupCongr e) '' rels)) (FreeGroup.freeGroupCongr e) ⋯

## Instances For

## Equations

- PresentedGroup.instInhabited rels = { default := 1 }