The order of an element in a group

Content created by Jonathan Prieto-Cubides, Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2022-08-18.
Last modified on 2025-10-31.

module group-theory.orders-of-elements-groups where
Imports 
open import elementary-number-theory.group-of-integers
open import elementary-number-theory.integers

open import foundation.universe-levels

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

Idea

For each element g : G of a group G we have a unique group homomorphism f : ℤ → G such that f 1 = g. The order of g is defined to be the kernel of this group homomorphism f. Since kernels are ordered by inclusion, it follows that the orders of elements of a group are ordered by reversed inclusion.

If the group G has decidable equality, then we can reduce the order of g to a natural number. In this case, the orders of elements of G are ordered by divisibility.

If the unique group homomorphism f : ℤ → G such that f 1 = g is injective, and G has decidable equality, then the order of g is set to be 0, which is a consequence of the point of view that orders are normal subgroups of ℤ.

Definitions

The order of an element in a group

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

  order-element-Group : Normal-Subgroup l ℤ-Group
  order-element-Group =
    kernel-hom-Group ℤ-Group G (hom-element-Group G g)

  subgroup-order-element-Group : Subgroup l ℤ-Group
  subgroup-order-element-Group =
    subgroup-kernel-hom-Group ℤ-Group G (hom-element-Group G g)

  subset-order-element-Group : subset-Group l ℤ-Group
  subset-order-element-Group =
    subset-kernel-hom-Group ℤ-Group G (hom-element-Group G g)

  is-in-order-element-Group : ℤ → UU l
  is-in-order-element-Group =
    is-in-kernel-hom-Group ℤ-Group G (hom-element-Group G g)

Divisibility of orders of elements of a group

We say that the order of x divides the order of y if the normal subgroup order-element-Group G y is contained in the normal subgroup order-elemetn-Group G x. In other words, the order of x divides the order of y if for every integer k such that yᵏ ＝ e we have xᵏ ＝ e.

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

  div-order-element-Group : (x y : type-Group G) → UU l
  div-order-element-Group x y =
    leq-Normal-Subgroup
      ( ℤ-Group)
      ( order-element-Group G y)
      ( order-element-Group G x)

Recent changes