Skip to content

Commit 20c7370

Browse files
EgbertRijkefredrik-bakke
EgbertRijke
and
fredrik-bakke
committed
rational commutative monoids (UniMath#763)
This small PR factors out rational commutative monoids from UniMath#623. --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
1 parent 47f04e3 commit 20c7370

File tree

4 files changed

+293
-2
lines changed

4 files changed

+293
-2
lines changed

‎src/group-theory.lagda.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,7 @@ open import group-theory.orbits-concrete-group-actions public
116116
open import group-theory.orbits-group-actions public
117117
open import group-theory.orbits-monoid-actions public
118118
open import group-theory.orders-of-elements-groups public
119+
open import group-theory.powers-of-elements-commutative-monoids public
119120
open import group-theory.powers-of-elements-groups public
120121
open import group-theory.powers-of-elements-monoids public
121122
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
132133
open import group-theory.quotient-groups public
133134
open import group-theory.quotient-groups-concrete-groups public
134135
open import group-theory.quotients-abelian-groups public
136+
open import group-theory.rational-commutative-monoids public
135137
open import group-theory.representations-monoids public
136138
open import group-theory.saturated-congruence-relations-commutative-monoids public
137139
open import group-theory.saturated-congruence-relations-monoids public

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

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
# Powers of elements in commutative monoids
2+
3+
```agda
4+
module group-theory.powers-of-elements-commutative-monoids where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.addition-natural-numbers
11+
open import elementary-number-theory.multiplication-natural-numbers
12+
open import elementary-number-theory.natural-numbers
13+
14+
open import foundation.identity-types
15+
open import foundation.universe-levels
16+
17+
open import group-theory.commutative-monoids
18+
open import group-theory.homomorphisms-commutative-monoids
19+
open import group-theory.powers-of-elements-monoids
20+
```
21+
22+
</details>
23+
24+
The **power operation** on a [monoid](group-theory.monoids.md) is the map
25+
`n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md)
26+
multiplying `x` with itself `n` times.
27+
28+
## Definition
29+
30+
```agda
31+
module _
32+
{l : Level} (M : Commutative-Monoid l)
33+
where
34+
35+
power-Commutative-Monoid :
36+
ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
37+
power-Commutative-Monoid = power-Monoid (monoid-Commutative-Monoid M)
38+
```
39+
40+
## Properties
41+
42+
### `1ⁿ ＝ 1`
43+
44+
```agda
45+
module _
46+
{l : Level} (M : Commutative-Monoid l)
47+
where
48+
49+
power-unit-Commutative-Monoid :
50+
(n : ℕ) →
51+
power-Commutative-Monoid M n (unit-Commutative-Monoid M) ＝
52+
unit-Commutative-Monoid M
53+
power-unit-Commutative-Monoid zero-ℕ = refl
54+
power-unit-Commutative-Monoid (succ-ℕ zero-ℕ) = refl
55+
power-unit-Commutative-Monoid (succ-ℕ (succ-ℕ n)) =
56+
right-unit-law-mul-Commutative-Monoid M _ ∙
57+
power-unit-Commutative-Monoid (succ-ℕ n)
58+
```
59+
60+
### `xⁿ⁺¹ = xⁿx`
61+
62+
```agda
63+
module _
64+
{l : Level} (M : Commutative-Monoid l)
65+
where
66+
67+
power-succ-Commutative-Monoid :
68+
(n : ℕ) (x : type-Commutative-Monoid M) →
69+
power-Commutative-Monoid M (succ-ℕ n) x ＝
70+
mul-Commutative-Monoid M (power-Commutative-Monoid M n x) x
71+
power-succ-Commutative-Monoid =
72+
power-succ-Monoid (monoid-Commutative-Monoid M)
73+
```
74+
75+
### `xⁿ⁺¹ ＝ xxⁿ`
76+
77+
```agda
78+
module _
79+
{l : Level} (M : Commutative-Monoid l)
80+
where
81+
82+
power-succ-Commutative-Monoid' :
83+
(n : ℕ) (x : type-Commutative-Monoid M) →
84+
power-Commutative-Monoid M (succ-ℕ n) x ＝
85+
mul-Commutative-Monoid M x (power-Commutative-Monoid M n x)
86+
power-succ-Commutative-Monoid' =
87+
power-succ-Monoid' (monoid-Commutative-Monoid M)
88+
```
89+
90+
### Powers by sums of natural numbers are products of powers
91+
92+
```agda
93+
module _
94+
{l : Level} (M : Commutative-Monoid l)
95+
where
96+
97+
distributive-power-add-Commutative-Monoid :
98+
(m n : ℕ) {x : type-Commutative-Monoid M} →
99+
power-Commutative-Monoid M (m +ℕ n) x ＝
100+
mul-Commutative-Monoid M
101+
( power-Commutative-Monoid M m x)
102+
( power-Commutative-Monoid M n x)
103+
distributive-power-add-Commutative-Monoid =
104+
distributive-power-add-Monoid (monoid-Commutative-Monoid M)
105+
```
106+
107+
### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`
108+
109+
```agda
110+
module _
111+
{l : Level} (M : Commutative-Monoid l)
112+
where
113+
114+
distributive-power-mul-Commutative-Monoid :
115+
(n : ℕ) {x y : type-Commutative-Monoid M} →
116+
(H : mul-Commutative-Monoid M x y ＝ mul-Commutative-Monoid M y x) →
117+
power-Commutative-Monoid M n (mul-Commutative-Monoid M x y) ＝
118+
mul-Commutative-Monoid M
119+
( power-Commutative-Monoid M n x)
120+
( power-Commutative-Monoid M n y)
121+
distributive-power-mul-Commutative-Monoid =
122+
distributive-power-mul-Monoid (monoid-Commutative-Monoid M)
123+
```
124+
125+
### Powers by products of natural numbers are iterated powers
126+
127+
```agda
128+
module _
129+
{l : Level} (M : Commutative-Monoid l)
130+
where
131+
132+
power-mul-Commutative-Monoid :
133+
(m n : ℕ) {x : type-Commutative-Monoid M} →
134+
power-Commutative-Monoid M (m *ℕ n) x ＝
135+
power-Commutative-Monoid M n (power-Commutative-Monoid M m x)
136+
power-mul-Commutative-Monoid =
137+
power-mul-Monoid (monoid-Commutative-Monoid M)
138+
```
139+
140+
### Commutative-Monoid homomorphisms preserve powers
141+
142+
```agda
143+
module _
144+
{l1 l2 : Level} (M : Commutative-Monoid l1)
145+
(N : Commutative-Monoid l2) (f : type-hom-Commutative-Monoid M N)
146+
where
147+
148+
preserves-powers-hom-Commutative-Monoid :
149+
(n : ℕ) (x : type-Commutative-Monoid M) →
150+
map-hom-Commutative-Monoid M N f (power-Commutative-Monoid M n x) ＝
151+
power-Commutative-Monoid N n (map-hom-Commutative-Monoid M N f x)
152+
preserves-powers-hom-Commutative-Monoid =
153+
preserves-powers-hom-Monoid
154+
( monoid-Commutative-Monoid M)
155+
( monoid-Commutative-Monoid N)
156+
( f)
157+
```

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,9 @@ open import group-theory.monoids
2323

2424
## Idea
2525

26-
The power operation on a monoid is the map `n x ↦ xⁿ`, which is defined by
27-
iteratively multiplying `x` with itself `n` times.
26+
The **power operation** on a [monoid](group-theory.monoids.md) is the map
27+
`n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md)
28+
multiplying `x` with itself `n` times.
2829

2930
## Definition
3031

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

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
# Rational commutative monoids
2+
3+
```agda
4+
module group-theory.rational-commutative-monoids where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.natural-numbers
11+
12+
open import foundation.dependent-pair-types
13+
open import foundation.equivalences
14+
open import foundation.identity-types
15+
open import foundation.propositions
16+
open import foundation.universe-levels
17+
18+
open import group-theory.commutative-monoids
19+
open import group-theory.monoids
20+
open import group-theory.powers-of-elements-commutative-monoids
21+
```
22+
23+
</details>
24+
25+
## Idea
26+
27+
A **rational commutative monoid** is a
28+
[commutative monoid](group-theory.commutative-monoids.md) `(M,0,+)` in which the
29+
map `x ↦ nx` is invertible for every
30+
[natural number](elementary-number-theory.natural-numbers.md) `n > 0`. This
31+
condition implies that we can invert the natural numbers in `M`, which are the
32+
elements of the form `n1` in `M`.
33+
34+
Note: Since we usually write commutative monoids multiplicatively, the condition
35+
that a commutative monoid is rational is that the map `x ↦ xⁿ` is invertible for
36+
every natural number `n > 0`. However, for rational commutative monoids we will
37+
write the binary operation additively.
38+
39+
## Definition
40+
41+
### The predicate of being a rational commutative monoid
42+
43+
```agda
44+
module _
45+
{l : Level} (M : Commutative-Monoid l)
46+
where
47+
48+
is-rational-prop-Commutative-Monoid : Prop l
49+
is-rational-prop-Commutative-Monoid =
50+
Π-Prop ℕ
51+
( λ n →
52+
is-equiv-Prop (power-Commutative-Monoid M (succ-ℕ n)))
53+
54+
is-rational-Commutative-Monoid : UU l
55+
is-rational-Commutative-Monoid =
56+
type-Prop is-rational-prop-Commutative-Monoid
57+
58+
is-prop-is-rational-Commutative-Monoid :
59+
is-prop is-rational-Commutative-Monoid
60+
is-prop-is-rational-Commutative-Monoid =
61+
is-prop-type-Prop is-rational-prop-Commutative-Monoid
62+
```
63+
64+
### Rational commutative monoids
65+
66+
```agda
67+
Rational-Commutative-Monoid : (l : Level) → UU (lsuc l)
68+
Rational-Commutative-Monoid l =
69+
Σ (Commutative-Monoid l) is-rational-Commutative-Monoid
70+
71+
module _
72+
{l : Level} (M : Rational-Commutative-Monoid l)
73+
where
74+
75+
commutative-monoid-Rational-Commutative-Monoid : Commutative-Monoid l
76+
commutative-monoid-Rational-Commutative-Monoid = pr1 M
77+
78+
monoid-Rational-Commutative-Monoid : Monoid l
79+
monoid-Rational-Commutative-Monoid =
80+
monoid-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
81+
82+
type-Rational-Commutative-Monoid : UU l
83+
type-Rational-Commutative-Monoid =
84+
type-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
85+
86+
add-Rational-Commutative-Monoid :
87+
(x y : type-Rational-Commutative-Monoid) →
88+
type-Rational-Commutative-Monoid
89+
add-Rational-Commutative-Monoid =
90+
mul-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
91+
92+
zero-Rational-Commutative-Monoid : type-Rational-Commutative-Monoid
93+
zero-Rational-Commutative-Monoid =
94+
unit-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
95+
96+
associative-add-Rational-Commutative-Monoid :
97+
(x y z : type-Rational-Commutative-Monoid) →
98+
add-Rational-Commutative-Monoid
99+
( add-Rational-Commutative-Monoid x y)
100+
( z) ＝
101+
add-Rational-Commutative-Monoid
102+
( x)
103+
( add-Rational-Commutative-Monoid y z)
104+
associative-add-Rational-Commutative-Monoid =
105+
associative-mul-Commutative-Monoid
106+
commutative-monoid-Rational-Commutative-Monoid
107+
108+
left-unit-law-add-Rational-Commutative-Monoid :
109+
(x : type-Rational-Commutative-Monoid) →
110+
add-Rational-Commutative-Monoid zero-Rational-Commutative-Monoid x ＝ x
111+
left-unit-law-add-Rational-Commutative-Monoid =
112+
left-unit-law-mul-Commutative-Monoid
113+
commutative-monoid-Rational-Commutative-Monoid
114+
115+
right-unit-law-add-Rational-Commutative-Monoid :
116+
(x : type-Rational-Commutative-Monoid) →
117+
add-Rational-Commutative-Monoid x zero-Rational-Commutative-Monoid ＝ x
118+
right-unit-law-add-Rational-Commutative-Monoid =
119+
right-unit-law-mul-Commutative-Monoid
120+
commutative-monoid-Rational-Commutative-Monoid
121+
122+
multiple-Rational-Commutative-Monoid :
123+
ℕ → type-Rational-Commutative-Monoid → type-Rational-Commutative-Monoid
124+
multiple-Rational-Commutative-Monoid =
125+
power-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
126+
127+
is-rational-Rational-Commutative-Monoid :
128+
is-rational-Commutative-Monoid
129+
commutative-monoid-Rational-Commutative-Monoid
130+
is-rational-Rational-Commutative-Monoid = pr2 M
131+
```

0 commit comments

Comments
 (0)