Presentation.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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.
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.GroupPresentation -> Group
Proof.GroupPresentation -> Group
  intros [X I R].X, I: Type
R: I -> FreeGroup X
Group
  exact (GroupCoeq
    (FreeGroup_rec R)
    (FreeGroup_rec (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 & forall r,
      FreeGroup_rec f (gp_relators P r) = group_unit}
    <~> GroupHomomorphism G H.funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
GroupHomomorphism G H
Proof.funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
GroupHomomorphism G H
  refine ((equiv_precompose_cat_equiv grp_iso_presentation (z:=H))^-1 oE _).funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
(group_gp P $-> H)
  refine (equiv_groupcoeq_rec _ _ oE _).funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
{h : FreeGroup (gp_generators P) $-> H &
h $o FreeGroup_rec (gp_relators P) $==
h $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)}
  srefine (equiv_functor_sigma_pb _ oE _).funext: Funext
G: Group
P: HasPresentation G
H: Group
Type
funext: Funext
G: Group
P: HasPresentation G
H: Group
?A <~> (FreeGroup (gp_generators P) $-> H)
funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
{x : _ &
((fun h : FreeGroup (gp_generators P) $-> H =>
  h $o FreeGroup_rec (gp_relators P) $==
  h $o
  FreeGroup_rec (fun _ : gp_rel_index P => group_unit))
 o ?f) x}
  2: apply equiv_freegroup_rec.funext: Funext
G: Group
P: HasPresentation G
H: Group
{f : gp_generators P -> H &
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit} <~>
{x : _ &
((fun h : FreeGroup (gp_generators P) $-> H =>
  h $o FreeGroup_rec (gp_relators P) $==
  h $o
  FreeGroup_rec (fun _ : gp_rel_index P => group_unit))
 o equiv_freegroup_rec H (gp_generators P)) x}
  apply equiv_functor_sigma_id.funext: Funext
G: Group
P: HasPresentation G
H: Group
forall a : gp_generators P -> H,
(forall r : gp_rel_index P,
 FreeGroup_rec a (gp_relators P r) = group_unit) <~>
equiv_freegroup_rec H (gp_generators P) a $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) a $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)
  intros f.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec f (gp_relators P r) = group_unit) <~>
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)
  srapply equiv_iff_hprop.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec f (gp_relators P r) = group_unit) ->
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)
funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit) ->
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit
  {funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
(forall r : gp_rel_index P,
 FreeGroup_rec f (gp_relators P r) = group_unit) ->
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit) intros p.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)
    change (equiv_freegroup_rec H _ f $o FreeGroup_rec (gp_relators P)
      $== equiv_freegroup_rec _ _ f $o FreeGroup_rec (fun _ => group_unit)).funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit)
    rapply FreeGroup_ind_homotopy.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit
forall x : gp_rel_index P,
(equiv_freegroup_rec H (gp_generators P) f $o
 FreeGroup_rec (gp_relators P)) (freegroup_in x) =
(equiv_freegroup_rec H (gp_generators P) f $o
 FreeGroup_rec (fun _ : gp_rel_index P => group_unit))
  (freegroup_in x)
    exact p. }funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (fun _ : gp_rel_index P => group_unit) ->
forall r : gp_rel_index P,
FreeGroup_rec f (gp_relators P r) = group_unit
  intros p r.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec (gp_relators P) $==
equiv_freegroup_rec H (gp_generators P) f $o
FreeGroup_rec
  (fun _ : gp_rel_index P => group_unit)
r: gp_rel_index P
FreeGroup_rec f (gp_relators P r) = group_unit
  hnf in p.funext: Funext
G: Group
P: HasPresentation G
H: Group
f: gp_generators P -> H
p: forall x : FreeGroup (gp_rel_index P),
(equiv_freegroup_rec H (gp_generators P) f $o
 FreeGroup_rec (gp_relators P)) x =
(equiv_freegroup_rec H (gp_generators P) f $o
 FreeGroup_rec
   (fun _ : gp_rel_index P => group_unit)) x
r: gp_rel_index P
FreeGroup_rec f (gp_relators P r) = group_unit
  exact (p (freegroup_in r)).
Defined.

(** ** Constructors for finite presentations *)

Definition Build_Finite_GroupPresentation n m
  (f : FinSeq m (FreeGroup (Fin n)))
  : GroupPresentation.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
Proof.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
  snapply Build_GroupPresentation.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
?gp_rel_index -> FreeGroup ?gp_generators
  -n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type exact (Fin n).
  -n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Type exact (Fin m).
  -n, m: nat
f: FinSeq m (FreeGroup (Fin n))
Fin m -> FreeGroup (Fin n) exact f.
Defined.

Instance FinitelyGeneratedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyGeneratedPresentation (Build_Finite_GroupPresentation n m f).n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
  (Build_Finite_GroupPresentation n m f)
Proof.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
  (Build_Finite_GroupPresentation n m f)
  unshelve econstructor.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
merely
  (gp_generators
     (Build_Finite_GroupPresentation n m f) <~>
   Fin ?fcard)
  2: simpl; apply tr; reflexivity.
Defined.

Instance FinitelyRelatedPresentation_Build_Finite_GroupPresentation
  {n m f}
  : FinitelyRelatedPresentation (Build_Finite_GroupPresentation n m f).n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
  (Build_Finite_GroupPresentation n m f)
Proof.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
  (Build_Finite_GroupPresentation n m f)
  unshelve econstructor.n, m: nat
f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat
f: FinSeq m (FreeGroup (Fin n))
merely
  (gp_rel_index (Build_Finite_GroupPresentation n m f) <~>
   Fin ?fcard)
  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).