The standard cyclic rings

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-09.

module elementary-number-theory.standard-cyclic-rings where

Imports
open import commutative-algebra.commutative-rings

open import elementary-number-theory.integers
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.ring-of-integers
open import elementary-number-theory.standard-cyclic-groups

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.homotopies
open import foundation.identity-types
open import foundation.surjective-maps
open import foundation.universe-levels

open import group-theory.cyclic-groups
open import group-theory.generating-elements-groups

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


Idea

The standard cyclic rings ℤ/n are the rings of integers modulo n.

Definitions

The standard cyclic rings

ℤ-Mod-Ring : ℕ → Ring lzero
pr1 (ℤ-Mod-Ring n) = ℤ-Mod-Ab n
pr1 (pr1 (pr2 (ℤ-Mod-Ring n))) = mul-ℤ-Mod n
pr2 (pr1 (pr2 (ℤ-Mod-Ring n))) = associative-mul-ℤ-Mod n
pr1 (pr1 (pr2 (pr2 (ℤ-Mod-Ring n)))) = one-ℤ-Mod n
pr1 (pr2 (pr1 (pr2 (pr2 (ℤ-Mod-Ring n))))) = left-unit-law-mul-ℤ-Mod n
pr2 (pr2 (pr1 (pr2 (pr2 (ℤ-Mod-Ring n))))) = right-unit-law-mul-ℤ-Mod n
pr1 (pr2 (pr2 (pr2 (ℤ-Mod-Ring n)))) = left-distributive-mul-add-ℤ-Mod n
pr2 (pr2 (pr2 (pr2 (ℤ-Mod-Ring n)))) = right-distributive-mul-add-ℤ-Mod n

ℤ-Mod-Commutative-Ring : ℕ → Commutative-Ring lzero
pr1 (ℤ-Mod-Commutative-Ring n) = ℤ-Mod-Ring n
pr2 (ℤ-Mod-Commutative-Ring n) = commutative-mul-ℤ-Mod n


Integer multiplication in the standard cyclic rings

integer-multiple-ℤ-Mod :
(n : ℕ) → ℤ → ℤ-Mod n → ℤ-Mod n
integer-multiple-ℤ-Mod n k x = integer-multiple-Ring (ℤ-Mod-Ring n) k x


Properties

The negative-one element of the ring ℤ/n coincides with the element neg-one-ℤ-Mod n

is-neg-one-neg-one-ℤ-Mod :
( n : ℕ) → neg-one-Ring (ℤ-Mod-Ring n) ＝ neg-one-ℤ-Mod n
is-neg-one-neg-one-ℤ-Mod zero-ℕ = refl
is-neg-one-neg-one-ℤ-Mod (succ-ℕ n) = is-neg-one-neg-one-Fin n


The integer multiple k · 1 is equal to [k] : ℤ-Mod n

integer-multiplication-by-one-preserves-succ-ℤ :
(n : ℕ) (x : ℤ) →
integer-multiple-ℤ-Mod n (succ-ℤ x) (one-ℤ-Mod n) ＝
succ-ℤ-Mod n (integer-multiple-ℤ-Mod n x (one-ℤ-Mod n))
integer-multiplication-by-one-preserves-succ-ℤ n x =
( integer-multiple-succ-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) ∙
( inv
( n)
( integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n))))

integer-multiplication-by-one-preserves-pred-ℤ :
(n : ℕ) (x : ℤ) →
integer-multiple-ℤ-Mod n (pred-ℤ x) (one-ℤ-Mod n) ＝
pred-ℤ-Mod n (integer-multiple-ℤ-Mod n x (one-ℤ-Mod n))
integer-multiplication-by-one-preserves-pred-ℤ n x =
( ap
( λ k → integer-multiple-ℤ-Mod n k (one-ℤ-Mod n))
( ℤ-Mod-Ring n)
( one-ℤ-Mod n)
( x)
( neg-one-ℤ)) ∙
( ap
( λ k →
( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n))
( k))
( integer-multiple-neg-one-Ring (ℤ-Mod-Ring n) (one-ℤ-Mod n))) ∙
( ap
( λ k →
( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n))
( k))
( is-neg-one-neg-one-ℤ-Mod n)) ∙
( inv
( n)
( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n))))

compute-integer-multiple-one-ℤ-Mod :
( n : ℕ) → (λ k → integer-multiple-ℤ-Mod n k (one-ℤ-Mod n)) ~ mod-ℤ n
compute-integer-multiple-one-ℤ-Mod zero-ℕ x = integer-multiple-one-ℤ-Ring x
compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl zero-ℕ) =
( integer-multiple-neg-one-Ring
( ℤ-Mod-Ring (succ-ℕ n))
( one-ℤ-Mod (succ-ℕ n))) ∙
( is-neg-one-neg-one-ℤ-Mod (succ-ℕ n)) ∙
( inv (mod-neg-one-ℤ (succ-ℕ n)))
compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl (succ-ℕ x)) =
( integer-multiplication-by-one-preserves-pred-ℤ
( succ-ℕ n)
( inl x)) ∙
( ap
( pred-ℤ-Mod (succ-ℕ n))
( compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl x))) ∙
( inv (preserves-predecessor-mod-ℤ (succ-ℕ n) (inl x)))
compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inl _)) = refl
compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr zero-ℕ)) =
( integer-multiple-one-Ring
( ℤ-Mod-Ring (succ-ℕ n))
( one-ℤ-Mod (succ-ℕ n))) ∙
( inv (mod-one-ℤ (succ-ℕ n)))
compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr (succ-ℕ x))) =
( integer-multiplication-by-one-preserves-succ-ℤ
( succ-ℕ n)
( inr (inr x))) ∙
( ap
( succ-ℤ-Mod (succ-ℕ n))
( compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr x)))) ∙
( inv (preserves-successor-mod-ℤ (succ-ℕ n) (inr (inr x))))


The standard cyclic rings are cyclic

is-surjective-hom-element-one-ℤ-Mod :
( n : ℕ) → is-surjective-hom-element-Group (ℤ-Mod-Group n) (one-ℤ-Mod n)
is-surjective-hom-element-one-ℤ-Mod n =
is-surjective-htpy
( compute-integer-multiple-one-ℤ-Mod n)
( is-surjective-mod-ℤ n)

is-generating-element-one-ℤ-Mod :
( n : ℕ) → is-generating-element-Group (ℤ-Mod-Group n) (one-ℤ-Mod n)
is-generating-element-one-ℤ-Mod n =
is-generating-element-is-surjective-hom-element-Group
( ℤ-Mod-Group n)
( one-ℤ-Mod n)
( is-surjective-hom-element-one-ℤ-Mod n)

is-cyclic-ℤ-Mod-Group :
( n : ℕ) → is-cyclic-Group (ℤ-Mod-Group n)
is-cyclic-ℤ-Mod-Group n =
intro-exists
( one-ℤ-Mod n)
( is-generating-element-one-ℤ-Mod n)

is-cyclic-ℤ-Mod-Ring :
( n : ℕ) → is-cyclic-Ring (ℤ-Mod-Ring n)
is-cyclic-ℤ-Mod-Ring =
is-cyclic-ℤ-Mod-Group


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