From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Spaces.Pos.Core Spaces.Int.
Require Import Algebra.AbGroups.AbelianGroup.

Local Set Universe Minimization ToSet.

Local Open Scope int_scope.
Local Open Scope mc_add_scope.

(** * The group of integers *)

(** See also Cyclic.v for a definition of the integers as the free group on one generator. *)

Definition abgroup_Z@{} : AbGroup@{Set}.
AbGroup
Proof.
AbGroup
  snapply Build_AbGroup'.
Type0
MonUnit ?G
Inverse ?G
SgOp ?G
IsHSet ?G
Commutative sg_op
Associative sg_op
LeftIdentity sg_op 0
LeftInverse sg_op inv 0
  -
Type0 exact Int.
  -
MonUnit Int exact 0%int.
  -
Inverse Int exact int_neg.
  -
SgOp Int exact int_add.
  -
IsHSet Int exact _.
  -
Commutative sg_op exact int_add_comm.
  -
Associative sg_op exact int_add_assoc.
  -
LeftIdentity sg_op 0 exact int_add_0_l.
  -
LeftInverse sg_op inv 0 exact int_add_neg_l.
Defined.

(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism.  See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *)
Definition grp_pow_homo {G : Group} (g : G)
  : GroupHomomorphism abgroup_Z G.
G: Group
g: G
GroupHomomorphism abgroup_Z G
Proof.
G: Group
g: G
GroupHomomorphism abgroup_Z G
  snapply Build_GroupHomomorphism.
G: Group
g: G
abgroup_Z -> G
G: Group
g: G
IsSemiGroupPreserving ?grp_homo_map
  1: exact (grp_pow g).
G: Group
g: G
IsSemiGroupPreserving (grp_pow g)
  intros m n; apply grp_pow_add.
Defined.

(** [ab_mul] (and [grp_pow]) give multiplication in [abgroup_Z]. *)
Definition abgroup_Z_ab_mul (z z' : Int)
  : ab_mul (A:=abgroup_Z) z z' = z * z'.
z, z': Int
ab_mul z z' = z * z'
Proof.
z, z': Int
ab_mul z z' = z * z'
  revert z.
z': Int
forall z : Int, ab_mul z z' = z * z'
  rapply (int_homotopic (fun x => int_add x z')); cbn beta.
z': Int
ab_mul 0 z' = 0 * z'
z': Int
(fun x : Int => ab_mul x.+1 z') == (fun x : Int => (ab_mul x z' + z')%int)
z': Int
(fun x : Int => x.+1 * z') == (fun x : Int => (x * z' + z')%int)
  1,3: reflexivity.
z': Int
(fun x : Int => ab_mul x.+1 z') == (fun x : Int => (ab_mul x z' + z')%int)
  -
z': Int
(fun x : Int => ab_mul x.+1 z') == (fun x : Int => (ab_mul x z' + z')%int) intro z.
z', z: Int
ab_mul z.+1 z' = (ab_mul z z' + z')%int
    lhs napply (grp_pow_succ (G:=abgroup_Z)).
z', z: Int
z' + grp_pow z' z = (ab_mul z z' + z')%int
    by rewrite int_add_comm.
Defined.