Timings for Presentation.v
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 Spaces.List.Core.
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.
exact (GroupCoeq
(FreeGroup_rec R)
(FreeGroup_rec (fun x => @group_unit (FreeGroup X)))).
(** 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 & forall r,
FreeGroup_rec f (gp_relators P r) = group_unit}
<~> GroupHomomorphism G H.
refine ((equiv_precompose_cat_equiv grp_iso_presentation (z:=H))^-1 oE _).
refine (equiv_groupcoeq_rec _ _ oE _).
srefine (equiv_functor_sigma_pb _ oE _).
2: apply equiv_freegroup_rec.
apply equiv_functor_sigma_id.
change (equiv_freegroup_rec H _ f $o FreeGroup_rec (gp_relators P)
$== equiv_freegroup_rec _ _ f $o FreeGroup_rec (fun _ => group_unit)).
rapply FreeGroup_ind_homotopy.
exact (p (freegroup_in r)).
(** ** Constructors for finite presentations *)
Definition Build_Finite_GroupPresentation n m
(f : FinSeq m (FreeGroup (Fin n)))
: GroupPresentation.
snapply Build_GroupPresentation.
Instance FinitelyGeneratedPresentation_Build_Finite_GroupPresentation
{n m f}
: FinitelyGeneratedPresentation (Build_Finite_GroupPresentation n m f).
2: simpl; apply tr; reflexivity.
Instance FinitelyRelatedPresentation_Build_Finite_GroupPresentation
{n m f}
: FinitelyRelatedPresentation (Build_Finite_GroupPresentation n m f).
2: simpl; apply tr; reflexivity.
(** ** 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.
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).
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).
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).