mathlib3 documentation

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 #

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 : free_group α), r rels (free_group.lift f) 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 : free_group α), r rels (free_group.lift f) r = 1) (x : free_group α) (H : x subgroup.normal_closure rels) :
def presented_group.to_group {α : Type u_1} {G : Type u_2} [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 {α : Type u_1} {G : Type u_2} [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 {α : Type u_1} {G : Type u_2} [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} :
@[protected, instance]
def presented_group.inhabited {α : Type u_1} (rels : set (free_group α)) :
Equations