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 #
PresentedGroup 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α
.toGroup f
: the canonical group homomorphismPresentedGroup 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 α
, PresentedGroup
constructs the group with
generators x : α
and relations rels
as a quotient of FreeGroup α
.
Instances For
instance
PresentedGroup.instGroupPresentedGroup
{α : Type u_1}
(rels : Set (FreeGroup α))
:
Group (PresentedGroup rels)
theorem
PresentedGroup.closure_rels_subset_ker
{α : Type u_1}
{G : Type u_2}
[Group G]
{f : α → G}
{rels : Set (FreeGroup α)}
(h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1)
:
Subgroup.normalClosure rels ≤ MonoidHom.ker (↑FreeGroup.lift f)
def
PresentedGroup.toGroup
{α : Type u_1}
{G : Type u_2}
[Group G]
{f : α → G}
{rels : Set (FreeGroup α)}
(h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1)
:
PresentedGroup rels →* G
The extension of a map f : α → G
that satisfies the given relations to a group homomorphism
from PresentedGroup rels → G
.
Instances For
@[simp]
theorem
PresentedGroup.toGroup.of
{α : Type u_1}
{G : Type u_2}
[Group G]
{f : α → G}
{rels : Set (FreeGroup α)}
(h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1)
{x : α}
:
↑(PresentedGroup.toGroup h) (PresentedGroup.of x) = f x
theorem
PresentedGroup.toGroup.unique
{α : Type u_1}
{G : Type u_2}
[Group G]
{f : α → G}
{rels : Set (FreeGroup α)}
(h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1)
(g : PresentedGroup rels →* G)
(hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x)
{x : PresentedGroup rels}
:
↑g x = ↑(PresentedGroup.toGroup h) x
instance
PresentedGroup.instInhabitedPresentedGroup
{α : Type u_1}
(rels : Set (FreeGroup α))
:
Inhabited (PresentedGroup rels)