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 #
presented_group rels
: the quotient group of the free group on a typeα
by a subsetrels
of relations of the free group onα
.of
: The canonical map fromα
to a presented group with generatorsα
.to_group f
: the canonical group homomorphismpresented_group rels → G
, given a functionf : α → G
from a typeα
to a groupG
which satisfies the relationsrels
.
Tags #
generators, relations, group presentations
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
@[protected, instance]
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 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) :
subgroup.normal_closure rels ≤ (⇑free_group.lift f).ker
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) :
⇑(⇑free_group.lift f) x = 1
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) :
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
@[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 : α} :
⇑(presented_group.to_group h) (presented_group.of x) = f 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} :
⇑g x = ⇑(presented_group.to_group h) x
@[protected, instance]
def
presented_group.inhabited
{α : Type}
(rels : set (free_group α)) :
inhabited (presented_group rels)
Equations
- presented_group.inhabited rels = {default := 1}