Timings for FreeGroup.v
Require Import Basics Types Group Subgroup
WildCat.Core WildCat.Universe Colimits.Coeq
Truncations.Core Truncations.SeparatedTrunc
Spaces.List.Core Spaces.List.Theory.
Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.
(** [IsFreeGroup] is defined in Group.v. In this file we construct free groups and and prove properties about them. *)
(** We construct the free group on a type [A] as a higher inductive type. This construction is due to Kraus-Altenkirch 2018 arXiv:1805.02069. Their construction is actually more general, but we set-truncate it to suit our needs which is the free group as a set. This is a very simple HIT in a similar manner to the abelianization HIT used in Algebra.AbGroup.Abelianization. *)
Local Open Scope list_scope.
(** We define words (with inverses) on A to be lists of marked elements of A *)
Local Definition Words : Type@{u} := list (A + A).
(** Given a marked element of A we can change its mark *)
Local Definition change_sign : A + A -> A + A := equiv_sum_symm A A.
(** We introduce a local notation for [change_sign]. It is only defined in this section however. *)
Local Notation "a ^'" := (change_sign a) (at level 1).
(** Changing sign is an involution *)
Local Definition change_sign_inv a : a^'^' = a.
(** Now we wish to define the free group on A as the following HIT:
HIT N(A) : hSet
| eta : Words -> N(A)
| tau (x : Words) (a : A + A) (y : Words)
: eta (x ++ [a] ++ [a^] ++ y) = eta (x ++ y).
Since we cannot write our HITs directly like this (without resorting to private inductive types), we will construct this HIT out of HITs we know. In fact, we can define N(A) as a coequalizer. *)
Local Definition map1 : Words * (A + A) * Words -> Words.
exact (x ++ [a] ++ [a^'] ++ y).
Local Definition map2 : Words * (A + A) * Words -> Words.
(** Now we can define the underlying type of the free group as the 0-truncated coequalizer of these two maps *)
Definition freegroup_type : Type := Tr 0 (Coeq map1 map2).
(** This is the point constructor *)
Definition freegroup_eta : Words -> freegroup_type := tr o coeq.
(** This is the path constructor *)
Definition freegroup_tau (x : Words) (a : A + A) (y : Words)
: freegroup_eta (x ++ [a] ++ [a^'] ++ y) = freegroup_eta (x ++ y).
exact ((cglue (x, a, y))).
(** The group operation *)
#[export] Instance sgop_freegroup : SgOp freegroup_type.
revert x; snapply Coeq_rec.
exact (freegroup_eta (x ++ y)).
change (freegroup_eta (x ++ y ++ ([a] ++ [a^'] ++ z))
= freegroup_eta (x ++ y ++ z)).
napply (freegroup_tau _ a).
change (freegroup_eta ((c ++ [b] ++ [b^'] ++ d) ++ a)
= freegroup_eta ((c ++ d) ++ a)).
lhs_V napply (ap (fun x => freegroup_eta (c ++ x))).
lhs_V napply (ap (fun x => freegroup_eta (c ++ _ ++ x))).
(** The unit of the free group is the empty word *)
#[export] Instance monunit_freegroup_type : MonUnit freegroup_type
:= freegroup_eta nil.
(** We can change the sign of all the elements in a word and reverse the order. This will be the inversion in the group *)
Definition word_change_sign (x : Words) : Words
:= reverse (list_map change_sign x).
(** Changing the sign changes the order of word concatenation *)
Definition word_change_sign_ww (x y : Words)
: word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x.
(** This is also involutive *)
Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x.
lhs_V napply list_map_reverse.
1: napply reverse_reverse.
lhs_V napply list_map_compose.
(** Changing the sign gives us left inverses *)
Lemma word_concat_Vw x : freegroup_eta (word_change_sign x ++ x) = mon_unit.
lhs napply (ap (fun x => freegroup_eta (x ++ _))).
change (freegroup_eta ((word_change_sign x ++ [a^']) ++ [a] ++ x)
= mon_unit).
rewrite <- (change_sign_inv a).
lhs napply freegroup_tau.
(** And since changing the sign is involutive we get right inverses from left inverses *)
Lemma word_concat_wV x : freegroup_eta (x ++ word_change_sign x) = mon_unit.
set (x' := word_change_sign x).
rewrite <- (word_change_sign_inv x).
change (freegroup_eta (word_change_sign x' ++ x') = mon_unit).
(** Inverses are defined by changing the order of a word that appears in eta. Most of the work here is checking that it is agreeable with the path constructor. *)
#[export] Instance inverse_freegroup_type : Inverse freegroup_type.
revert x; srapply Coeq_rec.
exact (word_change_sign x).
lhs napply word_change_sign_ww.
napply (ap (fun x => x ++ _)).
lhs napply word_change_sign_ww.
napply (ap (fun x => x ++ _)).
lhs napply word_change_sign_ww.
napply (ap (fun x => _ ++ x)).
exact (word_change_sign_inv [a]).
1: rhs_V napply app_assoc.
2: napply word_change_sign_ww.
(** Now we can start to prove the group laws. Since these are hprops we can ignore what happens with the path constructor. *)
(** Our operation is associative *)
#[export] Instance associative_freegroup_type : Associative sg_op.
revert x; srapply Coeq_ind_hprop; intro x.
revert y; srapply Coeq_ind_hprop; intro y.
revert z; srapply Coeq_ind_hprop; intro z.
#[export] Instance leftidentity_freegroup_type : LeftIdentity sg_op mon_unit.
srapply Coeq_ind_hprop; intros x.
#[export] Instance rightidentity_freegroup_type : RightIdentity sg_op mon_unit.
srapply Coeq_ind_hprop; intros x.
#[export] Instance leftinverse_freegroup_type : LeftInverse (.*.) (^) mon_unit.
srapply Coeq_ind_hprop; intro x.
#[export] Instance rightinverse_freegroup_type : RightInverse (.*.) (^) mon_unit.
srapply Coeq_ind_hprop; intro x.
(** Finally we have defined the free group on [A] *)
Definition FreeGroup : Group.
snapply (Build_Group freegroup_type); repeat split; exact _.
Definition word_rec (G : Group) (s : A -> G) : A + A -> G.
(** When we have a list of words we can recursively define a group element. The obvious choice would be to map [nil] to the identity and [x :: xs] to [x * words_rec xs]. This has the disadvantage that a single generating element gets mapped to [x * 1] instead of [x]. To fix this issue, we map [nil] to the identity, the singleton to the element we want, and do the rest recursively. *)
Definition words_rec (G : Group) (s : A -> G) : Words -> G.
induction xs as [|x [|y xs] IHxs].
exact (word_rec G s x * IHxs).
Definition words_rec_cons (G : Group) (s : A -> G) (x : A + A) (xs : Words)
: words_rec G s (x :: xs)%list = word_rec G s x * words_rec G s xs.
symmetry; napply grp_unit_r.
Lemma words_rec_pp (G : Group) (s : A -> G) (x y : Words)
: words_rec G s (x ++ y) = words_rec G s x * words_rec G s y.
induction x as [|x xs IHxs] in y |- *.
symmetry; napply grp_unit_l.
change ((?x :: ?xs) ++ y) with (x :: xs ++ y).
lhs napply words_rec_cons.
Lemma words_rec_coh (G : Group) (s : A -> G) (a : A + A) (b c : Words)
: words_rec G s (map1 (b, a, c)) = words_rec G s (map2 (b, a, c)).
rhs napply (words_rec_pp G s).
(** Given a group [G] we can construct a group homomorphism [FreeGroup A $-> G] if we have a map [A -> G]. *)
Definition FreeGroup_rec {G : Group} (s : A -> G) : FreeGroup $-> G.
snapply Build_GroupHomomorphism.
intros x y; strip_truncations.
revert x; srapply Coeq_ind_hprop; intro x.
revert y; srapply Coeq_ind_hprop; intro y.
Definition freegroup_in : A -> FreeGroup
:= freegroup_eta o (fun x => [ x ]) o inl.
Definition FreeGroup_rec_beta {G : Group} (f : A -> G)
: FreeGroup_rec f o freegroup_in == f
:= fun _ => idpath.
Coercion freegroup_in : A >-> group_type.
Definition FreeGroup_ind_hprop' (P : FreeGroup -> Type)
`{forall x, IsHProp (P x)}
(H1 : forall w, P (freegroup_eta w))
: forall x, P x.
Definition FreeGroup_ind_hprop (P : FreeGroup -> Type)
`{forall x, IsHProp (P x)}
(H1 : P mon_unit)
(Hin : forall x, P (freegroup_in x))
(Hop : forall x y, P x -> P y -> P (x^ * y))
: forall x, P x.
rapply FreeGroup_ind_hprop'.
induction w as [|a w IHw].
change (P ((freegroup_in a) * freegroup_eta w)).
rewrite <- (grp_inv_inv a).
change (P ((freegroup_in a)^ * freegroup_eta w)).
Definition FreeGroup_ind_homotopy {G : Group} {f f' : FreeGroup $-> G}
(H : forall x, f (freegroup_in x) = f' (freegroup_in x))
: f $== f'.
rapply FreeGroup_ind_hprop.
exact (concat (grp_homo_unit f) (grp_homo_unit f')^).
refine (grp_homo_op_agree f f' _ q).
(** Now we need to prove that the free group satisfies the universal property of the free group. *)
(** TODO: remove funext from here and universal property of free group *)
#[export] Instance isfreegroupon_freegroup `{Funext}
: IsFreeGroupOn A FreeGroup freegroup_in.
1: apply FreeGroup_rec, f.
napply path_sigma_hprop; [ exact _ |].
apply equiv_path_grouphomomorphism.
snapply FreeGroup_ind_homotopy.
(** Typeclass search can already find this but we leave it here as a definition for reference. *)
Definition isfreegroup_freegroup `{Funext} : IsFreeGroup FreeGroup := _.
Arguments FreeGroup_rec {A G}.
Arguments FreeGroup_ind_homotopy {A G f f'}.
Arguments freegroup_eta {A}.
Arguments freegroup_in {A}.
(** Properties of free groups *)
(* Given a function on the generators, there is an induced group homomorphism from the free group. *)
Definition isfreegroupon_rec {S : Type} {F_S : Group}
{i : S -> F_S} `{IsFreeGroupOn S F_S i}
{G : Group} (f : S -> G) : F_S $-> G
:= (center (FactorsThroughFreeGroup S F_S i G f)).1.
(* The propositional computation rule for the recursor. *)
Definition isfreegroupon_rec_beta
{S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}
{G : Group} (f : S -> G)
: isfreegroupon_rec f o i == f
:= (center (FactorsThroughFreeGroup S F_S i G f)).2.
(* Two homomorphisms from a free group are equal if they agree on the generators. *)
Definition path_homomorphism_from_free_group {S : Type}
{F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}
{G : Group} (f g : F_S $-> G) (K : f o i == g o i)
: f = g.
(* By assumption, the type [FactorsThroughFreeGroup S F_S i G (g o i)] of factorizations of [g o i] through [i] is contractible. Therefore the two elements we have are equal. Therefore, their first components are equal. *)
exact (path_contr (f; K) (g; fun x => idpath))..1.
Instance isequiv_isfreegroupon_rec `{Funext} {S : Type}
{F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i} {G : Group}
: IsEquiv (@isfreegroupon_rec S F_S i _ G).
apply (isequiv_adjointify isfreegroupon_rec (fun f => f o i)).
apply path_homomorphism_from_free_group.
apply isfreegroupon_rec_beta.
(* here we need [Funext]: *)
apply path_arrow, isfreegroupon_rec_beta.
(** The universal property of a free group. *)
Definition equiv_isfreegroupon_rec `{Funext} {G F : Group} {A : Type}
{i : A -> F} `{IsFreeGroupOn A F i}
: (A -> G) <~> (F $-> G) := Build_Equiv _ _ isfreegroupon_rec _.
(** The above theorem is true regardless of the implementation of free groups. This lets us state the more specific theorem about the canonical free groups. This can be read as [FreeGroup] is left adjoint to the forgetful functor [group_type]. *)
Definition equiv_freegroup_rec `{Funext} (G : Group) (A : Type)
: (A -> G) <~> (FreeGroup A $-> G)
:= equiv_isfreegroupon_rec.
Instance ishprop_isfreegroupon `{Funext} (F : Group) (A : Type) (i : A -> F)
: IsHProp (IsFreeGroupOn A F i).
(** Both ways of stating the universal property are equivalent. *)
Definition equiv_isfreegroupon_isequiv_precomp `{Funext}
(F : Group) (A : Type) (i : A -> F)
: IsFreeGroupOn A F i <~> forall G, IsEquiv (fun f : F $-> G => f o i).
1: intros ? ?; exact (equiv_isequiv (equiv_isfreegroupon_rec)^-1).
1: exact (hfiber (fun f x => grp_homo_map f (i x)) g).
rapply equiv_functor_sigma_id.
(** ** Subgroups of free groups *)
(* We say that a group [G] is generated by a subtype [X] if the natural map from the subgroup generated by [X] to [G] is a surjection. One could equivalently say [IsEquiv (subgroup_incl (subgroup_generated X))], [forall g, subgroup_generated X g], or [subgroup_generated X = maximal_subgroup], but the definition using surjectivity is convenient later. *)
Definition isgeneratedby (G : Group) (X : G -> Type)
:= IsSurjection (subgroup_incl (subgroup_generated X)).
Section FreeGroupGenerated.
(* In this Section, we prove that the free group [F_S] on a type [S] is generated in the above sense by the image of [S]. We conclude that the inclusion map is an equivalence, and that the free group is isomorphic as a group to the subgroup. We show that the inclusion is a surjection by showing that it is split epi in the category of groups. *)
Context {S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i}.
(* We define a group homomorphism from [F_S] to the subgroup [G] generated by [S] by sending a generator [s] to "itself". This map will be a section of the inclusion map. *)
Local Definition to_subgroup_generated
: F_S $-> subgroup_generated (hfiber i).
snapply subgroup_generated_gen_incl.
(* We record the computation rule that [to_subgroup_generated] satisfies. *)
Local Definition to_subgroup_generated_beta (s : S)
: to_subgroup_generated (i s) = subgroup_generated_gen_incl (i s) (s; idpath)
:= isfreegroupon_rec_beta _ _.
(* It follows that [to_subgroup_generated] is a section of the inclusion map from [G] to [F_S]. *)
Local Definition is_retraction
: (subgroup_incl _) $o to_subgroup_generated = grp_homo_id.
apply path_homomorphism_from_free_group; cbn.
exact (ap pr1 (to_subgroup_generated_beta s)).
(* It follows that the inclusion map is a surjection, i.e., that [F_S] is generated by the image of [S]. *)
Definition isgenerated_isfreegroupon
: isgeneratedby F_S (hfiber i).
exact to_subgroup_generated.
exact (ap grp_homo_map is_retraction).
(* Therefore, the inclusion map is an equivalence, since it is known to be an embedding. *)
Definition isequiv_subgroup_incl_freegroupon
: IsEquiv (subgroup_incl (subgroup_generated (hfiber i))).
exact isgenerated_isfreegroupon.
(* Therefore, the subgroup is isomorphic to the free group. *)
Definition iso_subgroup_incl_freegroupon
: GroupIsomorphism (subgroup_generated (hfiber i)) F_S.
napply Build_GroupIsomorphism.
exact isequiv_subgroup_incl_freegroupon.
(** ** Properties of recursor *)
Definition freegroup_rec_in {A : Type}
: FreeGroup_rec freegroup_in $== Id (FreeGroup A).
by snapply FreeGroup_ind_homotopy.
Definition freegroup_rec_compose {A : Type} {G H : Group}
(f : A -> G) (k : G $-> H)
: FreeGroup_rec (k o f) $== k $o FreeGroup_rec f.
by snapply FreeGroup_ind_homotopy; intros x.
Definition freegroup_const {A : Type} {G : Group}
: FreeGroup_rec (fun _ : A => 1) $== @grp_homo_const _ G.
by snapply FreeGroup_ind_homotopy.
Instance is0functor_freegroup : Is0Functor FreeGroup.
snapply Build_Is0Functor.
exact (freegroup_in o f).
Instance is1functor_freegroup : Is1Functor FreeGroup.
snapply Build_Is1Functor.
snapply FreeGroup_ind_homotopy.
exact (ap freegroup_in (p x)).
intro; exact freegroup_rec_in.
by snapply FreeGroup_ind_homotopy.