# Powers of elements in semirings

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Maša Žaucer.

Created on 2023-02-20.

module ring-theory.powers-of-elements-semirings 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.identity-types
open import foundation.universe-levels

open import group-theory.powers-of-elements-monoids

open import ring-theory.semirings


## Idea

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

## Definition

power-Semiring :
{l : Level} (R : Semiring l) → ℕ → type-Semiring R → type-Semiring R
power-Semiring R n x = power-Monoid (multiplicative-monoid-Semiring R) n x


## Properties

### 1ⁿ ＝ 1

module _
{l : Level} (R : Semiring l)
where

power-one-Semiring :
(n : ℕ) → power-Semiring R n (one-Semiring R) ＝ one-Semiring R
power-one-Semiring = power-unit-Monoid (multiplicative-monoid-Semiring R)


### xⁿ⁺¹ = xⁿx

module _
{l : Level} (R : Semiring l)
where

power-succ-Semiring :
(n : ℕ) (x : type-Semiring R) →
power-Semiring R (succ-ℕ n) x ＝ mul-Semiring R (power-Semiring R n x) x
power-succ-Semiring = power-succ-Monoid (multiplicative-monoid-Semiring R)


### xⁿ⁺¹ ＝ xxⁿ

module _
{l : Level} (R : Semiring l)
where

power-succ-Semiring' :
(n : ℕ) (x : type-Semiring R) →
power-Semiring R (succ-ℕ n) x ＝ mul-Semiring R x (power-Semiring R n x)
power-succ-Semiring' = power-succ-Monoid' (multiplicative-monoid-Semiring R)


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

module _
{l : Level} (R : Semiring l)
where

(m n : ℕ) {x : type-Semiring R} →
power-Semiring R (m +ℕ n) x ＝
mul-Semiring R (power-Semiring R m x) (power-Semiring R n x)


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

module _
{l : Level} (R : Semiring l)
where

commute-powers-Semiring' :
(n : ℕ) {x y : type-Semiring R} →
( mul-Semiring R x y ＝ mul-Semiring R y x) →
( mul-Semiring R (power-Semiring R n x) y) ＝
( mul-Semiring R y (power-Semiring R n x))
commute-powers-Semiring' =
commute-powers-Monoid' (multiplicative-monoid-Semiring R)

commute-powers-Semiring :
(m n : ℕ) {x y : type-Semiring R} →
( mul-Semiring R x y ＝ mul-Semiring R y x) →
( mul-Semiring R
( power-Semiring R m x)
( power-Semiring R n y)) ＝
( mul-Semiring R
( power-Semiring R n y)
( power-Semiring R m x))
commute-powers-Semiring =
commute-powers-Monoid (multiplicative-monoid-Semiring R)


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

module _
{l : Level} (R : Semiring l)
where

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


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

module _
{l : Level} (R : Semiring l)
where

power-mul-Semiring :
(m n : ℕ) {x : type-Semiring R} →
power-Semiring R (m *ℕ n) x ＝ power-Semiring R n (power-Semiring R m x)
power-mul-Semiring = power-mul-Monoid (multiplicative-monoid-Semiring R)