Timings for FreeAbelianGroup.v

Require Import Basics.Overture Basics.Tactics Basics.Equivalences.

Require Import Types.Sigma Types.Forall Types.Paths.

Require Import WildCat.Core WildCat.EquivGpd WildCat.Universe.

Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization.

Require Import Algebra.Groups.FreeGroup.

Require Import Spaces.List.Core.

(** * Free Abelian Groups *)

Definition FactorsThroughFreeAbGroup (S : Type) (F_S : AbGroup)
  (i : S -> F_S) (A : AbGroup) (g : S -> A) : Type
  := {f : F_S $-> A & f o i == g}.

(** Universal property of a free abelian group on a set (type). *)

Class IsFreeAbGroupOn (S : Type) (F_S : AbGroup) (i : S -> F_S)
  := contr_isfreeabgroupon :: forall (A : AbGroup) (g : S -> A),
      Contr (FactorsThroughFreeAbGroup S F_S i A g).

(** A abelian group is free if there exists a generating type on which it is a free group (a basis). *)

Class IsFreeAbGroup (F_S : AbGroup)
  := isfreegroup : {S : _ & {i : _ & IsFreeAbGroupOn S F_S i}}.

Instance isfreeabgroup_isfreeabgroupon (S : Type) (F_S : AbGroup) (i : S -> F_S)
  {H : IsFreeAbGroupOn S F_S i}
  : IsFreeAbGroup F_S
  := (S; i; H).

(** The abelianization of the free group on a set is the free abelian group. *)

Definition FreeAbGroup (S : Type) : AbGroup
  := abel (FreeGroup S).

Arguments FreeAbGroup S : simpl never.

Definition freeabgroup_in {S : Type} : S -> FreeAbGroup S
  := abel_unit o freegroup_in.

Definition FreeAbGroup_rec {S : Type} {A : AbGroup} (f : S -> A)
  : FreeAbGroup S $-> A
  := grp_homo_abel_rec (FreeGroup_rec f).

Definition FreeAbGroup_rec_beta_in {S : Type} {A : AbGroup} (f : S -> A)
  : FreeAbGroup_rec f o freeabgroup_in == f
  := fun _ => idpath.

Definition FreeAbGroup_ind_homotopy {X : Type} {A : AbGroup}
  {f f' : FreeAbGroup X $-> A}
  (p : forall x, f (freeabgroup_in x) = f' (freeabgroup_in x))
  : f $== f'.

Proof.

  snapply abel_ind_homotopy.

  snapply FreeGroup_ind_homotopy.

  snapply p.

Defined.

(** The abelianization of a free group on a set is a free abelian group on that set. *)

Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext}
  {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A)
  {H1 : IsAbelianization A g} {H2 : IsFreeGroupOn S G f}
  : IsFreeAbGroupOn S A (g o f).

Proof.

  unfold IsFreeAbGroupOn.

  intros B h.

  specialize (H2 B h).

  revert H2.

  unfold FactorsThroughFreeGroup, FactorsThroughFreeAbGroup.

  snapply contr_equiv'.

  symmetry.

  exact (equiv_functor_sigma_pb (equiv_group_precomp_isabelianization g B)).

Defined.

(** As a special case, the free abelian group is a free abelian group. *)

Instance isfreeabgroup_freeabgroup `{Funext} (S : Type)
  : IsFreeAbGroup (FreeAbGroup S).

Proof.

  exists S, freeabgroup_in.

  srapply isfreeabgroupon_isabelianization_isfreegroup.

Defined.

(** Functoriality follows from the functoriality of [abel] and [FreeGroup]. *)

Instance is0functor_freeabgroup : Is0Functor FreeAbGroup := _.

Instance is1functor_freeabgroup : Is1Functor FreeAbGroup := _.