Require Import Basics.Overture Basics.Tactics Basics.Equivalences.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'.
X: Type
A: AbGroup
f, f': FreeAbGroup X $-> A
p: forall x : X, f (freeabgroup_in x) = f' (freeabgroup_in x)
f $== f'
Proof.
X: Type
A: AbGroup
f, f': FreeAbGroup X $-> A
p: forall x : X, f (freeabgroup_in x) = f' (freeabgroup_in x)
f $== f'
  snapply abel_ind_homotopy.
X: Type
A: AbGroup
f, f': FreeAbGroup X $-> A
p: forall x : X, f (freeabgroup_in x) = f' (freeabgroup_in x)
f $o abel_unit $== f' $o abel_unit
  snapply FreeGroup_ind_homotopy.
X: Type
A: AbGroup
f, f': FreeAbGroup X $-> A
p: forall x : X, f (freeabgroup_in x) = f' (freeabgroup_in x)
forall x : X,
(f $o abel_unit) (freegroup_in x) = (f' $o abel_unit) (freegroup_in x)
  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).
H: 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.
H: 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)
  unfold IsFreeAbGroupOn.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
H2: IsFreeGroupOn S G f
forall (A0 : AbGroup) (g0 : S -> A0),
Contr (FactorsThroughFreeAbGroup S A (fun x : S => g (f x)) A0 g0)
  intros B h.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
H2: IsFreeGroupOn S G f
B: AbGroup
h: S -> B
Contr (FactorsThroughFreeAbGroup S A (fun x : S => g (f x)) B h)
  specialize (H2 B h).
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
B: AbGroup
h: S -> B
H2: Contr (FactorsThroughFreeGroup S G f B h)
Contr (FactorsThroughFreeAbGroup S A (fun x : S => g (f x)) B h)
  revert H2.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
B: AbGroup
h: S -> B
Contr (FactorsThroughFreeGroup S G f B h) ->
Contr (FactorsThroughFreeAbGroup S A (fun x : S => g (f x)) B h)
  unfold FactorsThroughFreeGroup, FactorsThroughFreeAbGroup.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
B: AbGroup
h: S -> B
Contr {f0 : G $-> B & (fun x : S => f0 (f x)) == h} ->
Contr {f0 : A $-> B & (fun x : S => f0 (g (f x))) == h}
  snapply contr_equiv'.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
B: AbGroup
h: S -> B
{f0 : G $-> B & (fun x : S => f0 (f x)) == h} <~>
{f0 : A $-> B & (fun x : S => f0 (g (f x))) == h}
  symmetry.
H: Funext
S: Type
G: Group
A: AbGroup
f: S -> G
g: G $-> A
H1: IsAbelianization A g
B: AbGroup
h: S -> B
{f0 : A $-> B & (fun x : S => f0 (g (f x))) == h} <~>
{f0 : G $-> B & (fun x : S => f0 (f x)) == h}
  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).
H: Funext
S: Type
IsFreeAbGroup (FreeAbGroup S)
Proof.
H: Funext
S: Type
IsFreeAbGroup (FreeAbGroup S)
  exists S, freeabgroup_in.
H: Funext
S: Type
IsFreeAbGroupOn S (FreeAbGroup 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 := _.