# mathlibdocumentation

group_theory.presented_group

def presented_group {α : Type} :
set (free_group α) → Type

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

Equations
@[instance]
def presented_group.group {α : Type} (rels : set (free_group α)) :

Equations
def presented_group.of {α : Type} {rels : set (free_group α)} :
α → presented_group rels

of x is the canonical map from α to a presented group with generators α. 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} [group β] {f : α → β} {rels : set (free_group α)} :
(∀ (r : , r rels r = 1)

theorem presented_group.to_group_eq_one_of_mem_closure {α β : Type} [group β] {f : α → β} {rels : set (free_group α)} (h : ∀ (r : , r rels r = 1) (x : free_group α) :
x x = 1

def presented_group.to_group {α β : Type} [group β] {f : α → β} {rels : set (free_group α)} :
(∀ (r : , r rels r = 1)presented_group rels →* β

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

Equations
@[simp]
theorem presented_group.to_group.of {α β : Type} [group β] {f : α → β} {rels : set (free_group α)} (h : ∀ (r : , r rels r = 1) {x : α} :
= f x

theorem presented_group.to_group.unique {α β : Type} [group β] {f : α → β} {rels : set (free_group α)} (h : ∀ (r : , r rels r = 1) (g : presented_group rels →* β) (hg : ∀ (x : α), g = f x) {x : presented_group rels} :
g x =

@[instance]
def presented_group.inhabited {α : Type} (rels : set (free_group α)) :

Equations