From 1faaf97d7e554fa49f89ab349fd160adea906561 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Sep 2023 14:05:22 +0200
Subject: [PATCH 1/3] rational commutative monoids

---
 src/group-theory.lagda.md                     |   2 +
 ...s-of-elements-commutative-monoids.lagda.md | 157 ++++++++++++++++++
 .../powers-of-elements-monoids.lagda.md       |   5 +-
 .../rational-commutative-monoids.lagda.md     | 107 ++++++++++++
 4 files changed, 269 insertions(+), 2 deletions(-)
 create mode 100644 src/group-theory/powers-of-elements-commutative-monoids.lagda.md
 create mode 100644 src/group-theory/rational-commutative-monoids.lagda.md

diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index 424febf2d0..b9552606e6 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -116,6 +116,7 @@ open import group-theory.orbits-concrete-group-actions public
 open import group-theory.orbits-group-actions public
 open import group-theory.orbits-monoid-actions public
 open import group-theory.orders-of-elements-groups public
+open import group-theory.powers-of-elements-commutative-monoids public
 open import group-theory.powers-of-elements-groups public
 open import group-theory.powers-of-elements-monoids public
 open import group-theory.precategory-of-abelian-groups public
@@ -132,6 +133,7 @@ open import group-theory.products-of-tuples-of-elements-commutative-monoids publ
 open import group-theory.quotient-groups public
 open import group-theory.quotient-groups-concrete-groups public
 open import group-theory.quotients-abelian-groups public
+open import group-theory.rational-commutative-monoids public
 open import group-theory.representations-monoids public
 open import group-theory.saturated-congruence-relations-commutative-monoids public
 open import group-theory.saturated-congruence-relations-monoids public
diff --git a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..56ffe733ca
--- /dev/null
+++ b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
@@ -0,0 +1,157 @@
+# Powers of elements in commutative monoids
+
+```agda
+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>
+
+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
+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)
+```
diff --git a/src/group-theory/powers-of-elements-monoids.lagda.md b/src/group-theory/powers-of-elements-monoids.lagda.md
index 5e484a3e20..24b2cdd1d7 100644
--- a/src/group-theory/powers-of-elements-monoids.lagda.md
+++ b/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
 
diff --git a/src/group-theory/rational-commutative-monoids.lagda.md b/src/group-theory/rational-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..d21f79ca7a
--- /dev/null
+++ b/src/group-theory/rational-commutative-monoids.lagda.md
@@ -0,0 +1,107 @@
+# Rational commutative monoids
+
+```agda
+module group-theory.rational-commutative-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## Idea
+
+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
+that a commutative monoid is rational is that the map `x ↦ xⁿ` is invertible for
+every natural number `n`. However, for rational commutative monoids we will
+write the binary operation additively.
+
+## Definition
+
+### The predicate of being a rational commutative monoid
+
+```agda
+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
+```

From b4a91cdbf100ce5b8183dd3f870ca14fe213a794 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Sep 2023 16:42:47 +0200
Subject: [PATCH 2/3] fix

---
 .../rational-commutative-monoids.lagda.md     | 33 +++++++++++++++----
 1 file changed, 27 insertions(+), 6 deletions(-)

diff --git a/src/group-theory/rational-commutative-monoids.lagda.md b/src/group-theory/rational-commutative-monoids.lagda.md
index d21f79ca7a..fadebbf4ba 100644
--- a/src/group-theory/rational-commutative-monoids.lagda.md
+++ b/src/group-theory/rational-commutative-monoids.lagda.md
@@ -12,6 +12,7 @@ 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.propositions
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
@@ -25,11 +26,11 @@ open import group-theory.powers-of-elements-commutative-monoids
 
 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`.
+map `x ↦ nx` is invertible for every natural number `n > 0`.
 
 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`. However, for rational commutative monoids we will
+every natural number `n > 0`. However, for rational commutative monoids we will
 write the binary operation additively.
 
 ## Definition
@@ -37,10 +38,29 @@ write the binary operation additively.
 ### The predicate of being a rational commutative monoid
 
 ```agda
-is-rational-Commutative-Monoid : {l : Level} → Commutative-Monoid l → UU l
-is-rational-Commutative-Monoid M =
-  (n : ℕ) → is-equiv (power-Commutative-Monoid M n)
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  is-rational-prop-Commutative-Monoid : Prop l
+  is-rational-prop-Commutative-Monoid =
+    Π-Prop ℕ
+      ( λ n →
+        is-equiv-Prop (power-Commutative-Monoid M (succ-ℕ n)))
 
+  is-rational-Commutative-Monoid : UU l
+  is-rational-Commutative-Monoid =
+    type-Prop is-rational-prop-Commutative-Monoid
+
+  is-prop-is-rational-Commutative-Monoid :
+    is-prop is-rational-Commutative-Monoid
+  is-prop-is-rational-Commutative-Monoid =
+    is-prop-type-Prop is-rational-prop-Commutative-Monoid
+```
+
+### Rational commutative monoids
+
+```agda
 Rational-Commutative-Monoid : (l : Level) → UU (lsuc l)
 Rational-Commutative-Monoid l =
   Σ (Commutative-Monoid l) is-rational-Commutative-Monoid
@@ -102,6 +122,7 @@ module _
     power-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
 
   is-rational-Rational-Commutative-Monoid :
-    (n : ℕ) → is-equiv (multiple-Rational-Commutative-Monoid n)
+    is-rational-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
   is-rational-Rational-Commutative-Monoid = pr2 M
 ```

From 3e37717702b069aa666841d24010308e5d6cc554 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Sep 2023 16:45:09 +0200
Subject: [PATCH 3/3] fix

---
 src/group-theory/rational-commutative-monoids.lagda.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/group-theory/rational-commutative-monoids.lagda.md b/src/group-theory/rational-commutative-monoids.lagda.md
index fadebbf4ba..2c036f47fe 100644
--- a/src/group-theory/rational-commutative-monoids.lagda.md
+++ b/src/group-theory/rational-commutative-monoids.lagda.md
@@ -26,7 +26,10 @@ open import group-theory.powers-of-elements-commutative-monoids
 
 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 > 0`.
+map `x ↦ nx` is invertible for every
+[natural number](elementary-number-theory.natural-numbers.md) `n > 0`. This
+condition implies that we can invert the natural numbers in `M`, which are the
+elements of the form `n1` in `M`.
 
 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