Exponents of groups

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

Created on 2023-09-21.
Last modified on 2023-11-24.

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))

Recent changes