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'
  induction z.
z': Int
ab_mul 0 z' = 0 * z'
n: nat
z': Int
IHz: ab_mul n z' = n * z'
ab_mul n.+1 z' = n.+1 * z'
n: nat
z': Int
IHz: ab_mul (- n)%int z' = (- n)%int * z'
ab_mul (- n)%int.-1 z' = (- n)%int.-1 * z'
  -
z': Int
ab_mul 0 z' = 0 * z' reflexivity.
  -
n: nat
z': Int
IHz: ab_mul n z' = n * z'
ab_mul n.+1 z' = n.+1 * z' cbn.
n: nat
z': Int
IHz: ab_mul n z' = n * z'
grp_pow z' n.+1 = n.+1 * z'
    lhs napply (grp_pow_succ (G:=abgroup_Z)).
n: nat
z': Int
IHz: ab_mul n z' = n * z'
z' + grp_pow z' n = n.+1 * z'
    rhs napply int_mul_succ_l.
n: nat
z': Int
IHz: ab_mul n z' = n * z'
z' + grp_pow z' n = (z' + n * z')%int
    f_ap.
  -
n: nat
z': Int
IHz: ab_mul (- n)%int z' = (- n)%int * z'
ab_mul (- n)%int.-1 z' = (- n)%int.-1 * z' cbn.
n: nat
z': Int
IHz: ab_mul (- n)%int z' = (- n)%int * z'
grp_pow z' (- n)%int.-1 = (- n)%int.-1 * z'
    lhs napply (grp_pow_pred (G:=abgroup_Z)).
n: nat
z': Int
IHz: ab_mul (- n)%int z' = (- n)%int * z'
- z' + grp_pow z' (- n)%int = (- n)%int.-1 * z'
    rhs napply int_mul_pred_l.
n: nat
z': Int
IHz: ab_mul (- n)%int z' = (- n)%int * z'
- z' + grp_pow z' (- n)%int = (- z' + - n * z')%int
    f_ap.
Defined.