The standard cyclic groups

Content created by Egbert Rijke.

Created on 2023-10-09.
Last modified on 2023-10-09.

module elementary-number-theory.standard-cyclic-groups where
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.groups
open import group-theory.semigroups


The standard cyclic groups are the groups of integers modulo k. The standard cyclic groups are abelian groups.

The fact that the standard cyclic groups are cyclic groups is shown in elementary-number-theory.standard-cyclic-rings.


The semigroup ℤ/k

ℤ-Mod-Semigroup : (k : )  Semigroup lzero
pr1 (ℤ-Mod-Semigroup k) = ℤ-Mod-Set k
pr1 (pr2 (ℤ-Mod-Semigroup k)) = add-ℤ-Mod k
pr2 (pr2 (ℤ-Mod-Semigroup k)) = associative-add-ℤ-Mod k

The group ℤ/k

ℤ-Mod-Group : (k : )  Group lzero
pr1 (ℤ-Mod-Group k) = ℤ-Mod-Semigroup k
pr1 (pr1 (pr2 (ℤ-Mod-Group k))) = zero-ℤ-Mod k
pr1 (pr2 (pr1 (pr2 (ℤ-Mod-Group k)))) = left-unit-law-add-ℤ-Mod k
pr2 (pr2 (pr1 (pr2 (ℤ-Mod-Group k)))) = right-unit-law-add-ℤ-Mod k
pr1 (pr2 (pr2 (ℤ-Mod-Group k))) = neg-ℤ-Mod k
pr1 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = left-inverse-law-add-ℤ-Mod k
pr2 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = right-inverse-law-add-ℤ-Mod k

The abelian group ℤ/k

ℤ-Mod-Ab : (k : )  Ab lzero
pr1 (ℤ-Mod-Ab k) = ℤ-Mod-Group k
pr2 (ℤ-Mod-Ab k) = commutative-add-ℤ-Mod k

See also

Recent changes