rational monoids

src/group-theory/powers-of-elements-commutative-monoids.lagda.md

@@ -7,30 +7,151 @@ module group-theory.powers-of-elements-commutative-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.identity-types
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.homomorphisms-commutative-monoids
+open import group-theory.powers-of-elements-monoids
 ```
 
 </details>
 
-## Idea
-
-Consider an element `x` in a
-[commutative monoid](group-theory.commutative-monoids.md) and a
-[natural number](elementary-number-theory.natural-numbers.md) `n : ℕ`. The
-`n`-th **power** of `x` is the `n` times iterated product of `x` with itself.
+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.
 
 ## Definition
 
 ```agda
-power-Commutative-Monoid :
-  {l : Level} (M : Commutative-Monoid l) →
-  ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
-power-Commutative-Monoid M zero-ℕ x = unit-Commutative-Monoid M
-power-Commutative-Monoid M (succ-ℕ zero-ℕ) x = x
-power-Commutative-Monoid M (succ-ℕ (succ-ℕ n)) x =
-  mul-Commutative-Monoid M (power-Commutative-Monoid M (succ-ℕ n) x) x
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-Commutative-Monoid :
+    ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
+  power-Commutative-Monoid = power-Monoid (monoid-Commutative-Monoid M)
+```
+
+## Properties
+
+### `1ⁿ ＝ 1`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-unit-Commutative-Monoid :
+    (n : ℕ) →
+    power-Commutative-Monoid M n (unit-Commutative-Monoid M) ＝
+    unit-Commutative-Monoid M
+  power-unit-Commutative-Monoid zero-ℕ = refl
+  power-unit-Commutative-Monoid (succ-ℕ zero-ℕ) = refl
+  power-unit-Commutative-Monoid (succ-ℕ (succ-ℕ n)) =
+    right-unit-law-mul-Commutative-Monoid M _ ∙
+    power-unit-Commutative-Monoid (succ-ℕ n)
+```
+
+### `xⁿ⁺¹ = xⁿx`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-succ-Commutative-Monoid :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    power-Commutative-Monoid M (succ-ℕ n) x ＝
+    mul-Commutative-Monoid M (power-Commutative-Monoid M n x) x
+  power-succ-Commutative-Monoid =
+    power-succ-Monoid (monoid-Commutative-Monoid M)
+```
+
+### `xⁿ⁺¹ ＝ xxⁿ`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-succ-Commutative-Monoid' :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    power-Commutative-Monoid M (succ-ℕ n) x ＝
+    mul-Commutative-Monoid M x (power-Commutative-Monoid M n x)
+  power-succ-Commutative-Monoid' =
+    power-succ-Monoid' (monoid-Commutative-Monoid M)
+```
+
+### Powers by sums of natural numbers are products of powers
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  distributive-power-add-Commutative-Monoid :
+    (m n : ℕ) {x : type-Commutative-Monoid M} →
+    power-Commutative-Monoid M (m +ℕ n) x ＝
+    mul-Commutative-Monoid M
+      ( power-Commutative-Monoid M m x)
+      ( power-Commutative-Monoid M n x)
+  distributive-power-add-Commutative-Monoid =
+    distributive-power-add-Monoid (monoid-Commutative-Monoid M)
+```
+
+### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  distributive-power-mul-Commutative-Monoid :
+    (n : ℕ) {x y : type-Commutative-Monoid M} →
+    (H : mul-Commutative-Monoid M x y ＝ mul-Commutative-Monoid M y x) →
+    power-Commutative-Monoid M n (mul-Commutative-Monoid M x y) ＝
+    mul-Commutative-Monoid M
+      ( power-Commutative-Monoid M n x)
+      ( power-Commutative-Monoid M n y)
+  distributive-power-mul-Commutative-Monoid =
+    distributive-power-mul-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Powers by products of natural numbers are iterated powers
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-mul-Commutative-Monoid :
+    (m n : ℕ) {x : type-Commutative-Monoid M} →
+    power-Commutative-Monoid M (m *ℕ n) x ＝
+    power-Commutative-Monoid M n (power-Commutative-Monoid M m x)
+  power-mul-Commutative-Monoid =
+    power-mul-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Commutative-Monoid homomorphisms preserve powers
+
+```agda
+module _
+  {l1 l2 : Level} (M : Commutative-Monoid l1)
+  (N : Commutative-Monoid l2) (f : type-hom-Commutative-Monoid M N)
+  where
+
+  preserves-powers-hom-Commutative-Monoid :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    map-hom-Commutative-Monoid M N f (power-Commutative-Monoid M n x) ＝
+    power-Commutative-Monoid N n (map-hom-Commutative-Monoid M N f x)
+  preserves-powers-hom-Commutative-Monoid =
+    preserves-powers-hom-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( monoid-Commutative-Monoid N)
+      ( f)
 ```

src/group-theory/powers-of-elements-monoids.lagda.md

@@ -23,8 +23,9 @@ open import group-theory.monoids
 
 ## Idea
 
-The power operation on a monoid is the map `n x ↦ xⁿ`, which is defined by
-iteratively multiplying `x` with itself `n` times.
+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.
 
 ## Definition
 

src/group-theory/rational-commutative-monoids.lagda.md

@@ -9,10 +9,13 @@ module group-theory.rational-commutative-monoids where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.monoids
 open import group-theory.powers-of-elements-commutative-monoids
 ```
 
@@ -24,9 +27,10 @@ A **rational commutative monoid** is a
 [commutative monoid](group-theory.commutative-monoids.md) `(M,0,+)` in which the
 map `x ↦ nx` is invertible for every natural number `n`.
 
-Note: since we usually write commutative monoids multiplicatively, the condition
+Note: Since we usually write commutative monoids multiplicatively, the condition
 that a commutative monoid is rational is that the map `x ↦ xⁿ` is invertible for
-every natural number `n`.
+every natural number `n`. However, for rational commutative monoids we will
+write the binary operation additively.
 
 ## Definition
 
@@ -36,4 +40,68 @@ every natural number `n`.
 is-rational-Commutative-Monoid : {l : Level} → Commutative-Monoid l → UU l
 is-rational-Commutative-Monoid M =
   (n : ℕ) → is-equiv (power-Commutative-Monoid M n)
+
+Rational-Commutative-Monoid : (l : Level) → UU (lsuc l)
+Rational-Commutative-Monoid l =
+  Σ (Commutative-Monoid l) is-rational-Commutative-Monoid
+
+module _
+  {l : Level} (M : Rational-Commutative-Monoid l)
+  where
+
+  commutative-monoid-Rational-Commutative-Monoid : Commutative-Monoid l
+  commutative-monoid-Rational-Commutative-Monoid = pr1 M
+
+  monoid-Rational-Commutative-Monoid : Monoid l
+  monoid-Rational-Commutative-Monoid =
+    monoid-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  type-Rational-Commutative-Monoid : UU l
+  type-Rational-Commutative-Monoid =
+    type-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  add-Rational-Commutative-Monoid :
+    (x y : type-Rational-Commutative-Monoid) →
+    type-Rational-Commutative-Monoid
+  add-Rational-Commutative-Monoid =
+    mul-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  zero-Rational-Commutative-Monoid : type-Rational-Commutative-Monoid
+  zero-Rational-Commutative-Monoid =
+    unit-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  associative-add-Rational-Commutative-Monoid :
+    (x y z : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid
+      ( add-Rational-Commutative-Monoid x y)
+      ( z) ＝
+    add-Rational-Commutative-Monoid
+      ( x)
+      ( add-Rational-Commutative-Monoid y z)
+  associative-add-Rational-Commutative-Monoid =
+    associative-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  left-unit-law-add-Rational-Commutative-Monoid :
+    (x : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid zero-Rational-Commutative-Monoid x ＝ x
+  left-unit-law-add-Rational-Commutative-Monoid =
+    left-unit-law-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  right-unit-law-add-Rational-Commutative-Monoid :
+    (x : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid x zero-Rational-Commutative-Monoid ＝ x
+  right-unit-law-add-Rational-Commutative-Monoid =
+    right-unit-law-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  multiple-Rational-Commutative-Monoid :
+    ℕ → type-Rational-Commutative-Monoid → type-Rational-Commutative-Monoid
+  multiple-Rational-Commutative-Monoid =
+    power-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  is-rational-Rational-Commutative-Monoid :
+    (n : ℕ) → is-equiv (multiple-Rational-Commutative-Monoid n)
+  is-rational-Rational-Commutative-Monoid = pr2 M
 ```