rational commutative monoids (UniMath#763)

This small PR factors out rational commutative monoids from UniMath#623.

---------

Co-authored-by: Fredrik Bakke <[email protected]>

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

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)
+```

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

@@ -0,0 +1,131 @@
+# 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.propositions
+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](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
+every natural number `n > 0`. However, for rational commutative monoids we will
+write the binary operation additively.
+
+## Definition
+
+### The predicate of being a rational commutative monoid
+
+```agda
+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
+
+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 :
+    is-rational-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+  is-rational-Rational-Commutative-Monoid = pr2 M
+```