Library HoTT.Algebra.Groups.Presentation

Require Import Basics Types.
Require Import Truncations.Core.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.FreeGroup.
Require Import Algebra.Groups.GroupCoeq.
Require Import Spaces.Finite.
Require Import WildCat.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

In this file we develop presentations of groups.

The data of a group presentation

Record GroupPresentation := {

We have a type of generators

gp_generators : Type ;

An indexing type for relators

gp_rel_index : Type ;

The relators are picked out amongst elements of the free group on the generators.

gp_relators : gp_rel_index → FreeGroup gp_generators;
}.

Note: A relator is a relation in the form of "w = 1", any relation "w = v" can become a relator "wv^-1 = 1" for words v and w.

Given the data of a group presentation we can construct the group. This is sometimes called the presented group.

Definition group_gp : GroupPresentation → Group.
Proof.
  intros [X I R].
  exact (GroupCoeq
    (FreeGroup_rec I (FreeGroup X) R)
    (FreeGroup_rec I (FreeGroup X) (fun x ⇒ @group_unit (FreeGroup X)))).
Defined.

A group G has a presentation if there exists a group presentation whose presented group is isomorphic to G.

Class HasPresentation (G : Group) := {
presentation : GroupPresentation;
grp_iso_presentation : GroupIsomorphism (group_gp presentation) G;
}.

Coercion presentation : HasPresentation >-> GroupPresentation.

Here are a few finiteness properties of group presentations.

A group presentation is finitely generated if its generating set is finite.

Class FinitelyGeneratedPresentation (P : GroupPresentation)
:= finite_gp_generators : Finite (gp_generators P).

A group presentation is finitely related if its relators indexing set is finite.

Class FinitelyRelatedPresentation (P : GroupPresentation)
:= finite_gp_relators : Finite (gp_rel_index P).

A group presentation is a finite presentation if it is finitely generated and related.

Class FinitePresentation (P : GroupPresentation) := {
fp_generators : FinitelyGeneratedPresentation P;
fp_relators : FinitelyRelatedPresentation P;
}.

These directly translate into properties of groups.

A group is finitely generated if it has a finitely generated presentation.

Class IsFinitelyGenerated (G : Group) := {
fg_presentation : HasPresentation G;
fg_presentation_fg : FinitelyGeneratedPresentation fg_presentation;
}.

A group is finitely related if it has a finitely related presentation.

Class IsFinitelyRelated (G : Group) := {
  fr_presentation : HasPresentation G;
  fr_presentation_fr : FinitelyRelatedPresentation fr_presentation;
}.

Class IsFinitelyPresented (G : Group) := {
  fp_presentation : HasPresentation G;
  fp_presentation_fp : FinitePresentation fp_presentation;
}.

Fundamental theorem of presentations of groups

A group homomorphism from a presented group is determined with how the underlying map acts on generators subject to the condition that relators are sent to the unit.

Theorem grp_pres_rec {funext : Funext} (G : Group) (P : HasPresentation G) (H : Group)
  : {f : gp_generators P → H & ∀ r ,
      FreeGroup_rec _ _ f (gp_relators P r) = group_unit }
    <~> GroupHomomorphism G H.
Proof.
  refine ((equiv_precompose_cat_equiv grp_iso_presentation )^-1 oE _).
  refine (equiv_groupcoeq_rec _ _ oE _).
  srefine (equiv_functor_sigma_pb _ oE _).
  2: apply equiv_freegroup_rec.
  apply equiv_functor_sigma_id.
  intros f.
  srapply equiv_iff_hprop.
  { intros p.
    hnf.
    rapply Trunc_ind.
    srapply Coeq.Coeq_ind.
    2: intros; apply path_ishprop.
    intros w; hnf.
    induction w.
    1: reflexivity.
    simpl.
    refine (_ @ _ @ _^).
    1,3: exact (grp_homo_op (FreeGroup_rec _ _ _) _ _).
    f_ap.
    destruct a.
    1: refine (p _ @ (grp_homo_unit _)^).
    refine (grp_homo_inv _ _ @ ap _ _ @ (grp_homo_inv _ _)^).
    refine (p _ @ (grp_homo_unit _)^). }
  intros p r.
  hnf in p.
  pose (p' := p o freegroup_eta).
  clearbody p'; clear p.
  specialize (p' (FreeGroup.word_sing _ (inl r))).
  refine (_ @ p').
  clear p'.
  symmetry.
  refine (grp_homo_op _ _ _ @ _).
  refine (_ @ right_identity _).
  f_ap.
Defined.

Constructors for finite presentations

Definition Build_Finite_GroupPresentation n m
  (f : FinSeq m (FreeGroup (Fin n)))
  : GroupPresentation.
Proof.
  snrapply Build_GroupPresentation.
  - exact (Fin n).
  - exact (Fin m).
  - exact f.
Defined.

Global Instance FinitelyGeneratedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyGeneratedPresentation (Build_Finite_GroupPresentation n m f).
Proof.
  unshelve econstructor.
  2: simpl; apply tr; reflexivity.
Defined.

Global Instance FinitelyRelatedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyRelatedPresentation (Build_Finite_GroupPresentation n m f).
Proof.
  unshelve econstructor.
  2: simpl; apply tr; reflexivity.
Defined.

Notations for presentations

Convenient abbreviation when defining notations.

Local Notation ff := (freegroup_in o fin_nat).

TODO: I haven't worked out how to generalize to any number of binders, so we explicitly list the first few levels.

Local Open Scope nat_scope.

One generator

Notation "⟨ x | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 1 _
    (fscons ((fun (x : FreeGroup (Fin 1))
      ⇒ F : FreeGroup (Fin _)) (ff 0%nat))
    .. (fscons ((fun (x : FreeGroup (Fin 1))
      ⇒ G : FreeGroup (Fin _)) (ff 0)) fsnil) ..))
  (at level 200, x binder).

Two generators

Notation "⟨ x , y | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 2 _
    (fscons ((fun (x y : FreeGroup (Fin 2))
      ⇒ F : FreeGroup (Fin _)) (ff 0) (ff 1))
    .. (fscons ((fun (x y : FreeGroup (Fin 2))
      ⇒ G : FreeGroup (Fin _)) (ff 0) (ff 1)) fsnil) ..))
  (at level 200, x binder, y binder).

Three generators

Notation "⟨ x , y , z | F , .. , G ⟩" :=
  (Build_Finite_GroupPresentation 3 _
    (fscons ((fun (x y z : FreeGroup (Fin 3))
      ⇒ F : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2))
    .. (fscons ((fun (x y z : FreeGroup (Fin 3))
      ⇒ G : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2)) fsnil) ..))
  (at level 200, x binder, y binder, z binder).