Require Import Classes.interfaces.canonical_names.Require Import Classes.interfaces.canonical_names.
Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Z.
Require Import Algebra.Rings.CRing.
Require Import Spaces.Int.
Require Import WildCat.Core.

(** * In this file we define the ring [cring_Z] of integers with underlying abelian group [abgroup_Z] defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that [cring_Z] is initial. *)

(** The ring of integers *)
Definition cring_Z : CRing.
CRing
Proof.
CRing
  snapply Build_CRing'.
AbGroup
One ?R
Mult ?R
Commutative mult
Associative mult
LeftDistribute mult plus
LeftIdentity mult 1
  -
AbGroup exact abgroup_Z.
  -
One abgroup_Z exact 1%int.
  -
Mult abgroup_Z exact int_mul.
  -
Commutative mult exact int_mul_comm.
  -
Associative mult exact int_mul_assoc.
  -
LeftDistribute mult plus exact int_dist_l.
  -
LeftIdentity mult 1 exact int_mul_1_l.
Defined.

Local Open Scope mc_scope.

(** Given a ring element [r], we get a map [Int -> R] sending an integer to that multiple of [r]. *)
Definition rng_int_mult (R : Ring) := grp_pow_homo : R -> Int -> R.

(** Multiplying a ring element [r] by an integer [n] is equivalent to first multiplying the unit [1] of the ring by [n], and then multiplying the result by [r].  This is distributivity of right multiplication by [r] over the sum. *)
Definition rng_int_mult_dist_r {R : Ring} (r : R) (n : cring_Z)
  : rng_int_mult R r n = (rng_int_mult R 1 n) * r.
R: Ring
r: R
n: cring_Z
rng_int_mult R r n = rng_int_mult R 1 n * r
Proof.
R: Ring
r: R
n: cring_Z
rng_int_mult R r n = rng_int_mult R 1 n * r
  cbn.
R: Ring
r: R
n: cring_Z
grp_pow r n = grp_pow 1 n * r
  rhs napply (grp_pow_natural (grp_homo_rng_right_mult r)); cbn.
R: Ring
r: R
n: cring_Z
grp_pow r n = grp_pow (1 * r) n
  by rewrite rng_mult_one_l.
Defined.

(** Similarly, there is a left-distributive law. *)
Definition rng_int_mult_dist_l {R : Ring} (r : R) (n : cring_Z)
  : rng_int_mult R r n = r * (rng_int_mult R 1 n).
R: Ring
r: R
n: cring_Z
rng_int_mult R r n = r * rng_int_mult R 1 n
Proof.
R: Ring
r: R
n: cring_Z
rng_int_mult R r n = r * rng_int_mult R 1 n
  cbn.
R: Ring
r: R
n: cring_Z
grp_pow r n = r * grp_pow 1 n
  rhs napply (grp_pow_natural (grp_homo_rng_left_mult r)); cbn.
R: Ring
r: R
n: cring_Z
grp_pow r n = grp_pow (r * 1) n
  by rewrite rng_mult_one_r.
Defined.

(** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
  : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
R: Ring
IsSemiGroupPreserving (rng_int_mult R 1)
Proof.
R: Ring
IsSemiGroupPreserving (rng_int_mult R 1)
  intros x y.
R: Ring
x, y: cring_Z
rng_int_mult R 1 (sg_op x y) =
sg_op (rng_int_mult R 1 x) (rng_int_mult R 1 y)
  cbn; unfold sg_op.
R: Ring
x, y: cring_Z
int_rec_equiv mon_unit (group_sgop 1) (x * y) = grp_pow 1 x * grp_pow 1 y
  lhs napply grp_pow_int_mul.
R: Ring
x, y: cring_Z
grp_pow (grp_pow 1 x) y = grp_pow 1 x * grp_pow 1 y
  napply rng_int_mult_dist_l.
Defined.

(** [rng_int_mult R 1] is a ring homomorphism *)
Definition rng_homo_int (R : Ring) : (cring_Z : Ring) $-> R.
R: Ring
(cring_Z : Ring) $-> R
Proof.
R: Ring
(cring_Z : Ring) $-> R
  snapply Build_RingHomomorphism.
R: Ring
cring_Z -> R
R: Ring
abstract_algebra.IsSemiRingPreserving ?rng_homo_map
  1: exact (rng_int_mult R 1).
R: Ring
abstract_algebra.IsSemiRingPreserving (rng_int_mult R 1)
  repeat split.
R: Ring
IsSemiGroupPreserving (rng_int_mult R 1)
R: Ring
IsSemiGroupPreserving (rng_int_mult R 1)
R: Ring
IsUnitPreserving (rng_int_mult R 1)
  1,2: exact _.
R: Ring
IsUnitPreserving (rng_int_mult R 1)
  apply rng_plus_zero_r.
Defined.

(** The integers are the initial commutative ring *)
Instance isinitial_cring_Z : IsInitial cring_Z.
IsInitial cring_Z
Proof.
IsInitial cring_Z
  unfold IsInitial.
forall y : CRing, {f : cring_Z $-> y & forall g : cring_Z $-> y, f $== g}
  intro R.
R: CRing
{f : cring_Z $-> R & forall g : cring_Z $-> R, f $== g}
  exists (rng_homo_int R).
R: CRing
forall g : cring_Z $-> R, rng_homo_int R $== g
  intros g.
R: CRing
g: cring_Z $-> R
rng_homo_int R $== g
  rapply (int_homotopic (ring_plus 1)); cbn beta.
R: CRing
g: cring_Z $-> R
rng_homo_int R 0%int = g 0%int
R: CRing
g: cring_Z $-> R
(fun x : Int => rng_homo_int R x.+1%int) ==
(fun x : Int => ring_plus 1 (rng_homo_int R x))
R: CRing
g: cring_Z $-> R
(fun x : Int => g x.+1%int) == (fun x : Int => ring_plus 1 (g x))
  -
R: CRing
g: cring_Z $-> R
rng_homo_int R 0%int = g 0%int exact (grp_homo_unit g)^.
  -
R: CRing
g: cring_Z $-> R
(fun x : Int => rng_homo_int R x.+1%int) ==
(fun x : Int => ring_plus 1 (rng_homo_int R x)) reflexivity.
  -
R: CRing
g: cring_Z $-> R
(fun x : Int => g x.+1%int) == (fun x : Int => ring_plus 1 (g x)) intro x.
R: CRing
g: cring_Z $-> R
x: Int
g x.+1%int = ring_plus 1 (g x)
    lhs exact (rng_homo_plus g 1 x).
R: CRing
g: cring_Z $-> R
x: Int
g 1 + g x = ring_plus 1 (g x)
    by rewrite rng_homo_one.
Defined.