Powers of elements in large commutative monoids

Content created by Louis Wasserman.

Created on 2025-10-17.
Last modified on 2025-10-17.

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

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

Idea

The power operation on a large commutative monoid is inherited from the power operation on the underlying large monoid.

Definition

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  power-Large-Commutative-Monoid :
    {l : Level}    type-Large-Commutative-Monoid M l 
    type-Large-Commutative-Monoid M l
  power-Large-Commutative-Monoid =
    power-Large-Monoid (large-monoid-Large-Commutative-Monoid M)

Properties

The power operation preserves similarity

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    preserves-sim-power-Large-Commutative-Monoid :
      {l1 l2 : Level} (n : ) 
      (x : type-Large-Commutative-Monoid M l1) 
      (y : type-Large-Commutative-Monoid M l2) 
      sim-Large-Commutative-Monoid M x y 
      sim-Large-Commutative-Monoid M
        ( power-Large-Commutative-Monoid M n x)
        ( power-Large-Commutative-Monoid M n y)
    preserves-sim-power-Large-Commutative-Monoid =
      preserves-sim-power-Large-Monoid
        ( large-monoid-Large-Commutative-Monoid M)

1ⁿ = 1

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    raise-power-unit-Large-Commutative-Monoid :
      (l : Level) (n : ) 
      power-Large-Commutative-Monoid M n
        ( raise-unit-Large-Commutative-Monoid M l) 
      raise-unit-Large-Commutative-Monoid M l
    raise-power-unit-Large-Commutative-Monoid =
      raise-power-unit-Large-Monoid (large-monoid-Large-Commutative-Monoid M)

xⁿ⁺¹ = xⁿx

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    power-succ-Large-Commutative-Monoid :
      {l : Level} (n : ) (x : type-Large-Commutative-Monoid M l) 
      power-Large-Commutative-Monoid M (succ-ℕ n) x 
      mul-Large-Commutative-Monoid M (power-Large-Commutative-Monoid M n x) x
    power-succ-Large-Commutative-Monoid =
      power-succ-Large-Monoid (large-monoid-Large-Commutative-Monoid M)

xⁿ⁺¹ = xxⁿ

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    power-succ-Large-Commutative-Monoid' :
      {l : Level} (n : ) (x : type-Large-Commutative-Monoid M l) 
      power-Large-Commutative-Monoid M (succ-ℕ n) x 
      mul-Large-Commutative-Monoid M x (power-Large-Commutative-Monoid M n x)
    power-succ-Large-Commutative-Monoid' =
      power-succ-Large-Monoid' (large-monoid-Large-Commutative-Monoid M)

Powers by sums of natural numbers are products of powers

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    distributive-power-add-Large-Commutative-Monoid :
      {l : Level} (m n : ) {x : type-Large-Commutative-Monoid M l} 
      power-Large-Commutative-Monoid M (m +ℕ n) x 
      mul-Large-Commutative-Monoid M
        ( power-Large-Commutative-Monoid M m x)
        ( power-Large-Commutative-Monoid M n x)
    distributive-power-add-Large-Commutative-Monoid =
      distributive-power-add-Large-Monoid
        ( large-monoid-Large-Commutative-Monoid M)

(xy)ⁿ = xⁿyⁿ

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    distributive-power-mul-Large-Commutative-Monoid :
      {l1 l2 : Level} (n : ) 
      {x : type-Large-Commutative-Monoid M l1} 
      {y : type-Large-Commutative-Monoid M l2} 
      power-Large-Commutative-Monoid M n (mul-Large-Commutative-Monoid M x y) 
      mul-Large-Commutative-Monoid M
        ( power-Large-Commutative-Monoid M n x)
        ( power-Large-Commutative-Monoid M n y)
    distributive-power-mul-Large-Commutative-Monoid n =
      distributive-power-mul-Large-Monoid
        ( large-monoid-Large-Commutative-Monoid M)
        ( n)
        ( commutative-mul-Large-Commutative-Monoid M _ _)

Powers by products of natural numbers are iterated powers

module _
  {α : Level  Level} {β : Level  Level  Level}
  (M : Large-Commutative-Monoid α β)
  where

  abstract
    power-mul-Large-Commutative-Monoid :
      {l : Level} (m n : ) {x : type-Large-Commutative-Monoid M l} 
      power-Large-Commutative-Monoid M (m *ℕ n) x 
      power-Large-Commutative-Monoid M n (power-Large-Commutative-Monoid M m x)
    power-mul-Large-Commutative-Monoid =
      power-mul-Large-Monoid (large-monoid-Large-Commutative-Monoid M)

Recent changes