# Powers of elements in monoids ```agda module group-theory.powers-of-elements-monoids where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea The **power operation** on a [monoid](group-theory.monoids.md) is the map `n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md) multiplying `x` with itself `n` times. ## Definitions ### Powers of elements of monoids ```agda 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](foundation.existential-quantification.md) a number `n` such that `xⁿ = y`. ```agda 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` ```agda 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` ```agda 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ⁿ` ```agda 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 ```agda module _ {l : Level} (M : Monoid l) where distributive-power-add-Monoid : (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) distributive-power-add-Monoid m zero-ℕ {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 ```agda 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` ```agda 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 ```agda 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 ```agda 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)) ```