Powers of elements in rings

module ring-theory.powers-of-elements-rings where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.parity-natural-numbers

open import foundation.empty-types
open import foundation.functions
open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.central-elements-rings
open import ring-theory.powers-of-elements-semirings
open import ring-theory.rings

Idea

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

Definition

power-Ring : {l : Level} (R : Ring l)    type-Ring R  type-Ring R
power-Ring R = power-Semiring (semiring-Ring R)

Properties

xⁿ⁺¹ = xⁿx

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

  power-succ-Ring :
    (n : ) (x : type-Ring R) 
    power-Ring R (succ-ℕ n) x  mul-Ring R (power-Ring R n x) x
  power-succ-Ring = power-succ-Semiring (semiring-Ring R)

Powers by sums of natural numbers are products of powers

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

  power-add-Ring :
    (m n : ) {x : type-Ring R} 
    power-Ring R (m +ℕ n) x 
    mul-Ring R (power-Ring R m x) (power-Ring R n x)
  power-add-Ring = power-add-Semiring (semiring-Ring R)

If x commutes with y then so do their powers

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

  commute-powers-Ring' :
    (n : ) {x y : type-Ring R} 
    ( mul-Ring R x y  mul-Ring R y x) 
    ( mul-Ring R (power-Ring R n x) y) 
    ( mul-Ring R y (power-Ring R n x))
  commute-powers-Ring' = commute-powers-Semiring' (semiring-Ring R)

  commute-powers-Ring :
    (m n : ) {x y : type-Ring R}  mul-Ring R x y  mul-Ring R y x 
    ( mul-Ring R (power-Ring R m x) (power-Ring R n y)) 
    ( mul-Ring R (power-Ring R n y) (power-Ring R m x))
  commute-powers-Ring = commute-powers-Semiring (semiring-Ring R)

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

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

  distributive-power-mul-Ring :
    (n : ) {x y : type-Ring R}  mul-Ring R x y  mul-Ring R y x 
    power-Ring R n (mul-Ring R x y) 
    mul-Ring R (power-Ring R n x) (power-Ring R n y)
  distributive-power-mul-Ring =
    distributive-power-mul-Semiring (semiring-Ring R)

(-x)ⁿ = (-1)ⁿxⁿ

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

  power-neg-Ring :
    (n : ) (x : type-Ring R) 
    power-Ring R n (neg-Ring R x) 
    mul-Ring R (power-Ring R n (neg-one-Ring R)) (power-Ring R n x)
  power-neg-Ring n x =
    ( ap (power-Ring R n) (inv (mul-neg-one-Ring R x))) 
    ( distributive-power-mul-Ring R n (is-central-element-neg-one-Ring R x))

  even-power-neg-Ring :
    (n : ) (x : type-Ring R) 
    is-even-ℕ n  power-Ring R n (neg-Ring R x)  power-Ring R n x
  even-power-neg-Ring zero-ℕ x H = refl
  even-power-neg-Ring (succ-ℕ zero-ℕ) x H = ex-falso (is-odd-one-ℕ H)
  even-power-neg-Ring (succ-ℕ (succ-ℕ n)) x H =
    ( right-negative-law-mul-Ring R
      ( power-Ring R (succ-ℕ n) (neg-Ring R x))
      ( x)) 
    ( ( ap
        ( neg-Ring R)
        ( ( ap
            ( mul-Ring' R x)
            ( ( power-succ-Ring R n (neg-Ring R x)) 
              ( ( right-negative-law-mul-Ring R
                  ( power-Ring R n (neg-Ring R x))
                  ( x)) 
                ( ap
                  ( neg-Ring R)
                  ( ( ap
                      ( mul-Ring' R x)
                      ( even-power-neg-Ring n x
                        ( is-even-is-even-succ-succ-ℕ n H))) 
                    ( inv (power-succ-Ring R n x))))))) 
          ( left-negative-law-mul-Ring R (power-Ring R (succ-ℕ n) x) x))) 
      ( neg-neg-Ring R (power-Ring R (succ-ℕ (succ-ℕ n)) x)))

  odd-power-neg-Ring :
    (n : ) (x : type-Ring R) 
    is-odd-ℕ n  power-Ring R n (neg-Ring R x)  neg-Ring R (power-Ring R n x)
  odd-power-neg-Ring zero-ℕ x H = ex-falso (H is-even-zero-ℕ)
  odd-power-neg-Ring (succ-ℕ zero-ℕ) x H = refl
  odd-power-neg-Ring (succ-ℕ (succ-ℕ n)) x H =
    ( right-negative-law-mul-Ring R
      ( power-Ring R (succ-ℕ n) (neg-Ring R x))
      ( x)) 
    ( ap
      ( neg-Ring R  mul-Ring' R x)
      ( ( power-succ-Ring R n (neg-Ring R x)) 
        ( ( right-negative-law-mul-Ring R
            ( power-Ring R n (neg-Ring R x))
            ( x)) 
          ( ( ap
              ( neg-Ring R)
              ( ( ap
                  ( mul-Ring' R x)
                  ( odd-power-neg-Ring n x
                    ( is-odd-is-odd-succ-succ-ℕ n H))) 
                ( ( left-negative-law-mul-Ring R (power-Ring R n x) x) 
                  ( ap (neg-Ring R) (inv (power-succ-Ring R n x)))))) 
            ( neg-neg-Ring R (power-Ring R (succ-ℕ n) x))))))