Library HoTT.Algebra.Rings.Z

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.
Proof.
  snapply Build_CRing'.
  - exact abgroup_Z.
  - exact 1%int.
  - exact int_mul.
  - exact int_mul_comm.
  - exact int_mul_assoc.
  - exact int_dist_l.
  - 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.
Proof.
  cbn.
  rhs napply (grp_pow_natural (grp_homo_rng_right_mult r)); cbn.
  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 ).
Proof.
  cbn.
  rhs napply (grp_pow_natural (grp_homo_rng_left_mult r)); cbn.
  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).
Proof.
  intros x y.
  cbn; unfold sg_op.
  lhs napply grp_pow_int_mul.
  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.
Proof.
  snapply Build_RingHomomorphism.
  1: exact (rng_int_mult R 1).
  repeat split.
  1,2: exact _.
  apply rng_plus_zero_r.
Defined.

The integers are the initial commutative ring

Instance isinitial_cring_Z : IsInitial cring_Z.
Proof.
  unfold IsInitial.
  intro R.
  ∃ (rng_homo_int R).
  intros g.
  rapply (int_homotopic (ring_plus 1)); cbn beta.
  - exact (grp_homo_unit g)^.
  - reflexivity.
  - intro x.
    lhs exact (rng_homo_plus g 1 x).
    by rewrite rng_homo_one.
Defined.