From HoTT Require Import Basics Types WildCat.Core Truncations.Core Spaces.IntFrom HoTT Require Import Basics Types WildCat.Core Truncations.Core Spaces.Int
  AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z.

(** * The free group on one generator *)

(** We can define the integers as the free group on one generator, which we denote [Z1] below. Results from Centralizer.v and Groups.FreeGroup let us show that [Z1] is abelian. *)

(** We define [Z1] as the free group with a single generator. *)
Definition Z1 := FreeGroup Unit.
Definition Z1_gen : Z1 := freegroup_in tt. (* The generator *)

(** The recursion principle of [Z1] and its computation rule. *)
Definition Z1_rec {G : Group} (g : G) : Z1 $-> G
  := FreeGroup_rec (unit_name g).

Definition Z1_rec_beta {G : Group} (g : G) : Z1_rec g Z1_gen = g
  := FreeGroup_rec_beta _ _ _.

(** The free group [Z1] on one generator is isomorphic to the subgroup of [Z1] generated by the generator.  And such cyclic subgroups are known to be commutative, by [commutative_cyclic_subgroup]. *)
Instance Z1_commutative `{Funext} : Commutative (@group_sgop Z1)
  := commutative_iso_commutative iso_subgroup_incl_freegroupon.
(* TODO: [Funext] is used in [isfreegroupon_freegroup], but there is a comment there saying that it can be removed.  If that is done, can remove it from many results in this file. A different proof of this result, directly using the construction of the free group, could probably also avoid [Funext]. *)

Definition ab_Z1 `{Funext} : AbGroup
  := Build_AbGroup Z1 _.

(** The universal property of [ab_Z1]. *)
Lemma equiv_Z1_hom@{u v | u < v} `{Funext} (A : AbGroup@{u})
  : GroupIsomorphism (ab_hom@{u v} ab_Z1@{u v} A) A.
H: Funext
A: AbGroup
GroupIsomorphism (ab_hom ab_Z1 A) A
Proof.
H: Funext
A: AbGroup
GroupIsomorphism (ab_hom ab_Z1 A) A
  snapply Build_GroupIsomorphism'.
H: Funext
A: AbGroup
ab_hom ab_Z1 A <~> A
H: Funext
A: AbGroup
IsSemiGroupPreserving ?f
  -
H: Funext
A: AbGroup
ab_hom ab_Z1 A <~> A refine (_ oE (equiv_freegroup_rec@{u u u v} A Unit)^-1).
H: Funext
A: AbGroup
(Unit -> A) <~> A
    symmetry.
H: Funext
A: AbGroup
A <~> (Unit -> A) exact (Build_Equiv _ _ (fun a => unit_name a) _).
  -
H: Funext
A: AbGroup
IsSemiGroupPreserving
  ({|
     equiv_fun := fun a : A => unit_name a;
     equiv_isequiv := isequiv_unit_name A
   |}^-1 oE (equiv_freegroup_rec A Unit)^-1) intros f g.
H: Funext
A: AbGroup
f, g: ab_hom ab_Z1 A
({|
   equiv_fun := fun a : A => unit_name a;
   equiv_isequiv := isequiv_unit_name A
 |}^-1 oE (equiv_freegroup_rec A Unit)^-1) (sg_op f g) =
sg_op
  (({|
      equiv_fun := fun a : A => unit_name a;
      equiv_isequiv := isequiv_unit_name A
    |}^-1 oE (equiv_freegroup_rec A Unit)^-1) f)
  (({|
      equiv_fun := fun a : A => unit_name a;
      equiv_isequiv := isequiv_unit_name A
    |}^-1 oE (equiv_freegroup_rec A Unit)^-1) g) cbn.
H: Funext
A: AbGroup
f, g: ab_hom ab_Z1 A
sg_op (f (freegroup_in tt)) (g (freegroup_in tt)) =
sg_op (f (freegroup_in tt)) (g (freegroup_in tt)) reflexivity.
Defined.

Definition nat_to_Z1 : nat -> Z1
  := fun n => grp_pow Z1_gen n.

Definition Z1_mul_nat `{Funext} (n : nat) : ab_Z1 $-> ab_Z1
  := Z1_rec (nat_to_Z1 n).

Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
  : Z1_rec a (nat_to_Z1 n) = ab_mul n a.
A: AbGroup
a: A
n: nat
Z1_rec a (nat_to_Z1 n) = ab_mul n a
Proof.
A: AbGroup
a: A
n: nat
Z1_rec a (nat_to_Z1 n) = ab_mul n a
  induction n as [|n H].
A: AbGroup
a: A
Z1_rec a (nat_to_Z1 0) = ab_mul 0%nat a
A: AbGroup
a: A
n: nat
H: Z1_rec a (nat_to_Z1 n) = ab_mul n a
Z1_rec a (nat_to_Z1 n.+1) = ab_mul n.+1%nat a
  1: done.
A: AbGroup
a: A
n: nat
H: Z1_rec a (nat_to_Z1 n) = ab_mul n a
Z1_rec a (nat_to_Z1 n.+1) = ab_mul n.+1%nat a
  exact (grp_pow_natural _ _ _).
Defined.

(** [ab_Z1] is projective. *)
Instance ab_Z1_projective `{Funext}
  : IsAbProjective ab_Z1.
H: Funext
IsAbProjective ab_Z1
Proof.
H: Funext
IsAbProjective ab_Z1
  intros A B p f H1.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
merely {l : ab_Z1 $-> A & p $o l == f}
  pose proof (a := @center _ (H1 (f Z1_gen))).
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: Tr (-1) (hfiber p (f Z1_gen))
merely {l : ab_Z1 $-> A & p $o l == f}
  strip_truncations.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
merely {l : ab_Z1 $-> A & p $o l == f}
  snrefine (tr (Z1_rec a.1; _)).
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
(fun l : ab_Z1 $-> A => p $o l == f) (Z1_rec a.1)
  cbn beta.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
p $o Z1_rec a.1 == f apply ap10.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
p $o Z1_rec a.1 = f
  apply ap. (* of the coercion [grp_homo_map] *)
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
p $o Z1_rec a.1 = f
  apply path_homomorphism_from_free_group.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
(fun x : Unit => (p $o Z1_rec a.1) (freegroup_in x)) ==
(fun x : Unit => f (freegroup_in x))
  simpl.
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
unit_name (p a.1) == (fun x : Unit => f (freegroup_in x))
  intros [].
H: Funext
A, B: AbGroup
p: A $-> B
f: ab_Z1 $-> B
H1: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
a: hfiber p (f Z1_gen)
p a.1 = f (freegroup_in tt)
  exact a.2.
Defined.

(** The map sending the generator to [1 : Int]. *)
Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
  := Z1_rec (G:=abgroup_Z) 1%int.

(** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)