Powers of elements in large rings

Content created by Louis Wasserman.

Created on 2025-11-08.
Last modified on 2025-11-08.

module ring-theory.powers-of-elements-large-rings 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.large-monoids
open import group-theory.powers-of-elements-large-monoids

open import ring-theory.large-rings

Idea

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

Definition

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  power-Large-Ring : {l : Level} → ℕ → type-Large-Ring R l → type-Large-Ring R l
  power-Large-Ring =
    power-Large-Monoid (multiplicative-large-monoid-Large-Ring R)

Properties

The power operation preserves similarity

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    preserves-sim-power-Large-Ring :
      {l1 l2 : Level} (n : ℕ) →
      (x : type-Large-Ring R l1) (y : type-Large-Ring R l2) →
      sim-Large-Ring R x y →
      sim-Large-Ring R (power-Large-Ring R n x) (power-Large-Ring R n y)
    preserves-sim-power-Large-Ring =
      preserves-sim-power-Large-Monoid
        ( multiplicative-large-monoid-Large-Ring R)

1ⁿ = 1

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    raise-power-one-Large-Ring :
      (l : Level) (n : ℕ) →
      power-Large-Ring R n (raise-one-Large-Ring R l) ＝
      raise-one-Large-Ring R l
    raise-power-one-Large-Ring =
      raise-power-unit-Large-Monoid
        ( multiplicative-large-monoid-Large-Ring R)

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

xⁿ⁺¹ = xⁿx

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    power-succ-Large-Ring :
      {l : Level} (n : ℕ) (x : type-Large-Ring R l) →
      power-Large-Ring R (succ-ℕ n) x ＝
      mul-Large-Ring R (power-Large-Ring R n x) x
    power-succ-Large-Ring =
      power-succ-Large-Monoid
        ( multiplicative-large-monoid-Large-Ring R)

xⁿ⁺¹ = xxⁿ

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    power-succ-Large-Ring' :
      {l : Level} (n : ℕ) (x : type-Large-Ring R l) →
      power-Large-Ring R (succ-ℕ n) x ＝
      mul-Large-Ring R x (power-Large-Ring R n x)
    power-succ-Large-Ring' =
      power-succ-Large-Monoid'
        ( multiplicative-large-monoid-Large-Ring R)

Powers by sums of natural numbers are products of powers

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    distributive-power-add-Large-Ring :
      {l : Level} (m n : ℕ) {x : type-Large-Ring R l} →
      power-Large-Ring R (m +ℕ n) x ＝
      mul-Large-Ring R (power-Large-Ring R m x) (power-Large-Ring R n x)
    distributive-power-add-Large-Ring =
      distributive-power-add-Large-Monoid
        ( multiplicative-large-monoid-Large-Ring R)

Powers by products of natural numbers are iterated powers

module _
  {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β)
  where

  abstract
    power-mul-Large-Ring :
      {l : Level} (m n : ℕ) {x : type-Large-Ring R l} →
      power-Large-Ring R (m *ℕ n) x ＝
      power-Large-Ring R n (power-Large-Ring R m x)
    power-mul-Large-Ring =
      power-mul-Large-Monoid
        ( multiplicative-large-monoid-Large-Ring R)

Recent changes