# Exponents of groups

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

Created on 2023-09-21.

module group-theory.exponents-groups where

Imports
open import elementary-number-theory.group-of-integers

open import foundation.universe-levels

open import group-theory.free-groups-with-one-generator
open import group-theory.groups
open import group-theory.intersections-subgroups-groups
open import group-theory.kernels-homomorphisms-groups
open import group-theory.subgroups


The exponent exp G of a group G is the intersection of the kernels of the group homomorphisms

  hom-element-Group G g : ℤ → G


indexed by all elements g : G. In other words, the exponent of G is the subgroup K of ℤ consisting of all integers k such that the integer power gᵏ ＝ 1 for every group element g.

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 G. In constructive mathematics, however, such an integer is not always well-defined.

## Definitions

### The exponent of a group

module _
{l : Level} (G : Group l)
where

exponent-Group : Subgroup l ℤ-Group
exponent-Group =
intersection-family-of-subgroups-Group ℤ-Group
( λ (g : type-Group G) →
subgroup-kernel-hom-Group ℤ-Group G (hom-element-Group G g))