# Integer powers of elements of groups

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

Created on 2023-09-10.

module group-theory.integer-powers-of-elements-groups where

Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.iterating-automorphisms
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-groups

open import structured-types.initial-pointed-type-equipped-with-automorphism


## Idea

The integer power operation on a group is the map k x ↦ xᵏ, which is defined by iteratively multiplying x with itself an integer k times.

## Definitions

### Iteratively multiplication by g

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

iterative-multiplication-by-element-Group :
type-Group G → ℤ → type-Group G → type-Group G
iterative-multiplication-by-element-Group g k =
map-iterate-automorphism-ℤ k (equiv-mul-Group G g)


### Integer powers of group elements

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

integer-power-Group : ℤ → type-Group G → type-Group G
integer-power-Group k g =
map-iterate-automorphism-ℤ k (equiv-mul-Group G g) (unit-Group G)


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

We say that an element y is an integer power of an element x if there exists an integer k such that xᵏ ＝ y.

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

is-integer-power-of-element-prop-Group :
(x y : type-Group G) → Prop l
is-integer-power-of-element-prop-Group x y =
exists-structure-Prop ℤ (λ k → integer-power-Group G k x ＝ y)

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

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


## Properties

### Associativity of iterated multiplication by a group element

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

associative-iterative-multiplication-by-element-Group :
(k : ℤ) (h1 h2 : type-Group G) →
iterative-multiplication-by-element-Group G g k (mul-Group G h1 h2) ＝
mul-Group G (iterative-multiplication-by-element-Group G g k h1) h2
associative-iterative-multiplication-by-element-Group
( inl zero-ℕ) h1 h2 =
inv (associative-mul-Group G (inv-Group G g) h1 h2)
associative-iterative-multiplication-by-element-Group
( inl (succ-ℕ x)) h1 h2 =
( ap
( mul-Group G (inv-Group G g))
( associative-iterative-multiplication-by-element-Group
( inl x)
( h1)
( h2))) ∙
( inv
( associative-mul-Group G
( inv-Group G g)
( iterative-multiplication-by-element-Group G g (inl x) h1)
( h2)))
associative-iterative-multiplication-by-element-Group
( inr (inl _)) h1 h2 =
refl
associative-iterative-multiplication-by-element-Group
( inr (inr zero-ℕ)) h1 h2 =
inv (associative-mul-Group G g h1 h2)
associative-iterative-multiplication-by-element-Group
( inr (inr (succ-ℕ x))) h1 h2 =
( ap
( mul-Group G g)
( associative-iterative-multiplication-by-element-Group
( inr (inr x))
( h1)
( h2))) ∙
( inv
( associative-mul-Group G g
( iterative-multiplication-by-element-Group G g (inr (inr x)) h1)
( h2)))


### integer-power-Group G (int-ℕ n) g ＝ power-Group G n g

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

integer-power-int-Group :
(n : ℕ) (g : type-Group G) →
integer-power-Group G (int-ℕ n) g ＝ power-Group G n g
integer-power-int-Group zero-ℕ g = refl
integer-power-int-Group (succ-ℕ zero-ℕ) g = right-unit-law-mul-Group G g
integer-power-int-Group (succ-ℕ (succ-ℕ n)) g =
( ap (mul-Group G g) (integer-power-int-Group (succ-ℕ n) g)) ∙
( inv (power-succ-Group' G (succ-ℕ n) g))

integer-power-in-pos-Group :
(n : ℕ) (g : type-Group G) →
integer-power-Group G (in-pos-ℤ n) g ＝
power-Group G (succ-ℕ n) g
integer-power-in-pos-Group n g = integer-power-int-Group (succ-ℕ n) g

integer-power-in-neg-Group :
(n : ℕ) (g : type-Group G) →
integer-power-Group G (in-neg-ℤ n) g ＝
inv-Group G (power-Group G (succ-ℕ n) g)
integer-power-in-neg-Group zero-ℕ g =
right-unit-law-mul-Group G (inv-Group G g)
integer-power-in-neg-Group (succ-ℕ n) g =
( ap (mul-Group G (inv-Group G g)) (integer-power-in-neg-Group n g)) ∙
( inv (distributive-inv-mul-Group G)) ∙
( ap (inv-Group G) (power-succ-Group G (succ-ℕ n) g))


### The integer power x⁰ is the unit of the group

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

integer-power-zero-Group :
integer-power-Group G zero-ℤ g ＝ unit-Group G
integer-power-zero-Group =
preserves-point-map-ℤ-Pointed-Type-With-Aut
( pointed-type-with-aut-Group G g)


### x¹ ＝ x

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

integer-power-one-Group :
integer-power-Group G one-ℤ g ＝ g
integer-power-one-Group = right-unit-law-mul-Group G g


### The integer power x⁻¹ is the inverse of x

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

integer-power-neg-one-Group :
integer-power-Group G neg-one-ℤ g ＝ inv-Group G g
integer-power-neg-one-Group = right-unit-law-mul-Group G (inv-Group G g)


### The integer power gˣ⁺ʸ computes to gˣgʸ

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

(x y : ℤ) →
integer-power-Group G (x +ℤ y) g ＝
mul-Group G
( integer-power-Group G x g)
( integer-power-Group G y g)
distributive-integer-power-add-Group x y =
( iterate-automorphism-add-ℤ x y (equiv-mul-Group G g) (unit-Group G)) ∙
( ap
( iterative-multiplication-by-element-Group G g x)
( inv (left-unit-law-mul-Group G (integer-power-Group G y g)))) ∙
( associative-iterative-multiplication-by-element-Group G g x
( unit-Group G)
( integer-power-Group G y g))


### The integer power x⁻ᵏ is the inverse of the integer power xᵏ

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

integer-power-neg-Group :
(k : ℤ) (x : type-Group G) →
integer-power-Group G (neg-ℤ k) x ＝ inv-Group G (integer-power-Group G k x)
integer-power-neg-Group (inl k) x =
transpose-eq-inv-Group G
( ( ap (inv-Group G) (integer-power-in-pos-Group G k x)) ∙
( inv (integer-power-in-neg-Group G k x)))
integer-power-neg-Group (inr (inl _)) x =
integer-power-zero-Group G x ∙ inv (inv-unit-Group G)
integer-power-neg-Group (inr (inr k)) x =
( integer-power-in-neg-Group G k x) ∙
( ap (inv-Group G) (inv (integer-power-in-pos-Group G k x)))


### xᵏ⁺¹ = xᵏx and xᵏ⁺¹ = xxᵏ

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

integer-power-succ-Group :
(k : ℤ) (x : type-Group G) →
integer-power-Group G (succ-ℤ k) x ＝
mul-Group G (integer-power-Group G k x) x
integer-power-succ-Group k x =
( ap (λ t → integer-power-Group G t x) (is-right-add-one-succ-ℤ k)) ∙
( distributive-integer-power-add-Group G x k one-ℤ) ∙
( ap (mul-Group G _) (integer-power-one-Group G x))

integer-power-succ-Group' :
(k : ℤ) (x : type-Group G) →
integer-power-Group G (succ-ℤ k) x ＝
mul-Group G x (integer-power-Group G k x)
integer-power-succ-Group' k x =
( ap (λ t → integer-power-Group G t x) (is-left-add-one-succ-ℤ k)) ∙
( distributive-integer-power-add-Group G x one-ℤ k) ∙
( ap (mul-Group' G _) (integer-power-one-Group G x))


### xᵏ⁻¹ = xᵏx⁻¹ and xᵏ⁻¹ = x⁻¹xᵏ

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

private

infixl 45 _*_
_*_ = mul-Group G

pwr = integer-power-Group G

infixr 50 _^_
_^_ : (x : type-Group G) (k : ℤ) → type-Group G
_^_ x k = integer-power-Group G k x

infix 55 _⁻¹
_⁻¹ = inv-Group G

integer-power-pred-Group :
(k : ℤ) (x : type-Group G) → x ^ (pred-ℤ k) ＝ x ^ k * x ⁻¹
integer-power-pred-Group k x =
( ap (x ^_) (is-right-add-neg-one-pred-ℤ k)) ∙
( distributive-integer-power-add-Group G x k neg-one-ℤ) ∙
( ap ((x ^ k) *_) (integer-power-neg-one-Group G x))

integer-power-pred-Group' :
(k : ℤ) (x : type-Group G) → x ^ (pred-ℤ k) ＝ x ⁻¹ * x ^ k
integer-power-pred-Group' k x =
( ap (x ^_) (is-left-add-neg-one-pred-ℤ k)) ∙
( distributive-integer-power-add-Group G x neg-one-ℤ k) ∙
( ap (_* (x ^ k)) (integer-power-neg-one-Group G x))


### 1ᵏ ＝ 1

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

integer-power-unit-Group :
(k : ℤ) → integer-power-Group G k (unit-Group G) ＝ unit-Group G
integer-power-unit-Group (inl zero-ℕ) =
integer-power-neg-one-Group G (unit-Group G) ∙ inv-unit-Group G
integer-power-unit-Group (inl (succ-ℕ k)) =
( ap-mul-Group G (inv-unit-Group G) (integer-power-unit-Group (inl k))) ∙
( left-unit-law-mul-Group G (unit-Group G))
integer-power-unit-Group (inr (inl _)) = refl
integer-power-unit-Group (inr (inr zero-ℕ)) =
integer-power-one-Group G (unit-Group G)
integer-power-unit-Group (inr (inr (succ-ℕ k))) =
left-unit-law-mul-Group G _ ∙ integer-power-unit-Group (inr (inr k))


### If x commutes with y then so do their integer powers

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

private

infixl 45 _*_
_*_ = mul-Group G

pwr = integer-power-Group G

infixr 50 _^_
_^_ : (x : type-Group G) (k : ℤ) → type-Group G
_^_ x k = integer-power-Group G k x

infix 55 _⁻¹
_⁻¹ = inv-Group G

commute-integer-powers-Group' :
(k : ℤ) {x y : type-Group G} →
commute-Group G x y → commute-Group G x (y ^ k)
commute-integer-powers-Group' (inl zero-ℕ) {x} {y} H =
( ap (x *_) (integer-power-neg-one-Group G y)) ∙
( commute-inv-Group G x y H) ∙
( ap (_* x) (inv (integer-power-neg-one-Group G y)))
commute-integer-powers-Group' (inl (succ-ℕ k)) {x} {y} H =
commute-mul-Group G x
( inv-Group G y)
( integer-power-Group G (inl k) y)
( commute-inv-Group G x y H)
( commute-integer-powers-Group' (inl k) H)
commute-integer-powers-Group' (inr (inl _)) {x} {y} H =
commute-unit-Group G x
commute-integer-powers-Group' (inr (inr zero-ℕ)) {x} {y} H =
( ap (x *_) (integer-power-one-Group G y)) ∙
( H) ∙
( ap (_* x) (inv (integer-power-one-Group G y)))
commute-integer-powers-Group' (inr (inr (succ-ℕ k))) {x} {y} H =
commute-mul-Group G x y
( integer-power-Group G (inr (inr k)) y)
( H)
( commute-integer-powers-Group' (inr (inr k)) H)

commute-integer-powers-Group :
(k l : ℤ) {x y : type-Group G} →
commute-Group G x y → commute-Group G (x ^ k) (y ^ l)
commute-integer-powers-Group (inl zero-ℕ) l {x} {y} H =
( ap (_* (y ^ l)) (integer-power-neg-one-Group G x)) ∙
( inv
( commute-inv-Group G
( y ^ l)
( x)
( inv (commute-integer-powers-Group' l H)))) ∙
( ap ((y ^ l) *_) (inv (integer-power-neg-one-Group G x)))
commute-integer-powers-Group (inl (succ-ℕ k)) l {x} {y} H =
inv
( commute-mul-Group G
( y ^ l)
( inv-Group G x)
( x ^ inl k)
( commute-inv-Group G (y ^ l) x
( inv (commute-integer-powers-Group' l H)))
( inv (commute-integer-powers-Group (inl k) l H)))
commute-integer-powers-Group (inr (inl _)) l {x} {y} H =
inv (commute-unit-Group G (y ^ l))
commute-integer-powers-Group (inr (inr zero-ℕ)) l {x} {y} H =
( ap (_* (y ^ l)) (integer-power-one-Group G x)) ∙
( commute-integer-powers-Group' l H) ∙
( ap ((y ^ l) *_) (inv (integer-power-one-Group G x)))
commute-integer-powers-Group (inr (inr (succ-ℕ k))) l {x} {y} H =
inv
( commute-mul-Group G
( y ^ l)
( x)
( x ^ inr (inr k))
( inv (commute-integer-powers-Group' l H))
( inv (commute-integer-powers-Group (inr (inr k)) l H)))


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

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

private

infixl 45 _*_
_*_ = mul-Group G

pwr = integer-power-Group G

infixr 50 _^_
_^_ : (x : type-Group G) (k : ℤ) → type-Group G
_^_ x k = integer-power-Group G k x

infix 55 _⁻¹
_⁻¹ = inv-Group G

distributive-integer-power-mul-Group :
(k : ℤ) (x y : type-Group G) →
commute-Group G x y → (x * y) ^ k ＝ x ^ k * y ^ k
distributive-integer-power-mul-Group (inl zero-ℕ) x y H =
equational-reasoning
(x * y) ^ neg-one-ℤ
＝ (x * y) ⁻¹
by integer-power-neg-one-Group G (x * y)
＝ x ⁻¹ * y ⁻¹
by distributive-inv-mul-Group' G x y H
＝ x ^ neg-one-ℤ * y ^ neg-one-ℤ
by
inv
( ap-mul-Group G
( integer-power-neg-one-Group G x)
( integer-power-neg-one-Group G y))
distributive-integer-power-mul-Group (inl (succ-ℕ k)) x y H =
equational-reasoning
(x * y) ^ (pred-ℤ (inl k))
＝ (x * y) ^ (inl k) * (x * y) ⁻¹
by integer-power-pred-Group G (inl k) (x * y)
＝ (x ^ (inl k) * y ^ (inl k)) * (x ⁻¹ * y ⁻¹)
by
ap-mul-Group G
( distributive-integer-power-mul-Group (inl k) x y H)
( distributive-inv-mul-Group' G x y H)
＝ (x ^ (inl k) * x ⁻¹) * (y ^ (inl k) * y ⁻¹)
by
interchange-mul-mul-Group G
( double-transpose-eq-mul-Group' G
( commute-integer-powers-Group' G (inl k) H))
＝ (x ^ (pred-ℤ (inl k))) * (y ^ (pred-ℤ (inl k)))
by
ap-mul-Group G
( inv (integer-power-pred-Group G (inl k) x))
( inv (integer-power-pred-Group G (inl k) y))
distributive-integer-power-mul-Group (inr (inl _)) x y H =
inv (left-unit-law-mul-Group G (unit-Group G))
distributive-integer-power-mul-Group (inr (inr zero-ℕ)) x y H =
( integer-power-one-Group G (x * y)) ∙
( inv
( ap-mul-Group G
( integer-power-one-Group G x)
( integer-power-one-Group G y)))
distributive-integer-power-mul-Group (inr (inr (succ-ℕ k))) x y H =
equational-reasoning
(x * y) ^ (succ-ℤ (in-pos-ℤ k))
＝ (x * y) ^ (in-pos-ℤ k) * (x * y)
by integer-power-succ-Group G (in-pos-ℤ k) (x * y)
＝ (x ^ (in-pos-ℤ k) * y ^ (in-pos-ℤ k)) * (x * y)
by
ap
( _* (x * y))
( distributive-integer-power-mul-Group (inr (inr k)) x y H)
＝ (x ^ (in-pos-ℤ k) * x) * (y ^ (in-pos-ℤ k) * y)
by
interchange-mul-mul-Group G
( inv (commute-integer-powers-Group' G (in-pos-ℤ k) H))
＝ x ^ (succ-ℤ (in-pos-ℤ k)) * y ^ (succ-ℤ (in-pos-ℤ k))
by
ap-mul-Group G
( inv (integer-power-succ-Group G (in-pos-ℤ k) x))
( inv (integer-power-succ-Group G (in-pos-ℤ k) y))


### Powers by products of integers are iterated integer powers

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

private

infixl 45 _*_
_*_ = mul-ℤ

pwr = integer-power-Group G

infixr 50 _^_
_^_ : (x : type-Group G) (k : ℤ) → type-Group G
_^_ x k = integer-power-Group G k x

integer-power-mul-Group :
(k l : ℤ) (x : type-Group G) → x ^ (k * l) ＝ (x ^ k) ^ l
integer-power-mul-Group k (inl zero-ℕ) x =
( ap (x ^_) (right-neg-unit-law-mul-ℤ k)) ∙
( integer-power-neg-Group G k x) ∙
( inv (integer-power-neg-one-Group G _))
integer-power-mul-Group k (inl (succ-ℕ l)) x =
equational-reasoning
(x ^ (k * inl (succ-ℕ l)))
＝ x ^ (neg-ℤ k +ℤ (k *ℤ inl l))
by ap (x ^_) (right-predecessor-law-mul-ℤ k (inl l))
＝ mul-Group G (x ^ neg-ℤ k) (x ^ (k * (inl l)))
by distributive-integer-power-add-Group G x (neg-ℤ k) _
＝ mul-Group G ((x ^ k) ^ neg-one-ℤ) ((x ^ k) ^ (inl l))
by
ap-mul-Group G
( ( integer-power-neg-Group G k x) ∙
( inv (integer-power-neg-one-Group G (x ^ k))))
( integer-power-mul-Group k (inl l) x)
＝ (x ^ k) ^ (neg-one-ℤ +ℤ (inl l))
by
inv (distributive-integer-power-add-Group G (x ^ k) neg-one-ℤ (inl l))
＝ (x ^ k) ^ (inl (succ-ℕ l))
by ap ((x ^ k) ^_) (is-left-add-neg-one-pred-ℤ (inl l))
integer-power-mul-Group k (inr (inl _)) x =
ap (x ^_) (right-zero-law-mul-ℤ k)
integer-power-mul-Group k (inr (inr zero-ℕ)) x =
( ap (x ^_) (right-unit-law-mul-ℤ k)) ∙
( inv (integer-power-one-Group G _))
integer-power-mul-Group k (inr (inr (succ-ℕ l))) x =
equational-reasoning
(x ^ (k * succ-ℤ (in-pos-ℤ l)))
＝ x ^ (k +ℤ k * (in-pos-ℤ l))
by ap (x ^_) (right-successor-law-mul-ℤ k (in-pos-ℤ l))
＝ mul-Group G (x ^ k) (x ^ (k * in-pos-ℤ l))
by
distributive-integer-power-add-Group G x k (k * in-pos-ℤ l)
＝ mul-Group G (x ^ k) ((x ^ k) ^ (in-pos-ℤ l))
by
ap (mul-Group G _) (integer-power-mul-Group k (inr (inr l)) x)
＝ (x ^ k) ^ (succ-ℤ (in-pos-ℤ l))
by
inv (integer-power-succ-Group' G (in-pos-ℤ l) (x ^ k))

swap-integer-power-Group :
(k l : ℤ) (x : type-Group G) →
integer-power-Group G k (integer-power-Group G l x) ＝
integer-power-Group G l (integer-power-Group G k x)
swap-integer-power-Group k l x =
( inv (integer-power-mul-Group l k x)) ∙
( ap (λ t → integer-power-Group G t x) (commutative-mul-ℤ l k)) ∙
( integer-power-mul-Group k l x)


### Group homomorphisms preserve integer powers

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

preserves-integer-powers-hom-Group :
(k : ℤ) (x : type-Group G) →
map-hom-Group G H f (integer-power-Group G k x) ＝
integer-power-Group H k (map-hom-Group G H f x)
preserves-integer-powers-hom-Group (inl zero-ℕ) x =
( preserves-mul-hom-Group G H f) ∙
( ap-mul-Group H
( preserves-inv-hom-Group G H f)
( preserves-unit-hom-Group G H f))
preserves-integer-powers-hom-Group (inl (succ-ℕ k)) x =
( preserves-mul-hom-Group G H f) ∙
( ap-mul-Group H
( preserves-inv-hom-Group G H f)
( preserves-integer-powers-hom-Group (inl k) x))
preserves-integer-powers-hom-Group (inr (inl _)) x =
preserves-unit-hom-Group G H f
preserves-integer-powers-hom-Group (inr (inr zero-ℕ)) x =
( preserves-mul-hom-Group G H f) ∙
( ap (mul-Group H (map-hom-Group G H f x)) (preserves-unit-hom-Group G H f))
preserves-integer-powers-hom-Group (inr (inr (succ-ℕ k))) x =
( preserves-mul-hom-Group G H f) ∙
( ap
( mul-Group H (map-hom-Group G H f x))
( preserves-integer-powers-hom-Group (inr (inr k)) x))

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

eq-integer-power-hom-Group :
(g : hom-Group G H) (k : ℤ) (x : type-Group G) →
( map-hom-Group G H f x ＝ map-hom-Group G H g x) →
( map-hom-Group G H f (integer-power-Group G k x) ＝
map-hom-Group G H g (integer-power-Group G k x))
eq-integer-power-hom-Group g k x p =
( preserves-integer-powers-hom-Group G H f k x) ∙
( ap (integer-power-Group H k) p) ∙
( inv (preserves-integer-powers-hom-Group G H g k x))