mathlib documentation

group_theory.presented_group

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 #

Tags #

generators, relations, group presentations

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

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
def presented_group.of {α : Type} {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 {α G : Type} [group G] {f : α → G} {rels : set (free_group α)} (h : ∀ (r : free_group α), r rels(free_group.lift f) r = 1) :
theorem presented_group.to_group_eq_one_of_mem_closure {α G : Type} [group G] {f : α → G} {rels : set (free_group α)} (h : ∀ (r : free_group α), r rels(free_group.lift f) r = 1) (x : free_group α) (H : x subgroup.normal_closure rels) :
def presented_group.to_group {α G : Type} [group G] {f : α → G} {rels : set (free_group α)} (h : ∀ (r : free_group α), r rels(free_group.lift f) 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 {α G : Type} [group G] {f : α → G} {rels : set (free_group α)} (h : ∀ (r : free_group α), r rels(free_group.lift f) r = 1) {x : α} :
theorem presented_group.to_group.unique {α G : Type} [group G] {f : α → G} {rels : set (free_group α)} (h : ∀ (r : free_group α), r rels(free_group.lift f) r = 1) (g : presented_group rels →* G) (hg : ∀ (x : α), g (presented_group.of x) = f x) {x : presented_group rels} :
@[instance]
def presented_group.inhabited {α : Type} (rels : set (free_group α)) :
Equations