# Powers of elements in monoids

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

Created on 2023-08-21.

module group-theory.powers-of-elements-monoids 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.existential-quantification
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.homomorphisms-monoids
open import group-theory.monoids


## Idea

The power operation on a monoid is the map n x ↦ xⁿ, which is defined by iteratively multiplying x with itself n times.

## Definitions

### Powers of elements of monoids

module _
{l : Level} (M : Monoid l)
where

power-Monoid : ℕ → type-Monoid M → type-Monoid M
power-Monoid zero-ℕ x = unit-Monoid M
power-Monoid (succ-ℕ zero-ℕ) x = x
power-Monoid (succ-ℕ (succ-ℕ n)) x =
mul-Monoid M (power-Monoid (succ-ℕ n) x) x


### The predicate of being a power of an element of a monoid

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} (M : Monoid l)
where

is-power-of-element-prop-Monoid : (x y : type-Monoid M) → Prop l
is-power-of-element-prop-Monoid x y =
exists-structure-Prop ℕ (λ n → power-Monoid M n x ＝ y)

is-power-of-element-Monoid : (x y : type-Monoid M) → UU l
is-power-of-element-Monoid x y =
type-Prop (is-power-of-element-prop-Monoid x y)

is-prop-is-power-of-element-Monoid :
(x y : type-Monoid M) → is-prop (is-power-of-element-Monoid x y)
is-prop-is-power-of-element-Monoid x y =
is-prop-type-Prop (is-power-of-element-prop-Monoid x y)


## Properties

### 1ⁿ ＝ 1

module _
{l : Level} (M : Monoid l)
where

power-unit-Monoid :
(n : ℕ) →
power-Monoid M n (unit-Monoid M) ＝ unit-Monoid M
power-unit-Monoid zero-ℕ = refl
power-unit-Monoid (succ-ℕ zero-ℕ) = refl
power-unit-Monoid (succ-ℕ (succ-ℕ n)) =
right-unit-law-mul-Monoid M _ ∙ power-unit-Monoid (succ-ℕ n)


### xⁿ⁺¹ = xⁿx

module _
{l : Level} (M : Monoid l)
where

power-succ-Monoid :
(n : ℕ) (x : type-Monoid M) →
power-Monoid M (succ-ℕ n) x ＝ mul-Monoid M (power-Monoid M n x) x
power-succ-Monoid zero-ℕ x = inv (left-unit-law-mul-Monoid M x)
power-succ-Monoid (succ-ℕ n) x = refl


### xⁿ⁺¹ ＝ xxⁿ

module _
{l : Level} (M : Monoid l)
where

power-succ-Monoid' :
(n : ℕ) (x : type-Monoid M) →
power-Monoid M (succ-ℕ n) x ＝ mul-Monoid M x (power-Monoid M n x)
power-succ-Monoid' zero-ℕ x = inv (right-unit-law-mul-Monoid M x)
power-succ-Monoid' (succ-ℕ zero-ℕ) x = refl
power-succ-Monoid' (succ-ℕ (succ-ℕ n)) x =
( ap (mul-Monoid' M x) (power-succ-Monoid' (succ-ℕ n) x)) ∙
( associative-mul-Monoid M x (power-Monoid M (succ-ℕ n) x) x)


### Powers by sums of natural numbers are products of powers

module _
{l : Level} (M : Monoid l)
where

(m n : ℕ) {x : type-Monoid M} →
power-Monoid M (m +ℕ n) x ＝
mul-Monoid M (power-Monoid M m x) (power-Monoid M n x)
inv
( right-unit-law-mul-Monoid M
( power-Monoid M m x))
distributive-power-add-Monoid m (succ-ℕ n) {x} =
( power-succ-Monoid M (m +ℕ n) x) ∙
( ap (mul-Monoid' M x) (distributive-power-add-Monoid m n)) ∙
( associative-mul-Monoid M
( power-Monoid M m x)
( power-Monoid M n x)
( x)) ∙
( ap
( mul-Monoid M (power-Monoid M m x))
( inv (power-succ-Monoid M n x)))


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

module _
{l : Level} (M : Monoid l)
where

commute-powers-Monoid' :
(n : ℕ) {x y : type-Monoid M} →
( mul-Monoid M x y ＝ mul-Monoid M y x) →
( mul-Monoid M (power-Monoid M n x) y) ＝
( mul-Monoid M y (power-Monoid M n x))
commute-powers-Monoid' zero-ℕ H =
left-unit-law-mul-Monoid M _ ∙ inv (right-unit-law-mul-Monoid M _)
commute-powers-Monoid' (succ-ℕ zero-ℕ) {x} {y} H = H
commute-powers-Monoid' (succ-ℕ (succ-ℕ n)) {x} {y} H =
( associative-mul-Monoid M (power-Monoid M (succ-ℕ n) x) x y) ∙
( ap (mul-Monoid M (power-Monoid M (succ-ℕ n) x)) H) ∙
( inv (associative-mul-Monoid M (power-Monoid M (succ-ℕ n) x) y x)) ∙
( ap (mul-Monoid' M x) (commute-powers-Monoid' (succ-ℕ n) H)) ∙
( associative-mul-Monoid M y (power-Monoid M (succ-ℕ n) x) x)

commute-powers-Monoid :
(m n : ℕ) {x y : type-Monoid M} →
( mul-Monoid M x y ＝ mul-Monoid M y x) →
( mul-Monoid M
( power-Monoid M m x)
( power-Monoid M n y)) ＝
( mul-Monoid M
( power-Monoid M n y)
( power-Monoid M m x))
commute-powers-Monoid zero-ℕ zero-ℕ H = refl
commute-powers-Monoid zero-ℕ (succ-ℕ n) H =
( left-unit-law-mul-Monoid M (power-Monoid M (succ-ℕ n) _)) ∙
( inv (right-unit-law-mul-Monoid M (power-Monoid M (succ-ℕ n) _)))
commute-powers-Monoid (succ-ℕ m) zero-ℕ H =
( right-unit-law-mul-Monoid M (power-Monoid M (succ-ℕ m) _)) ∙
( inv (left-unit-law-mul-Monoid M (power-Monoid M (succ-ℕ m) _)))
commute-powers-Monoid (succ-ℕ m) (succ-ℕ n) {x} {y} H =
( ap-mul-Monoid M (power-succ-Monoid M m x) (power-succ-Monoid M n y)) ∙
( associative-mul-Monoid M
( power-Monoid M m x)
( x)
( mul-Monoid M (power-Monoid M n y) y)) ∙
( ap
( mul-Monoid M (power-Monoid M m x))
( ( inv (associative-mul-Monoid M x (power-Monoid M n y) y)) ∙
( ap
( mul-Monoid' M y)
( inv (commute-powers-Monoid' n (inv H)))) ∙
( associative-mul-Monoid M (power-Monoid M n y) x y) ∙
( ap (mul-Monoid M (power-Monoid M n y)) H) ∙
( inv (associative-mul-Monoid M (power-Monoid M n y) y x)))) ∙
( inv
( associative-mul-Monoid M
( power-Monoid M m x)
( mul-Monoid M (power-Monoid M n y) y)
( x))) ∙
( ap
( mul-Monoid' M x)
( ( inv
( associative-mul-Monoid M
( power-Monoid M m x)
( power-Monoid M n y)
( y))) ∙
( ap
( mul-Monoid' M y)
( commute-powers-Monoid m n H)) ∙
( associative-mul-Monoid M
( power-Monoid M n y)
( power-Monoid M m x)
( y)) ∙
( ap
( mul-Monoid M (power-Monoid M n y))
( commute-powers-Monoid' m H)) ∙
( inv
( associative-mul-Monoid M
( power-Monoid M n y)
( y)
( power-Monoid M m x))) ∙
( ap
( mul-Monoid' M (power-Monoid M m x))
( inv (power-succ-Monoid M n y))))) ∙
( associative-mul-Monoid M
( power-Monoid M (succ-ℕ n) y)
( power-Monoid M m x)
( x)) ∙
( ap
( mul-Monoid M (power-Monoid M (succ-ℕ n) y))
( inv (power-succ-Monoid M m x)))


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

module _
{l : Level} (M : Monoid l)
where

distributive-power-mul-Monoid :
(n : ℕ) {x y : type-Monoid M} →
(H : mul-Monoid M x y ＝ mul-Monoid M y x) →
power-Monoid M n (mul-Monoid M x y) ＝
mul-Monoid M (power-Monoid M n x) (power-Monoid M n y)
distributive-power-mul-Monoid zero-ℕ H =
inv (left-unit-law-mul-Monoid M (unit-Monoid M))
distributive-power-mul-Monoid (succ-ℕ n) {x} {y} H =
( power-succ-Monoid M n (mul-Monoid M x y)) ∙
( ap
( mul-Monoid' M (mul-Monoid M x y))
( distributive-power-mul-Monoid n H)) ∙
( inv
( associative-mul-Monoid M
( mul-Monoid M (power-Monoid M n x) (power-Monoid M n y))
( x)
( y))) ∙
( ap
( mul-Monoid' M y)
( ( associative-mul-Monoid M
( power-Monoid M n x)
( power-Monoid M n y)
( x)) ∙
( ap
( mul-Monoid M (power-Monoid M n x))
( commute-powers-Monoid' M n (inv H))) ∙
( inv
( associative-mul-Monoid M
( power-Monoid M n x)
( x)
( power-Monoid M n y))))) ∙
( associative-mul-Monoid M
( mul-Monoid M (power-Monoid M n x) x)
( power-Monoid M n y)
( y)) ∙
( ap-mul-Monoid M
( inv (power-succ-Monoid M n x))
( inv (power-succ-Monoid M n y)))


### Powers by products of natural numbers are iterated powers

module _
{l : Level} (M : Monoid l)
where

power-mul-Monoid :
(m n : ℕ) {x : type-Monoid M} →
power-Monoid M (m *ℕ n) x ＝
power-Monoid M n (power-Monoid M m x)
power-mul-Monoid zero-ℕ n {x} =
inv (power-unit-Monoid M n)
power-mul-Monoid (succ-ℕ zero-ℕ) n {x} =
ap (λ t → power-Monoid M t x) (left-unit-law-add-ℕ n)
power-mul-Monoid (succ-ℕ (succ-ℕ m)) n {x} =
( distributive-power-add-Monoid M (succ-ℕ m *ℕ n) n) ∙
( ap
( mul-Monoid' M (power-Monoid M n x))
( power-mul-Monoid (succ-ℕ m) n)) ∙
( inv
( distributive-power-mul-Monoid M n
( commute-powers-Monoid' M (succ-ℕ m) refl)))


### Monoid homomorphisms preserve powers

module _
{l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : hom-Monoid M N)
where

preserves-powers-hom-Monoid :
(n : ℕ) (x : type-Monoid M) →
map-hom-Monoid M N f (power-Monoid M n x) ＝
power-Monoid N n (map-hom-Monoid M N f x)
preserves-powers-hom-Monoid zero-ℕ x = preserves-unit-hom-Monoid M N f
preserves-powers-hom-Monoid (succ-ℕ zero-ℕ) x = refl
preserves-powers-hom-Monoid (succ-ℕ (succ-ℕ n)) x =
( preserves-mul-hom-Monoid M N f) ∙
( ap (mul-Monoid' N _) (preserves-powers-hom-Monoid (succ-ℕ n) x))