This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
The standard cyclic groups
module elementary-number-theory.standard-cyclic-groups where
Imports
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
Idea
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.
Definitions
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