# Exponents of abelian groups

Content created by Egbert Rijke and Gregor Perčič.

Created on 2023-09-21.

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)