# Cyclic rings

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

Created on 2023-09-21.

module ring-theory.cyclic-rings where

Imports
open import commutative-algebra.commutative-rings

open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.ring-of-integers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.cyclic-groups
open import group-theory.free-groups-with-one-generator
open import group-theory.generating-elements-groups
open import group-theory.groups

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


## Idea

A ring is said to be cyclic if its underlying additive group is a cyclic group. We will show that the following three claims about a ring R are equivalent:

1. The ring R is cyclic.
2. The element 1 is a generating element of the abelian group (R,0,+,-).
3. The subset of generating elements of R is the subset of invertible elements of R.

Cyclic rings therefore have a specified generating element, i.e., the element 1. With this fact in the pocket, it is easy to show that cyclic rings are commutative rings. Furthermore, the multiplicative structure of R coincides with the multiplicative structure constructed in group-theory.generating-elements-groups using the generating element 1. In particular, it follows that for any cyclic group G, the type of ring structures on G is equivalent with the type of generating elements of G.

Note that the classification of cyclic unital rings is somewhat different from the nonunital cyclic rings: Cyclic unital rings are quotients of the ring ℤ of integers, whereas cyclic nonunital rings are isomorphic to ideals of quotients of the ring ℤ. [BSCS05]

Since cyclic rings are quotients of ℤ, it follows that quotients of cyclic rings are cyclic rings.

## Definitions

### The predicate of being a cyclic ring

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

is-cyclic-prop-Ring : Prop l
is-cyclic-prop-Ring = is-cyclic-prop-Group (group-Ring R)

is-cyclic-Ring : UU l
is-cyclic-Ring = is-cyclic-Group (group-Ring R)

is-prop-is-cyclic-Ring : is-prop is-cyclic-Ring
is-prop-is-cyclic-Ring = is-prop-is-cyclic-Group (group-Ring R)


### The predicate of the initial morphism being surjective

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

is-surjective-initial-hom-prop-Ring : Prop l
is-surjective-initial-hom-prop-Ring =
is-surjective-Prop (map-initial-hom-Ring R)

is-surjective-initial-hom-Ring : UU l
is-surjective-initial-hom-Ring =
type-Prop is-surjective-initial-hom-prop-Ring

is-prop-is-surjective-initial-hom-Ring :
is-prop is-surjective-initial-hom-Ring
is-prop-is-surjective-initial-hom-Ring =
is-prop-type-Prop is-surjective-initial-hom-prop-Ring


### Cyclic rings

Cyclic-Ring : (l : Level) → UU (lsuc l)
Cyclic-Ring l = Σ (Ring l) is-cyclic-Ring

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

ring-Cyclic-Ring : Ring l
ring-Cyclic-Ring = pr1 R

ab-Cyclic-Ring : Ab l
ab-Cyclic-Ring = ab-Ring ring-Cyclic-Ring

group-Cyclic-Ring : Group l
group-Cyclic-Ring = group-Ring ring-Cyclic-Ring

is-cyclic-Cyclic-Ring : is-cyclic-Ring ring-Cyclic-Ring
is-cyclic-Cyclic-Ring = pr2 R

cyclic-group-Cyclic-Ring : Cyclic-Group l
pr1 cyclic-group-Cyclic-Ring = group-Cyclic-Ring
pr2 cyclic-group-Cyclic-Ring = is-cyclic-Cyclic-Ring

type-Cyclic-Ring : UU l
type-Cyclic-Ring = type-Ring ring-Cyclic-Ring

set-Cyclic-Ring : Set l
set-Cyclic-Ring = set-Ring ring-Cyclic-Ring

zero-Cyclic-Ring : type-Cyclic-Ring
zero-Cyclic-Ring = zero-Ring ring-Cyclic-Ring

one-Cyclic-Ring : type-Cyclic-Ring
one-Cyclic-Ring = one-Ring ring-Cyclic-Ring

add-Cyclic-Ring : (x y : type-Cyclic-Ring) → type-Cyclic-Ring

neg-Cyclic-Ring : type-Cyclic-Ring → type-Cyclic-Ring
neg-Cyclic-Ring = neg-Ring ring-Cyclic-Ring

mul-Cyclic-Ring : (x y : type-Cyclic-Ring) → type-Cyclic-Ring
mul-Cyclic-Ring = mul-Ring ring-Cyclic-Ring

mul-Cyclic-Ring' : (x y : type-Cyclic-Ring) → type-Cyclic-Ring
mul-Cyclic-Ring' = mul-Ring' ring-Cyclic-Ring

integer-multiple-Cyclic-Ring : ℤ → type-Cyclic-Ring → type-Cyclic-Ring
integer-multiple-Cyclic-Ring = integer-multiple-Ring ring-Cyclic-Ring

(x : type-Cyclic-Ring) →

(x : type-Cyclic-Ring) →

(x y z : type-Cyclic-Ring) →

(x : type-Cyclic-Ring) →
add-Cyclic-Ring (neg-Cyclic-Ring x) x ＝ zero-Cyclic-Ring

(x : type-Cyclic-Ring) →
add-Cyclic-Ring x (neg-Cyclic-Ring x) ＝ zero-Cyclic-Ring

left-unit-law-mul-Cyclic-Ring :
(x : type-Cyclic-Ring) →
mul-Cyclic-Ring one-Cyclic-Ring x ＝ x
left-unit-law-mul-Cyclic-Ring =
left-unit-law-mul-Ring ring-Cyclic-Ring

right-unit-law-mul-Cyclic-Ring :
(x : type-Cyclic-Ring) →
mul-Cyclic-Ring x one-Cyclic-Ring ＝ x
right-unit-law-mul-Cyclic-Ring =
right-unit-law-mul-Ring ring-Cyclic-Ring

associative-mul-Cyclic-Ring :
(x y z : type-Cyclic-Ring) →
mul-Cyclic-Ring (mul-Cyclic-Ring x y) z ＝
mul-Cyclic-Ring x (mul-Cyclic-Ring y z)
associative-mul-Cyclic-Ring =
associative-mul-Ring ring-Cyclic-Ring

(x y z : type-Cyclic-Ring) →
mul-Cyclic-Ring x (add-Cyclic-Ring y z) ＝
add-Cyclic-Ring (mul-Cyclic-Ring x y) (mul-Cyclic-Ring x z)

(x y z : type-Cyclic-Ring) →
mul-Cyclic-Ring (add-Cyclic-Ring x y) z ＝
add-Cyclic-Ring (mul-Cyclic-Ring x z) (mul-Cyclic-Ring y z)

swap-integer-multiple-Cyclic-Ring :
(k l : ℤ) (x : type-Cyclic-Ring) →
integer-multiple-Cyclic-Ring k (integer-multiple-Cyclic-Ring l x) ＝
integer-multiple-Cyclic-Ring l (integer-multiple-Cyclic-Ring k x)
swap-integer-multiple-Cyclic-Ring =
swap-integer-multiple-Ring ring-Cyclic-Ring

left-integer-multiple-law-mul-Cyclic-Ring :
(k : ℤ) (x y : type-Cyclic-Ring) →
mul-Cyclic-Ring (integer-multiple-Cyclic-Ring k x) y ＝
integer-multiple-Cyclic-Ring k (mul-Cyclic-Ring x y)
left-integer-multiple-law-mul-Cyclic-Ring =
left-integer-multiple-law-mul-Ring ring-Cyclic-Ring

right-integer-multiple-law-mul-Cyclic-Ring :
(k : ℤ) (x y : type-Cyclic-Ring) →
mul-Cyclic-Ring x (integer-multiple-Cyclic-Ring k y) ＝
integer-multiple-Cyclic-Ring k (mul-Cyclic-Ring x y)
right-integer-multiple-law-mul-Cyclic-Ring =
right-integer-multiple-law-mul-Ring ring-Cyclic-Ring


## Properties

### If R is a cyclic ring, then any generator of its additive group is invertible

Proof: Let g be a generator of the additive group (R,0,+,-). Then there is an integer n such that ng ＝ 1. Then we obtain that (n1)g ＝ n(1g) ＝ ng ＝ 1 and that g(n1) ＝ n(g1) ＝ ng ＝ 1. It follows that the element n1 is the multiplicative inverse of g.

module _
{l : Level} (R : Ring l) (g : type-Ring R)
(H : is-generating-element-Group (group-Ring R) g)
where

abstract
is-invertible-is-generating-element-group-Ring :
is-invertible-element-Ring R g
is-invertible-is-generating-element-group-Ring =
apply-universal-property-trunc-Prop
( is-surjective-hom-element-is-generating-element-Group
( group-Ring R)
( g)
( H)
( one-Ring R))
( is-invertible-element-prop-Ring R g)
( λ (n , p) →
( integer-multiple-Ring R n (one-Ring R)) ,
( ( right-integer-multiple-law-mul-Ring R n g
( one-Ring R)) ∙
( ap
( integer-multiple-Ring R n)
( right-unit-law-mul-Ring R g)) ∙
( p)) ,
( ( left-integer-multiple-law-mul-Ring R n
( one-Ring R)
( g)) ∙
( ap
( integer-multiple-Ring R n)
( left-unit-law-mul-Ring R g)) ∙
( p)))


### If R is a cyclic ring if and only if 1 is a generator of its additive group

Equivalently, we assert that R is cyclic if and only if initial-hom-Ring R is surjective.

Proof: Of course, if 1 is a generator of the additive group of R, then the additive group of R is cyclic. For the converse, consider a generating element g of the additive group (R,0,+,-). Then there exists an integer n such that ng ＝ 1.

Let x be an arbitrary element of the ring R. Then there exists an integer k such that kg ＝ gx. We claim that k1 ＝ x. To see this, we calculate:

  k1 ＝ k(ng) ＝ n(kg) ＝ n(gx) ＝ (ng)x ＝ 1x ＝ x.


This proves that every element is an integer multiple of 1. We conclude that 1 generates the additive group (R,0,+,-).

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

abstract
is-surjective-initial-hom-Cyclic-Ring :
is-surjective-initial-hom-Ring (ring-Cyclic-Ring R)
is-surjective-initial-hom-Cyclic-Ring x =
apply-universal-property-trunc-Prop
( is-cyclic-Cyclic-Ring R)
( trunc-Prop
( fiber (map-initial-hom-Ring (ring-Cyclic-Ring R)) x))
( λ (g , u) →
apply-twice-universal-property-trunc-Prop
( is-surjective-hom-element-is-generating-element-Group
( group-Cyclic-Ring R)
( g)
( u)
( one-Cyclic-Ring R))
( is-surjective-hom-element-is-generating-element-Group
( group-Cyclic-Ring R)
( g)
( u)
( mul-Cyclic-Ring R g x))
( trunc-Prop
( fiber (map-initial-hom-Ring (ring-Cyclic-Ring R)) x))
( λ (n , p) (k , q) →
unit-trunc-Prop
( ( k) ,
( equational-reasoning
integer-multiple-Cyclic-Ring R k
( one-Cyclic-Ring R)
＝ integer-multiple-Cyclic-Ring R k
( integer-multiple-Cyclic-Ring R n g)
by
ap
( integer-multiple-Cyclic-Ring R k)
( inv p)
＝ integer-multiple-Cyclic-Ring R n
( integer-multiple-Cyclic-Ring R k g)
by
swap-integer-multiple-Cyclic-Ring R k n g
＝ integer-multiple-Cyclic-Ring R n
( mul-Cyclic-Ring R g x)
by
ap (integer-multiple-Cyclic-Ring R n) q
＝ mul-Cyclic-Ring R
( integer-multiple-Cyclic-Ring R n g)
( x)
by
inv (left-integer-multiple-law-mul-Cyclic-Ring R n g x)
＝ mul-Cyclic-Ring R (one-Cyclic-Ring R) x
by ap (mul-Cyclic-Ring' R x) p
＝ x
by left-unit-law-mul-Cyclic-Ring R x))))

abstract
is-generating-element-one-Cyclic-Ring :
is-generating-element-Group (group-Cyclic-Ring R) (one-Cyclic-Ring R)
is-generating-element-one-Cyclic-Ring =
is-generating-element-is-surjective-hom-element-Group
( group-Cyclic-Ring R)
( one-Cyclic-Ring R)
( is-surjective-initial-hom-Cyclic-Ring)


### The classification of cyclic rings

module _
{l : Level}
where

is-cyclic-is-surjective-initial-hom-Ring :
(R : Ring l) →
is-surjective-initial-hom-Ring R → is-cyclic-Ring R
is-cyclic-is-surjective-initial-hom-Ring R H =
unit-trunc-Prop
( one-Ring R ,
is-generating-element-is-surjective-hom-element-Group
( group-Ring R)
( one-Ring R)
( H))

classification-Cyclic-Ring :
Cyclic-Ring l ≃ Σ (Ring l) is-surjective-initial-hom-Ring
classification-Cyclic-Ring =
equiv-type-subtype
( is-prop-is-cyclic-Ring)
( is-prop-is-surjective-initial-hom-Ring)
( λ R H → is-surjective-initial-hom-Cyclic-Ring (R , H))
( is-cyclic-is-surjective-initial-hom-Ring)


### If R is a cyclic ring, then any invertible element is a generator of its additive group

Proof: Let x be an invertible element of R. To show that x generates the abelian group (R,0,+,1) we need to show that for any element y : R there exists an integer k such that kx ＝ y. Let n1 ＝ x⁻¹ and let m1 ＝ y. Then we calculate

  (mn)x ＝ m(nx) ＝ m(n(1x)) ＝ m((n1)x) ＝ m(x⁻¹x) ＝ m1 ＝ y.

module _
{l : Level} (R : Cyclic-Ring l) {x : type-Cyclic-Ring R}
(H : is-invertible-element-Ring (ring-Cyclic-Ring R) x)
where

abstract
is-surjective-hom-element-is-invertible-element-Cyclic-Ring :
is-surjective-hom-element-Group (group-Cyclic-Ring R) x
is-surjective-hom-element-is-invertible-element-Cyclic-Ring y =
apply-twice-universal-property-trunc-Prop
( is-surjective-initial-hom-Cyclic-Ring R
( inv-is-invertible-element-Ring (ring-Cyclic-Ring R) H))
( is-surjective-initial-hom-Cyclic-Ring R y)
( trunc-Prop (fiber (map-hom-element-Group (group-Cyclic-Ring R) x) y))
( λ (n , p) (m , q) →
unit-trunc-Prop
( ( mul-ℤ m n) ,
( ( integer-multiple-mul-Ring (ring-Cyclic-Ring R) m n x) ∙
( ap
( integer-multiple-Cyclic-Ring R m)
( ( ap
( integer-multiple-Cyclic-Ring R n)
( inv (left-unit-law-mul-Cyclic-Ring R x))) ∙
( inv
( left-integer-multiple-law-mul-Ring
( ring-Cyclic-Ring R)
( n)
( one-Cyclic-Ring R)
( x))) ∙
( ap (mul-Cyclic-Ring' R x) p) ∙
( is-left-inverse-inv-is-invertible-element-Ring
( ring-Cyclic-Ring R)
( H)))) ∙
( q))))

is-generating-element-group-is-invertible-element-Cyclic-Ring :
is-generating-element-Group (group-Cyclic-Ring R) x
is-generating-element-group-is-invertible-element-Cyclic-Ring =
is-generating-element-is-surjective-hom-element-Group
( group-Cyclic-Ring R)
( x)
( is-surjective-hom-element-is-invertible-element-Cyclic-Ring)


### Any cyclic ring is commutative

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

abstract
commutative-mul-Cyclic-Ring :
(x y : type-Cyclic-Ring R) →
mul-Cyclic-Ring R x y ＝ mul-Cyclic-Ring R y x
commutative-mul-Cyclic-Ring x y =
apply-twice-universal-property-trunc-Prop
( is-surjective-initial-hom-Cyclic-Ring R x)
( is-surjective-initial-hom-Cyclic-Ring R y)
( Id-Prop (set-Cyclic-Ring R) _ _)
( λ where
( n , refl) (m , refl) →
commute-integer-multiples-diagonal-Ring (ring-Cyclic-Ring R) n m)

commutative-ring-Cyclic-Ring : Commutative-Ring l
pr1 commutative-ring-Cyclic-Ring = ring-Cyclic-Ring R
pr2 commutative-ring-Cyclic-Ring = commutative-mul-Cyclic-Ring


ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings

## References

[BSCS05]
Mária Bálintné Szendrei, Gábor Czédli, and Ágnes Szendrei. Absztrakt algebrai feladatok. Polygon, 2005. URL: https://interkonyv.hu/konyvek/balintne-szendrei-maria-czedli-gabor-szendrei-agnes-absztrakt-algebrai-feladatok/.