Normal (commutative) submonoids and saturated congruence relations (#543

)

This PR develops some theory of monoids and commutative monoids
- Submonoids
- Normal Submonoids
- Saturated congruence relations, and proof that they correspond
uniquely to normal submonoids
- Submonoids of commutative monoids
- Normal submonoids of commutative monoids
- Saturated congruence relations, and proof that they correspond
uniquely to norma submonoids of commutative monoids
- The example of the natural numbers with max, and a proof that its
normal submonoids are initial segments of the natural numbers.

src/elementary-number-theory.lagda.md

@@ -51,6 +51,7 @@ open import elementary-number-theory.inequality-integers public
 open import elementary-number-theory.inequality-natural-numbers public
 open import elementary-number-theory.inequality-standard-finite-types public
 open import elementary-number-theory.infinitude-of-primes public
+open import elementary-number-theory.initial-segments-natural-numbers public
 open import elementary-number-theory.integer-partitions public
 open import elementary-number-theory.integers public
 open import elementary-number-theory.kolakoski-sequence public
@@ -62,6 +63,7 @@ open import elementary-number-theory.minimum-natural-numbers public
 open import elementary-number-theory.minimum-standard-finite-types public
 open import elementary-number-theory.modular-arithmetic public
 open import elementary-number-theory.modular-arithmetic-standard-finite-types public
+open import elementary-number-theory.monoid-of-natural-numbers-with-maximum public
 open import elementary-number-theory.multiplication-integers public
 open import elementary-number-theory.multiplication-natural-numbers public
 open import elementary-number-theory.multiset-coefficients public

src/elementary-number-theory/initial-segments-natural-numbers.lagda.md

@@ -0,0 +1,119 @@
+# Initial segments of the natural numbers
+
+```agda
+module elementary-number-theory.initial-segments-natural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.functions
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An **initial segment** of the natural numbers is a subtype `P : ℕ → Prop` such
+that the implication
+
+```md
+  P (n + 1) → P n
+```
+
+holds for every `n : ℕ`.
+
+## Definitions
+
+### Initial segments
+
+```agda
+is-initial-segment-subset-ℕ-Prop : {l : Level} (P : subtype l ℕ) → Prop l
+is-initial-segment-subset-ℕ-Prop P =
+  Π-Prop ℕ (λ n → implication-Prop (P (succ-ℕ n)) (P n))
+
+is-initial-segment-subset-ℕ : {l : Level} (P : subtype l ℕ) → UU l
+is-initial-segment-subset-ℕ P = type-Prop (is-initial-segment-subset-ℕ-Prop P)
+
+initial-segment-ℕ : (l : Level) → UU (lsuc l)
+initial-segment-ℕ l = type-subtype is-initial-segment-subset-ℕ-Prop
+
+module _
+  {l : Level} (I : initial-segment-ℕ l)
+  where
+
+  subset-initial-segment-ℕ : subtype l ℕ
+  subset-initial-segment-ℕ = pr1 I
+
+  is-initial-segment-initial-segment-ℕ :
+    is-initial-segment-subset-ℕ subset-initial-segment-ℕ
+  is-initial-segment-initial-segment-ℕ = pr2 I
+
+  is-in-initial-segment-ℕ : ℕ → UU l
+  is-in-initial-segment-ℕ = is-in-subtype subset-initial-segment-ℕ
+
+  is-closed-under-eq-initial-segment-ℕ :
+    {x y : ℕ} → is-in-initial-segment-ℕ x → x ＝ y → is-in-initial-segment-ℕ y
+  is-closed-under-eq-initial-segment-ℕ =
+    is-closed-under-eq-subtype subset-initial-segment-ℕ
+
+  is-closed-under-eq-initial-segment-ℕ' :
+    {x y : ℕ} → is-in-initial-segment-ℕ y → x ＝ y → is-in-initial-segment-ℕ x
+  is-closed-under-eq-initial-segment-ℕ' =
+    is-closed-under-eq-subtype' subset-initial-segment-ℕ
+```
+
+### Shifting initial segments
+
+```agda
+shift-initial-segment-ℕ :
+  {l : Level} → initial-segment-ℕ l → initial-segment-ℕ l
+pr1 (shift-initial-segment-ℕ I) = subset-initial-segment-ℕ I ∘ succ-ℕ
+pr2 (shift-initial-segment-ℕ I) =
+  is-initial-segment-initial-segment-ℕ I ∘ succ-ℕ
+```
+
+## Properties
+
+### Inhabited initial segments contain `0`
+
+```agda
+contains-zero-initial-segment-ℕ :
+  {l : Level} (I : initial-segment-ℕ l) →
+  (x : ℕ) → is-in-initial-segment-ℕ I x → is-in-initial-segment-ℕ I 0
+contains-zero-initial-segment-ℕ I zero-ℕ H = H
+contains-zero-initial-segment-ℕ I (succ-ℕ x) H =
+  is-initial-segment-initial-segment-ℕ I 0
+    ( contains-zero-initial-segment-ℕ (shift-initial-segment-ℕ I) x H)
+```
+
+### Initial segments that contain a successor contain `1`
+
+```agda
+contains-one-initial-segment-ℕ :
+  {l : Level} (I : initial-segment-ℕ l) →
+  (x : ℕ) → is-in-initial-segment-ℕ I (succ-ℕ x) → is-in-initial-segment-ℕ I 1
+contains-one-initial-segment-ℕ I =
+  contains-zero-initial-segment-ℕ (shift-initial-segment-ℕ I)
+```
+
+### Initial segments are closed under `max-ℕ`
+
+```agda
+max-initial-segment-ℕ :
+  {l : Level} (I : initial-segment-ℕ l) →
+  (x y : ℕ) → is-in-initial-segment-ℕ I x → is-in-initial-segment-ℕ I y →
+  is-in-initial-segment-ℕ I (max-ℕ x y)
+max-initial-segment-ℕ I zero-ℕ y H K = K
+max-initial-segment-ℕ I (succ-ℕ x) zero-ℕ H K = H
+max-initial-segment-ℕ I (succ-ℕ x) (succ-ℕ y) H K =
+  max-initial-segment-ℕ (shift-initial-segment-ℕ I) x y H K
+```

src/elementary-number-theory/maximum-natural-numbers.lagda.md

@@ -7,11 +7,13 @@ module elementary-number-theory.maximum-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.unit-type
 
 open import order-theory.least-upper-bounds-posets
@@ -27,12 +29,24 @@ We define the operation of maximum (least upper bound) for the natural numbers.
 
 ## Definition
 
+### Maximum of natural numbers
+
 ```agda
 max-ℕ : ℕ → (ℕ → ℕ)
 max-ℕ 0 n = n
 max-ℕ (succ-ℕ m) 0 = succ-ℕ m
 max-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (max-ℕ m n)
 
+ap-max-ℕ : {x x' y y' : ℕ} → x ＝ x' → y ＝ y' → max-ℕ x y ＝ max-ℕ x' y'
+ap-max-ℕ p q = ap-binary max-ℕ p q
+
+max-ℕ' : ℕ → (ℕ → ℕ)
+max-ℕ' x y = max-ℕ y x
+```
+
+### Maximum of elements of standard finite types
+
+```agda
 max-Fin-ℕ : (n : ℕ) → (Fin n → ℕ) → ℕ
 max-Fin-ℕ zero-ℕ f = zero-ℕ
 max-Fin-ℕ (succ-ℕ n) f = max-ℕ (f (inr star)) (max-Fin-ℕ n (λ k → f (inl k)))
@@ -74,3 +88,82 @@ is-least-upper-bound-max-ℕ m n =
     leq-right-leq-max-ℕ (max-ℕ m n) m n (refl-leq-ℕ (max-ℕ m n))),
   λ x (m≤x , n≤x) → leq-max-ℕ x m n m≤x n≤x
 ```
+
+### Associativity of `max-ℕ`
+
+```agda
+associative-max-ℕ :
+  (x y z : ℕ) → max-ℕ (max-ℕ x y) z ＝ max-ℕ x (max-ℕ y z)
+associative-max-ℕ zero-ℕ y z = refl
+associative-max-ℕ (succ-ℕ x) zero-ℕ zero-ℕ = refl
+associative-max-ℕ (succ-ℕ x) zero-ℕ (succ-ℕ z) = refl
+associative-max-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ = refl
+associative-max-ℕ (succ-ℕ x) (succ-ℕ y) (succ-ℕ z) =
+  ap succ-ℕ (associative-max-ℕ x y z)
+```
+
+### Unit laws for `max-ℕ`
+
+```agda
+left-unit-law-max-ℕ : (x : ℕ) → max-ℕ 0 x ＝ x
+left-unit-law-max-ℕ x = refl
+
+right-unit-law-max-ℕ : (x : ℕ) → max-ℕ x 0 ＝ x
+right-unit-law-max-ℕ zero-ℕ = refl
+right-unit-law-max-ℕ (succ-ℕ x) = refl
+```
+
+### Commutativity of `max-ℕ`
+
+```agda
+commutative-max-ℕ : (x y : ℕ) → max-ℕ x y ＝ max-ℕ y x
+commutative-max-ℕ zero-ℕ zero-ℕ = refl
+commutative-max-ℕ zero-ℕ (succ-ℕ y) = refl
+commutative-max-ℕ (succ-ℕ x) zero-ℕ = refl
+commutative-max-ℕ (succ-ℕ x) (succ-ℕ y) = ap succ-ℕ (commutative-max-ℕ x y)
+```
+
+### `max-ℕ` is idempotent
+
+```agda
+idempotent-max-ℕ : (x : ℕ) → max-ℕ x x ＝ x
+idempotent-max-ℕ zero-ℕ = refl
+idempotent-max-ℕ (succ-ℕ x) = ap succ-ℕ (idempotent-max-ℕ x)
+```
+
+### Successor diagonal laws for `max-ℕ`
+
+```agda
+left-successor-diagonal-law-max-ℕ : (x : ℕ) → max-ℕ (succ-ℕ x) x ＝ succ-ℕ x
+left-successor-diagonal-law-max-ℕ zero-ℕ = refl
+left-successor-diagonal-law-max-ℕ (succ-ℕ x) =
+  ap succ-ℕ (left-successor-diagonal-law-max-ℕ x)
+
+right-successor-diagonal-law-max-ℕ : (x : ℕ) → max-ℕ x (succ-ℕ x) ＝ succ-ℕ x
+right-successor-diagonal-law-max-ℕ zero-ℕ = refl
+right-successor-diagonal-law-max-ℕ (succ-ℕ x) =
+  ap succ-ℕ (right-successor-diagonal-law-max-ℕ x)
+```
+
+### Addition distributes over `max-ℕ`
+
+```agda
+left-distributive-add-max-ℕ :
+  (x y z : ℕ) → add-ℕ x (max-ℕ y z) ＝ max-ℕ (add-ℕ x y) (add-ℕ x z)
+left-distributive-add-max-ℕ zero-ℕ y z =
+  ( left-unit-law-add-ℕ (max-ℕ y z)) ∙
+  ( ap-max-ℕ (inv (left-unit-law-add-ℕ y)) (inv (left-unit-law-add-ℕ z)))
+left-distributive-add-max-ℕ (succ-ℕ x) y z =
+  ( left-successor-law-add-ℕ x (max-ℕ y z)) ∙
+  ( ( ap succ-ℕ (left-distributive-add-max-ℕ x y z)) ∙
+    ( ap-max-ℕ
+      ( inv (left-successor-law-add-ℕ x y))
+      ( inv (left-successor-law-add-ℕ x z))))
+
+right-distributive-add-max-ℕ :
+  (x y z : ℕ) → add-ℕ (max-ℕ x y) z ＝ max-ℕ (add-ℕ x z) (add-ℕ y z)
+right-distributive-add-max-ℕ x y z =
+  ( commutative-add-ℕ (max-ℕ x y) z) ∙
+  ( ( left-distributive-add-max-ℕ z x y) ∙
+    ( ap-max-ℕ (commutative-add-ℕ z x) (commutative-add-ℕ z y)))
+```

src/elementary-number-theory/minimum-natural-numbers.lagda.md

@@ -7,11 +7,13 @@ module elementary-number-theory.minimum-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.unit-type
 
 open import order-theory.greatest-lower-bounds-posets
@@ -34,14 +36,17 @@ min-ℕ 0 n = 0
 min-ℕ (succ-ℕ m) 0 = 0
 min-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (min-ℕ m n)
 
+ap-min-ℕ : {x x' y y' : ℕ} → x ＝ x' → y ＝ y' → min-ℕ x y ＝ min-ℕ x' y'
+ap-min-ℕ p q = ap-binary min-ℕ p q
+
 min-Fin-ℕ : (n : ℕ) → (Fin (succ-ℕ n) → ℕ) → ℕ
 min-Fin-ℕ zero-ℕ f = f (inr star)
 min-Fin-ℕ (succ-ℕ n) f = min-ℕ (f (inr star)) (min-Fin-ℕ n (λ k → f (inl k)))
 ```
 
 ## Properties
 
-### Minimum is a greatest lower bound
+### The minimum of two natural numbers is a greatest lower bound
 
 ```agda
 leq-min-ℕ :
@@ -77,3 +82,68 @@ is-greatest-lower-bound-min-ℕ l m =
     leq-right-leq-min-ℕ (min-ℕ l m) l m (refl-leq-ℕ (min-ℕ l m))),
   λ x (x≤l , x≤m) → leq-min-ℕ x l m x≤l x≤m
 ```
+
+### Associativity of `min-ℕ`
+
+```agda
+associative-min-ℕ :
+  (x y z : ℕ) → min-ℕ (min-ℕ x y) z ＝ min-ℕ x (min-ℕ y z)
+associative-min-ℕ zero-ℕ y z = refl
+associative-min-ℕ (succ-ℕ x) zero-ℕ zero-ℕ = refl
+associative-min-ℕ (succ-ℕ x) zero-ℕ (succ-ℕ z) = refl
+associative-min-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ = refl
+associative-min-ℕ (succ-ℕ x) (succ-ℕ y) (succ-ℕ z) =
+  ap succ-ℕ (associative-min-ℕ x y z)
+```
+
+### Zero laws for `min-ℕ`
+
+```agda
+left-zero-law-min-ℕ : (x : ℕ) → min-ℕ 0 x ＝ 0
+left-zero-law-min-ℕ x = refl
+
+right-zero-law-min-ℕ : (x : ℕ) → min-ℕ x 0 ＝ 0
+right-zero-law-min-ℕ zero-ℕ = refl
+right-zero-law-min-ℕ (succ-ℕ x) = refl
+```
+
+### Commutativity of `min-ℕ`
+
+```agda
+commutative-min-ℕ : (x y : ℕ) → min-ℕ x y ＝ min-ℕ y x
+commutative-min-ℕ zero-ℕ zero-ℕ = refl
+commutative-min-ℕ zero-ℕ (succ-ℕ y) = refl
+commutative-min-ℕ (succ-ℕ x) zero-ℕ = refl
+commutative-min-ℕ (succ-ℕ x) (succ-ℕ y) = ap succ-ℕ (commutative-min-ℕ x y)
+```
+
+### `min-ℕ` is idempotent
+
+```agda
+idempotent-min-ℕ : (x : ℕ) → min-ℕ x x ＝ x
+idempotent-min-ℕ zero-ℕ = refl
+idempotent-min-ℕ (succ-ℕ x) = ap succ-ℕ (idempotent-min-ℕ x)
+```
+
+### Addition distributes over `min-ℕ`
+
+```agda
+left-distributive-add-min-ℕ :
+  (x y z : ℕ) → add-ℕ x (min-ℕ y z) ＝ min-ℕ (add-ℕ x y) (add-ℕ x z)
+left-distributive-add-min-ℕ zero-ℕ y z =
+  ( left-unit-law-add-ℕ (min-ℕ y z)) ∙
+  ( ap-min-ℕ (inv (left-unit-law-add-ℕ y)) (inv (left-unit-law-add-ℕ z)))
+left-distributive-add-min-ℕ (succ-ℕ x) y z =
+  ( left-successor-law-add-ℕ x (min-ℕ y z)) ∙
+  ( ( ap succ-ℕ (left-distributive-add-min-ℕ x y z)) ∙
+    ( ap-min-ℕ
+      ( inv (left-successor-law-add-ℕ x y))
+      ( inv (left-successor-law-add-ℕ x z))))
+
+right-distributive-add-min-ℕ :
+  (x y z : ℕ) → add-ℕ (min-ℕ x y) z ＝ min-ℕ (add-ℕ x z) (add-ℕ y z)
+right-distributive-add-min-ℕ x y z =
+  ( commutative-add-ℕ (min-ℕ x y) z) ∙
+  ( ( left-distributive-add-min-ℕ z x y) ∙
+    ( ap-min-ℕ (commutative-add-ℕ z x) (commutative-add-ℕ z y)))
+```