Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Pos.Core Spaces.Int.
Require Import Algebra.AbGroups.AbelianGroup.

(** * The group of integers *)

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

Local Open Scope int_scope.

Section MinimizationToSet.

Local Set Universe Minimization ToSet.

Definition abgroup_Z@{} : AbGroup@{Set}.
AbGroup
Proof.
AbGroup
  snrapply Build_AbGroup.
Group
Commutative group_sgop
  -
Group refine (Build_Group Int int_add 0 int_negation _); repeat split.
IsHSet Int
Associative sg_op
RightIdentity sg_op mon_unit
LeftInverse sg_op negate mon_unit
RightInverse sg_op negate mon_unit
    +
IsHSet Int exact _.
    +
Associative sg_op exact int_add_assoc.
    +
RightIdentity sg_op mon_unit exact int_add_0_r.
    +
LeftInverse sg_op negate mon_unit exact int_add_negation_l.
    +
RightInverse sg_op negate mon_unit exact int_add_negation_r.
  -
Commutative group_sgop exact int_add_comm.
Defined.

End MinimizationToSet.

(** We can multiply by [n : Int] in any abelian group. *)
Definition ab_mul (n : Int) {A : AbGroup} : GroupHomomorphism A A.
n: Int
A: AbGroup
GroupHomomorphism A A
Proof.
n: Int
A: AbGroup
GroupHomomorphism A A
  induction n.
p: Pos
A: AbGroup
GroupHomomorphism A A
A: AbGroup
GroupHomomorphism A A
p: Pos
A: AbGroup
GroupHomomorphism A A
  -
p: Pos
A: AbGroup
GroupHomomorphism A A exact (grp_homo_compose ab_homo_negation (ab_mul_nat (pos_to_nat p))).
  -
A: AbGroup
GroupHomomorphism A A exact grp_homo_const.
  -
p: Pos
A: AbGroup
GroupHomomorphism A A exact (ab_mul_nat (pos_to_nat p)).
Defined.

(** Homomorphisms respect multiplication. *)
Lemma ab_mul_homo {A B : AbGroup} (n : Int) (f : GroupHomomorphism A B)
  : grp_homo_compose f (ab_mul n) == grp_homo_compose (ab_mul n) f.
A, B: AbGroup
n: Int
f: GroupHomomorphism A B
grp_homo_compose f (ab_mul n) ==
grp_homo_compose (ab_mul n) f
Proof.
A, B: AbGroup
n: Int
f: GroupHomomorphism A B
grp_homo_compose f (ab_mul n) ==
grp_homo_compose (ab_mul n) f
  intro x.
A, B: AbGroup
n: Int
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul n) x =
grp_homo_compose (ab_mul n) f x
  induction n.
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul (neg p)) x =
grp_homo_compose (ab_mul (neg p)) f x
A, B: AbGroup
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul 0) x =
grp_homo_compose (ab_mul 0) f x
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul (pos p)) x =
grp_homo_compose (ab_mul (pos p)) f x
  -
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul (neg p)) x =
grp_homo_compose (ab_mul (neg p)) f x cbn.
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
f (negate (grp_pow x (pos_to_nat p))) =
negate (grp_pow (f x) (pos_to_nat p)) refine (grp_homo_inv _ _ @ _).
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
negate (f (grp_pow x (pos_to_nat p))) =
negate (grp_pow (f x) (pos_to_nat p))
    refine (ap negate _).
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
f (grp_pow x (pos_to_nat p)) =
grp_pow (f x) (pos_to_nat p)
    apply grp_pow_homo.
  -
A, B: AbGroup
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul 0) x =
grp_homo_compose (ab_mul 0) f x cbn.
A, B: AbGroup
f: GroupHomomorphism A B
x: A
f group_unit = group_unit apply grp_homo_unit.
  -
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
grp_homo_compose f (ab_mul (pos p)) x =
grp_homo_compose (ab_mul (pos p)) f x cbn.
A, B: AbGroup
p: Pos
f: GroupHomomorphism A B
x: A
f (grp_pow x (pos_to_nat p)) =
grp_pow (f x) (pos_to_nat p) apply grp_pow_homo.
Defined.

(** Multiplication by zero gives the constant group homomorphism. *)
Definition ab_mul_const `{Funext} {A : AbGroup} : ab_mul 0 (A:=A) = grp_homo_const.
H: Funext
A: AbGroup
ab_mul 0 = grp_homo_const
Proof.
H: Funext
A: AbGroup
ab_mul 0 = grp_homo_const
  apply equiv_path_grouphomomorphism.
H: Funext
A: AbGroup
ab_mul 0 == grp_homo_const
  reflexivity.
Defined.