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
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
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).