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 #

presented_group 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 α.
to_group f: the canonical group homomorphism presented_group rels → G, given a function f : α → G from a type α to a group G which satisfies the relations rels.

Tags #

generators, relations, group presentations

source

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

presented_group rels = (free_group α ⧸ subgroup.normal_closure rels)

Instances for presented_group

source

@[protected, instance]

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

group (presented_group rels)

Equations

presented_group.group rels = quotient_group.quotient.group (subgroup.normal_closure rels)

source

def presented_group.of {α : Type u_1} {rels : set (free_group α)} (x : α) :

presented_group rels

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

presented_group.of x = quotient_group.mk (free_group.of x)

source

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) :

subgroup.normal_closure rels ≤ (⇑free_group.lift f).ker

source

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) :

⇑(⇑free_group.lift f) x = 1

source

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) :

presented_group rels →* G

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

Equations

presented_group.to_group h = quotient_group.lift (subgroup.normal_closure rels) (⇑free_group.lift f) _

source

@[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 : α} :

⇑(presented_group.to_group h) (presented_group.of x) = f x

source

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} :

⇑g x = ⇑(presented_group.to_group h) x

source

@[protected, instance]

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

inhabited (presented_group rels)

Equations

presented_group.inhabited rels = {default := 1}