Documentation

Mathlib.GroupTheory.PresentedGroup

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 PresentedGroup {α : Type u_1} (rels : Set (FreeGroup α)) :
Type u_1

Given a set of relations, rels, over a type α, PresentedGroup constructs the group with generators x : α and relations rels as a quotient of FreeGroup α.

Equations
Instances For
    def PresentedGroup.of {α : Type u_1} {rels : Set (FreeGroup α)} (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 FreeGroup α.

    Equations
    Instances For
      @[simp]
      theorem PresentedGroup.closure_range_of {α : Type u_1} (rels : Set (FreeGroup α)) :
      Subgroup.closure (Set.range PresentedGroup.of) =

      The generators of a presented group generate the presented group. That is, the subgroup closure of the set of generators equals .

      theorem PresentedGroup.closure_rels_subset_ker {α : Type u_1} {G : Type u_2} [Group G] {f : αG} {rels : Set (FreeGroup α)} (h : rrels, (FreeGroup.lift f) r = 1) :
      Subgroup.normalClosure rels (FreeGroup.lift f).ker
      theorem PresentedGroup.to_group_eq_one_of_mem_closure {α : Type u_1} {G : Type u_2} [Group G] {f : αG} {rels : Set (FreeGroup α)} (h : rrels, (FreeGroup.lift f) r = 1) (x : FreeGroup α) :
      x Subgroup.normalClosure rels(FreeGroup.lift f) x = 1
      def PresentedGroup.toGroup {α : Type u_1} {G : Type u_2} [Group G] {f : αG} {rels : Set (FreeGroup α)} (h : rrels, (FreeGroup.lift f) r = 1) :

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

      Equations
      Instances For
        @[simp]
        theorem PresentedGroup.toGroup.of {α : Type u_1} {G : Type u_2} [Group G] {f : αG} {rels : Set (FreeGroup α)} (h : rrels, (FreeGroup.lift f) r = 1) {x : α} :
        theorem PresentedGroup.toGroup.unique {α : Type u_1} {G : Type u_2} [Group G] {f : αG} {rels : Set (FreeGroup α)} (h : rrels, (FreeGroup.lift f) r = 1) (g : PresentedGroup rels →* G) (hg : ∀ (x : α), g (PresentedGroup.of x) = f x) {x : PresentedGroup rels} :
        theorem PresentedGroup.ext_iff {α : Type u_1} {G : Type u_2} [Group G] {rels : Set (FreeGroup α)} {φ : PresentedGroup rels →* G} {ψ : PresentedGroup rels →* G} :
        φ = ψ ∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)
        theorem PresentedGroup.ext {α : Type u_1} {G : Type u_2} [Group G] {rels : Set (FreeGroup α)} {φ : PresentedGroup rels →* G} {ψ : PresentedGroup rels →* G} (hx : ∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)) :
        φ = ψ
        def PresentedGroup.equivPresentedGroup {α : Type u_1} {β : Type u_3} (rels : Set (FreeGroup α)) (e : α β) :

        Presented groups of isomorphic types are isomorphic.

        Equations
        Instances For
          theorem PresentedGroup.equivPresentedGroup_apply_of {α : Type u_1} {β : Type u_3} (x : α) (rels : Set (FreeGroup α)) (e : α β) :
          theorem PresentedGroup.equivPresentedGroup_symm_apply_of {α : Type u_1} {β : Type u_3} (x : β) (rels : Set (FreeGroup α)) (e : α β) :
          instance PresentedGroup.instInhabited {α : Type u_1} (rels : Set (FreeGroup α)) :
          Equations