# Integer multiples of elements of rings

Content created by Fredrik Bakke, Egbert Rijke, Gregor Perčič and malarbol.

Created on 2023-09-10.

module ring-theory.integer-multiples-of-elements-rings where

Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import group-theory.homomorphisms-abelian-groups
open import group-theory.integer-multiples-of-elements-abelian-groups

open import ring-theory.commuting-elements-rings
open import ring-theory.homomorphisms-rings
open import ring-theory.multiples-of-elements-rings
open import ring-theory.rings


## Idea

The integer multiple operation on a ring is the map k x ↦ kx, which is defined by iteratively adding x with itself an integer k times.

## Definitions

### Iteratively adding g

module _
{l : Level} (R : Ring l)
where

type-Ring R → ℤ → type-Ring R → type-Ring R


### Integer multiples of elements of rings

module _
{l : Level} (R : Ring l)
where

integer-multiple-Ring : ℤ → type-Ring R → type-Ring R
integer-multiple-Ring = integer-multiple-Ab (ab-Ring R)


### The predicate of being a natural multiple of an element in an ring

We say that an element y is an integer multiple of an element x if there exists an integer k such that kx ＝ y.

module _
{l : Level} (R : Ring l)
where

is-integer-multiple-of-element-prop-Ring :
(x y : type-Ring R) → Prop l
is-integer-multiple-of-element-prop-Ring =
is-integer-multiple-of-element-prop-Ab (ab-Ring R)

is-integer-multiple-of-element-Ring :
(x y : type-Ring R) → UU l
is-integer-multiple-of-element-Ring =
is-integer-multiple-of-element-Ab (ab-Ring R)

is-prop-is-integer-multiple-of-element-Ring :
(x y : type-Ring R) →
is-prop (is-integer-multiple-of-element-Ring x y)
is-prop-is-integer-multiple-of-element-Ring =
is-prop-is-integer-multiple-of-element-Ab (ab-Ring R)


## Properties

### Associativity of iterated addition by a ring element

module _
{l : Level} (R : Ring l) (a : type-Ring R)
where

(k : ℤ) (h1 h2 : type-Ring R) →


### integer-multiple-Ring R (int-ℕ n) a ＝ multiple-Ring R n a

module _
{l : Level} (R : Ring l)
where

integer-multiple-int-Ring :
(n : ℕ) (a : type-Ring R) →
integer-multiple-Ring R (int-ℕ n) a ＝ multiple-Ring R n a
integer-multiple-int-Ring = integer-multiple-int-Ab (ab-Ring R)

integer-multiple-in-pos-Ring :
(n : ℕ) (a : type-Ring R) →
integer-multiple-Ring R (in-pos-ℤ n) a ＝
multiple-Ring R (succ-ℕ n) a
integer-multiple-in-pos-Ring =
integer-multiple-in-pos-Ab (ab-Ring R)

integer-multiple-in-neg-Ring :
(n : ℕ) (a : type-Ring R) →
integer-multiple-Ring R (in-neg-ℤ n) a ＝
neg-Ring R (multiple-Ring R (succ-ℕ n) a)
integer-multiple-in-neg-Ring =
integer-multiple-in-neg-Ab (ab-Ring R)


### The integer multiple 0x is 0

module _
{l : Level} (R : Ring l) (a : type-Ring R)
where

integer-multiple-zero-Ring :
integer-multiple-Ring R zero-ℤ a ＝ zero-Ring R
integer-multiple-zero-Ring =
integer-multiple-zero-Ab (ab-Ring R) a


### 1x ＝ x

module _
{l : Level} (R : Ring l) (a : type-Ring R)
where

integer-multiple-one-Ring :
integer-multiple-Ring R one-ℤ a ＝ a
integer-multiple-one-Ring =
integer-multiple-one-Ab (ab-Ring R) a


### The integer multiple (-1)x is the negative of x

module _
{l : Level} (R : Ring l) (a : type-Ring R)
where

integer-multiple-neg-one-Ring :
integer-multiple-Ring R neg-one-ℤ a ＝ neg-Ring R a
integer-multiple-neg-one-Ring =
integer-multiple-neg-one-Ab (ab-Ring R) a


### The integer multiple (x + y)a computes to xa + ya

module _
{l : Level} (R : Ring l) (a : type-Ring R)
where

(x y : ℤ) →
integer-multiple-Ring R (x +ℤ y) a ＝
( integer-multiple-Ring R x a)
( integer-multiple-Ring R y a)


### The integer multiple (-k)x is the negative of the integer multiple kx

module _
{l : Level} (R : Ring l)
where

integer-multiple-neg-Ring :
(k : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (neg-ℤ k) x ＝
neg-Ring R (integer-multiple-Ring R k x)
integer-multiple-neg-Ring =
integer-multiple-neg-Ab (ab-Ring R)


### (k + 1)x = kx + x and (k + 1)x = x + kx

module _
{l1 : Level} (R : Ring l1)
where

integer-multiple-succ-Ring :
(k : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (succ-ℤ k) x ＝
add-Ring R (integer-multiple-Ring R k x) x
integer-multiple-succ-Ring =
integer-multiple-succ-Ab (ab-Ring R)

integer-multiple-succ-Ring' :
(k : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (succ-ℤ k) x ＝
add-Ring R x (integer-multiple-Ring R k x)
integer-multiple-succ-Ring' =
integer-multiple-succ-Ab' (ab-Ring R)


### (k - 1)x = kx - x and (k - 1)x = -x + kx

module _
{l1 : Level} (R : Ring l1)
where

integer-multiple-pred-Ring :
(k : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (pred-ℤ k) x ＝
right-subtraction-Ring R (integer-multiple-Ring R k x) x
integer-multiple-pred-Ring =
integer-multiple-pred-Ab (ab-Ring R)

integer-multiple-pred-Ring' :
(k : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (pred-ℤ k) x ＝
left-subtraction-Ring R x (integer-multiple-Ring R k x)
integer-multiple-pred-Ring' =
integer-multiple-pred-Ab' (ab-Ring R)


### k0 ＝ 0

module _
{l : Level} (R : Ring l)
where

right-zero-law-integer-multiple-Ring :
(k : ℤ) → integer-multiple-Ring R k (zero-Ring R) ＝ zero-Ring R
right-zero-law-integer-multiple-Ring =
right-zero-law-integer-multiple-Ab (ab-Ring R)


### Integer multiples distribute over the sum of x and y

module _
{l : Level} (R : Ring l)
where

(k : ℤ) (x y : type-Ring R) →
integer-multiple-Ring R k (add-Ring R x y) ＝
add-Ring R (integer-multiple-Ring R k x) (integer-multiple-Ring R k y)


### Left and right integer multiple laws for ring multiplication

module _
{l : Level} (R : Ring l)
where

left-integer-multiple-law-mul-Ring :
(k : ℤ) (x y : type-Ring R) →
mul-Ring R (integer-multiple-Ring R k x) y ＝
integer-multiple-Ring R k (mul-Ring R x y)
left-integer-multiple-law-mul-Ring (inl zero-ℕ) x y =
( ap (mul-Ring' R y) (integer-multiple-neg-one-Ring R x)) ∙
( ( left-negative-law-mul-Ring R x y) ∙
( inv (integer-multiple-neg-one-Ring R _)))
left-integer-multiple-law-mul-Ring (inl (succ-ℕ k)) x y =
( ap (mul-Ring' R y) (integer-multiple-pred-Ring R (inl k) x)) ∙
( ( right-distributive-mul-right-subtraction-Ring R _ _ _) ∙
( ( ap
( λ u → right-subtraction-Ring R u _)
( left-integer-multiple-law-mul-Ring (inl k) _ _)) ∙
( inv (integer-multiple-pred-Ring R (inl k) _))))
left-integer-multiple-law-mul-Ring (inr (inl _)) x y =
( ap (mul-Ring' R y) (integer-multiple-zero-Ring R x)) ∙
( left-zero-law-mul-Ring R y)
left-integer-multiple-law-mul-Ring (inr (inr zero-ℕ)) x y =
( ap (mul-Ring' R y) (integer-multiple-one-Ring R x)) ∙
( inv (integer-multiple-one-Ring R _))
left-integer-multiple-law-mul-Ring (inr (inr (succ-ℕ k))) x y =
( ap (mul-Ring' R y) (integer-multiple-succ-Ring R (inr (inr k)) x)) ∙
( ( right-distributive-mul-add-Ring R _ _ _) ∙
( ( ap
( left-integer-multiple-law-mul-Ring (inr (inr k)) _ _)) ∙
( inv (integer-multiple-succ-Ring R (inr (inr k)) _))))

right-integer-multiple-law-mul-Ring :
(k : ℤ) (x y : type-Ring R) →
mul-Ring R x (integer-multiple-Ring R k y) ＝
integer-multiple-Ring R k (mul-Ring R x y)
right-integer-multiple-law-mul-Ring (inl zero-ℕ) x y =
( ap (mul-Ring R x) (integer-multiple-neg-one-Ring R y)) ∙
( ( right-negative-law-mul-Ring R x y) ∙
( inv (integer-multiple-neg-one-Ring R _)))
right-integer-multiple-law-mul-Ring (inl (succ-ℕ k)) x y =
( ap (mul-Ring R x) (integer-multiple-pred-Ring R (inl k) y)) ∙
( ( left-distributive-mul-right-subtraction-Ring R _ _ _) ∙
( ( ap
( right-integer-multiple-law-mul-Ring (inl k) x y)) ∙
( inv (integer-multiple-pred-Ring R (inl k) _))))
right-integer-multiple-law-mul-Ring (inr (inl _)) x y =
( ap (mul-Ring R x) (integer-multiple-zero-Ring R y)) ∙
( right-zero-law-mul-Ring R x)
right-integer-multiple-law-mul-Ring (inr (inr zero-ℕ)) x y =
( ap (mul-Ring R x) (integer-multiple-one-Ring R y)) ∙
( inv (integer-multiple-one-Ring R _))
right-integer-multiple-law-mul-Ring (inr (inr (succ-ℕ k))) x y =
( ap (mul-Ring R x) (integer-multiple-succ-Ring R (inr (inr k)) y)) ∙
( ( left-distributive-mul-add-Ring R x _ _) ∙
( ( ap
( right-integer-multiple-law-mul-Ring (inr (inr k)) x y)) ∙
( inv (integer-multiple-succ-Ring R (inr (inr k)) _))))


### If x and y commute, then integer multiples of x and y commute

module _
{l : Level} (R : Ring l)
where

commute-integer-multiple-Ring :
(k : ℤ) {x y : type-Ring R} → commute-Ring R x y →
commute-Ring R x (integer-multiple-Ring R k y)
commute-integer-multiple-Ring (inl zero-ℕ) H =
tr
( commute-Ring R _)
( inv (integer-multiple-neg-one-Ring R _))
( commute-neg-Ring R H)
commute-integer-multiple-Ring (inl (succ-ℕ k)) H =
tr
( commute-Ring R _)
( inv (integer-multiple-pred-Ring R (inl k) _))
( commute-right-subtraction-Ring R
( commute-integer-multiple-Ring (inl k) H)
( H))
commute-integer-multiple-Ring (inr (inl _)) {x} H =
tr
( commute-Ring R _)
( inv (integer-multiple-zero-Ring R x))
( inv (commute-zero-Ring R _))
commute-integer-multiple-Ring (inr (inr zero-ℕ)) H =
tr
( commute-Ring R _)
( inv (integer-multiple-one-Ring R _))
( H)
commute-integer-multiple-Ring (inr (inr (succ-ℕ k))) H =
tr
( commute-Ring R _)
( inv (integer-multiple-succ-Ring R (inr (inr k)) _))
( commute-integer-multiple-Ring (inr (inr k)) H)
( H))

commute-integer-multiples-Ring :
(k l : ℤ) {x y : type-Ring R} → commute-Ring R x y →
commute-Ring R (integer-multiple-Ring R k x) (integer-multiple-Ring R l y)
commute-integer-multiples-Ring (inl zero-ℕ) l H =
tr
( commute-Ring' R _)
( inv (integer-multiple-neg-one-Ring R _))
( inv (commute-neg-Ring R (inv (commute-integer-multiple-Ring l H))))
commute-integer-multiples-Ring (inl (succ-ℕ k)) l H =
tr
( commute-Ring' R _)
( inv (integer-multiple-pred-Ring R (inl k) _))
( inv
( commute-right-subtraction-Ring R
( commute-integer-multiples-Ring l (inl k) (inv H))
( inv (commute-integer-multiple-Ring l H))))
commute-integer-multiples-Ring (inr (inl _)) l {x} H =
tr
( commute-Ring' R _)
( inv (integer-multiple-zero-Ring R x))
( commute-zero-Ring R _)
commute-integer-multiples-Ring (inr (inr zero-ℕ)) l H =
tr
( commute-Ring' R _)
( inv (integer-multiple-one-Ring R _))
( commute-integer-multiple-Ring l H)
commute-integer-multiples-Ring (inr (inr (succ-ℕ k))) l H =
tr
( commute-Ring' R _)
( inv (integer-multiple-succ-Ring R (inr (inr k)) _))
( inv
( commute-integer-multiples-Ring l (inr (inr k)) (inv H))
( inv (commute-integer-multiple-Ring l H))))

commute-integer-multiples-diagonal-Ring :
(k l : ℤ) {x : type-Ring R} →
commute-Ring R (integer-multiple-Ring R k x) (integer-multiple-Ring R l x)
commute-integer-multiples-diagonal-Ring k l =
commute-integer-multiples-Ring k l refl


### For each integer k, the operation of taking k-multiples is a group homomorphism

module _
{l : Level} (R : Ring l) (k : ℤ)
where

hom-ab-integer-multiple-Ring : hom-Ab (ab-Ring R) (ab-Ring R)
hom-ab-integer-multiple-Ring = hom-integer-multiple-Ab (ab-Ring R) k


### Multiples by products of integers are iterated integer multiples

module _
{l : Level} (R : Ring l)
where

integer-multiple-mul-Ring :
(k l : ℤ) (x : type-Ring R) →
integer-multiple-Ring R (k *ℤ l) x ＝
integer-multiple-Ring R k (integer-multiple-Ring R l x)
integer-multiple-mul-Ring =
integer-multiple-mul-Ab (ab-Ring R)

swap-integer-multiple-Ring :
(k l : ℤ) (x : type-Ring R) →
integer-multiple-Ring R k (integer-multiple-Ring R l x) ＝
integer-multiple-Ring R l (integer-multiple-Ring R k x)
swap-integer-multiple-Ring =
swap-integer-multiple-Ab (ab-Ring R)


### Ring homomorphisms preserve integer multiples

module _
{l1 l2 : Level} (R : Ring l1) (S : Ring l2) (f : hom-Ring R S)
where

preserves-integer-multiples-hom-Ring :
(k : ℤ) (x : type-Ring R) →
map-hom-Ring R S f (integer-multiple-Ring R k x) ＝
integer-multiple-Ring S k (map-hom-Ring R S f x)
preserves-integer-multiples-hom-Ring =
preserves-integer-multiples-hom-Ab
( ab-Ring R)
( ab-Ring S)
( hom-ab-hom-Ring R S f)

module _
{l1 l2 : Level} (R : Ring l1) (S : Ring l2) (f : hom-Ring R S)
where

eq-integer-multiple-hom-Ring :
(g : hom-Ring R S) (k : ℤ) (x : type-Ring R) →
( map-hom-Ring R S f x ＝ map-hom-Ring R S g x) →
map-hom-Ring R S f (integer-multiple-Ring R k x) ＝
map-hom-Ring R S g (integer-multiple-Ring R k x)
eq-integer-multiple-hom-Ring g =
eq-integer-multiple-hom-Ab
( ab-Ring R)
( ab-Ring S)
( hom-ab-hom-Ring R S f)
( hom-ab-hom-Ring R S g)


### Ring homomorphisms preserve integer multiples of 1

module _
{l1 l2 : Level} (R : Ring l1) (S : Ring l2) (f : hom-Ring R S)
where

preserves-integer-multiple-one-hom-Ring :
(k : ℤ) →
map-hom-Ring R S f (integer-multiple-Ring R k (one-Ring R)) ＝
integer-multiple-Ring S k (one-Ring S)
preserves-integer-multiple-one-hom-Ring k =
( preserves-integer-multiples-hom-Ring R S f k (one-Ring R)) ∙
( ap (integer-multiple-Ring S k) (preserves-one-hom-Ring R S f))