Additive orders of elements of rings

Content created by Egbert Rijke and Gregor Perčič.

Created on 2023-09-21.

module ring-theory.additive-orders-of-elements-rings where

Imports
open import elementary-number-theory.group-of-integers
open import elementary-number-theory.integers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import group-theory.normal-subgroups
open import group-theory.orders-of-elements-groups
open import group-theory.subgroups
open import group-theory.subsets-groups

open import ring-theory.integer-multiples-of-elements-rings
open import ring-theory.rings


Idea

The additive order of an element x of a ring R is the normal subgroup of the group ℤ of integers consisting of all integers k such that kx ＝ 0.

Definitions

Additive orders of elements of rings

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

additive-order-element-Ring = order-element-Group (group-Ring R) x

subgroup-order-element-Group (group-Ring R) x

subset-order-element-Group (group-Ring R) x

is-in-additive-order-element-Ring : ℤ → UU l
is-in-order-element-Group (group-Ring R) x


Divisibility of additive orders of elements of rings

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

(x y : type-Ring R) → UU l
div-order-element-Group (group-Ring R)


Properties

The order of any element divides the order of 1

Suppose that k·1 ＝ 0 for some integer k. Then we have

  k·x ＝ k·(1x) ＝ (k·1)x ＝ 0x ＝ 0.


This shows that if the integer k is in the order of 1, then it is in the order of x. Therefore we conclude that the order of x always divides the order of 1.

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

(x : type-Ring R) →
div-order-element-Group (group-Ring R) x (one-Ring R)
( inv (left-zero-law-mul-Ring R x)) ∙
( ap (mul-Ring' R x) H) ∙
( left-integer-multiple-law-mul-Ring R k _ _) ∙
( ap (integer-multiple-Ring R k) (left-unit-law-mul-Ring R x))


If there exists an integer k such that k·x ＝ y then the order of y divides the order of x

Proof: Suppose that k·x ＝ y and l·x ＝ 0, then it follows that

  l·y ＝ l·(k·x) ＝ k·(l·x) ＝ k·0 ＝ 0.

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

(x y : type-Ring R) → is-integer-multiple-of-element-Ring R x y →
div-additive-order-element-is-integer-multiple-Ring x y H l p =
apply-universal-property-trunc-Prop H
( λ (k , q) →
( inv (right-zero-law-integer-multiple-Ring R k)) ∙
( ap (integer-multiple-Ring R k) p) ∙
( swap-integer-multiple-Ring R k l x ∙
( ap (integer-multiple-Ring R l) q)))


If there exists an integer k such that k·x ＝ 1 then the order of x is the order of 1

In other words, if there exists an integer k such that k·x ＝ 1, then the additive order of x is the characteristic of the ring R.

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

(x : type-Ring R) →
is-integer-multiple-of-element-Ring R x (one-Ring R) →
has-same-elements-Normal-Subgroup
( ℤ-Group)
div-additive-order-element-is-integer-multiple-Ring R x (one-Ring R) H y