Powers of elements in groups

Content created by Egbert Rijke, Fredrik Bakke, Louis Wasserman and Gregor Perčič.

Created on 2023-08-21.
Last modified on 2025-10-17.

module group-theory.powers-of-elements-groups where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.commuting-elements-groups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.powers-of-elements-monoids

Idea

The power operation on a group is the map n x ↦ xⁿ, which is defined by iteratively multiplying x with itself n times. This file describes the case where n is a natural number.

Definition

Powers by natural numbers of group elements

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

  power-Group : ℕ → type-Group G → type-Group G
  power-Group = power-Monoid (monoid-Group G)

The predicate of being a power of an element in a group

We say that an element y is a power of an element x if there exists a number n such that xⁿ ＝ y.

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

  is-power-of-element-prop-Group :
    (x y : type-Group G) → Prop l
  is-power-of-element-prop-Group =
    is-power-of-element-prop-Monoid (monoid-Group G)

  is-power-of-element-Group :
    (x y : type-Group G) → UU l
  is-power-of-element-Group =
    is-power-of-element-Monoid (monoid-Group G)

  is-prop-is-power-of-element-Group :
    (x y : type-Group G) →
    is-prop (is-power-of-element-Group x y)
  is-prop-is-power-of-element-Group =
    is-prop-is-power-of-element-Monoid (monoid-Group G)

Properties

1ⁿ ＝ 1

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

  power-unit-Group :
    (n : ℕ) → power-Group G n (unit-Group G) ＝ unit-Group G
  power-unit-Group = power-unit-Monoid (monoid-Group G)

xⁿ⁺¹ = xⁿx

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

  power-succ-Group :
    (n : ℕ) (x : type-Group G) →
    power-Group G (succ-ℕ n) x ＝ mul-Group G (power-Group G n x) x
  power-succ-Group = power-succ-Monoid (monoid-Group G)

xⁿ⁺¹ ＝ xxⁿ

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

  power-succ-Group' :
    (n : ℕ) (x : type-Group G) →
    power-Group G (succ-ℕ n) x ＝ mul-Group G x (power-Group G n x)
  power-succ-Group' = power-succ-Monoid' (monoid-Group G)

Powers by sums of natural numbers are products of powers

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

  distributive-power-add-Group :
    (m n : ℕ) {x : type-Group G} →
    power-Group G (m +ℕ n) x ＝
    mul-Group G (power-Group G m x) (power-Group G n x)
  distributive-power-add-Group = distributive-power-add-Monoid (monoid-Group G)

If x commutes with y then so do their powers

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

  commute-powers-Group' :
    (n : ℕ) {x y : type-Group G} →
    commute-Group G x y → commute-Group G (power-Group G n x) y
  commute-powers-Group' = commute-powers-Monoid' (monoid-Group G)

  commute-powers-Group :
    (m n : ℕ) {x y : type-Group G} →
    commute-Group G x y →
    commute-Group G (power-Group G m x) (power-Group G n y)
  commute-powers-Group = commute-powers-Monoid (monoid-Group G)

If x commutes with y, then powers distribute over the product of x and y

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

  distributive-power-mul-Group :
    (n : ℕ) {x y : type-Group G} →
    (H : mul-Group G x y ＝ mul-Group G y x) →
    power-Group G n (mul-Group G x y) ＝
    mul-Group G (power-Group G n x) (power-Group G n y)
  distributive-power-mul-Group =
    distributive-power-mul-Monoid (monoid-Group G)

Powers by products of natural numbers are iterated powers

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

  power-mul-Group :
    (m n : ℕ) {x : type-Group G} →
    power-Group G (m *ℕ n) x ＝ power-Group G n (power-Group G m x)
  power-mul-Group = power-mul-Monoid (monoid-Group G)

The inverse of x, raised to the power n, is the inverse of x raised to the power n

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

  abstract
    power-inv-Group :
      (n : ℕ) (x : type-Group G) →
      power-Group G n (inv-Group G x) ＝ inv-Group G (power-Group G n x)
    power-inv-Group 0 _ = inv (inv-unit-Group G)
    power-inv-Group 1 _ = refl
    power-inv-Group (succ-ℕ n@(succ-ℕ _)) x =
      equational-reasoning
        mul-Group G (power-Group G n (inv-Group G x)) (inv-Group G x)
        ＝ mul-Group G (inv-Group G (power-Group G n x)) (inv-Group G x)
          by ap-mul-Group G (power-inv-Group n x) refl
        ＝ inv-Group G (mul-Group G x (power-Group G n x))
          by inv (distributive-inv-mul-Group G)
        ＝ inv-Group G (power-Group G (succ-ℕ n) x)
          by ap (inv-Group G) (inv (power-succ-Group' G n x))

Group homomorphisms preserve powers

module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  where

  preserves-powers-hom-Group :
    (n : ℕ) (x : type-Group G) →
    map-hom-Group G H f (power-Group G n x) ＝
    power-Group H n (map-hom-Group G H f x)
  preserves-powers-hom-Group =
    preserves-powers-hom-Monoid
      ( monoid-Group G)
      ( monoid-Group H)
      ( hom-monoid-hom-Group G H f)

See also

Recent changes