This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Exponents of abelian groups

module group-theory.exponents-abelian-groups where
Imports 
open import elementary-number-theory.group-of-integers

open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.exponents-groups
open import group-theory.subgroups-abelian-groups

The exponent exp A of an abelian group A is the intersection of the kernels of the group homomorphisms

  hom-element-Group (group-Ab A) a : ℤ → A

indexed by all elements a : A. In other words, the exponent of A is the subgroup K of ℤ consisting of all integers k such that the integer multiple kx ＝ 1 for every group element x.

Note that our conventions are slightly different from the conventions in classical mathematics, where the exponent is taken to be the positive integer k that generates the subgroup of ℤ that we call the exponent of A. In constructive mathematics, however, such an integer is not always well-defined.

Definitions

The exponent of an abelian group

module _
  {l : Level} (A : Ab l)
  where

  exponent-Ab : Subgroup-Ab l ℤ-Ab
  exponent-Ab = exponent-Group (group-Ab A)