Require Import Basics Types WildCat.Core Truncations.Core
  AbelianGroup AbHom Centralizer AbProjective
  Groups.FreeGroup AbGroups.Z Int.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * Cyclic groups *)

(** ** 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 [Z] 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@{u}} (g : G) : Z1 $-> G
  := FreeGroup_rec Unit G (unit_name g).

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

(** The free group [Z] on one generator is isomorphic to the subgroup of [Z] generated by the generator.  And such cyclic subgroups are known to be commutative, by [commutative_cyclic_subgroup]. *)
Global 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
  snrapply 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) refine (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_eta
        (FreeGroup.word_sing Unit (inl tt))))
  (g
     (freegroup_eta
        (FreeGroup.word_sing Unit (inl tt)))) =
sg_op
  (f
     (freegroup_eta
        (FreeGroup.word_sing Unit (inl tt))))
  (g
     (freegroup_eta
        (FreeGroup.word_sing Unit (inl 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_nat n a.
A: AbGroup
a: A
n: nat
Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a
Proof.
A: AbGroup
a: A
n: nat
Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a
  induction n as [|n H].
A: AbGroup
a: A
Z1_rec a (nat_to_Z1 0) = ab_mul_nat 0 a
A: AbGroup
a: A
n: nat
H: Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a
Z1_rec a (nat_to_Z1 n.+1) = ab_mul_nat n.+1 a
  1: easy.
A: AbGroup
a: A
n: nat
H: Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a
Z1_rec a (nat_to_Z1 n.+1) = ab_mul_nat n.+1 a
  refine (grp_pow_homo _ _ _ @ _); simpl.
A: AbGroup
a: A
n: nat
H: Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a
sg_op (sg_op a mon_unit)
  (grp_pow (sg_op a mon_unit) n) =
sg_op a (grp_pow a n)
  by rewrite grp_unit_r.
Defined.

(** [ab_Z1] is projective. *)
Global 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_eta (FreeGroup.word_sing Unit (inl x)))) ==
(fun x : Unit =>
 f (freegroup_eta (FreeGroup.word_sing Unit (inl 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 (sg_op a.1 mon_unit)) ==
(fun x : Unit =>
 f (freegroup_eta (FreeGroup.word_sing Unit (inl 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 (sg_op a.1 mon_unit) =
f (freegroup_eta (FreeGroup.word_sing Unit (inl tt)))
  refine (_ @ a.2).
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 (sg_op a.1 mon_unit) = p a.1
  exact (ap p (grp_unit_r _)).
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. *)

(** * Finite cyclic groups *)

(** The [n]-th cyclic group is the cokernel of [Z1_mul_nat n]. *)
Definition cyclic@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u}
  := ab_cokernel@{u v} (Z1_mul_nat n).