From 418af109e808dd2691e7cec61a7e1f50cb555400 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 25 Oct 2025 02:57:10 +0200 Subject: [PATCH 1/3] min/max semigroups of real numbers --- .../binary-maximum-real-numbers.lagda.md | 75 +++++++++++++++++++ .../binary-minimum-real-numbers.lagda.md | 75 +++++++++++++++++++ 2 files changed, 150 insertions(+) diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md index 7d521f85c1b..ef34da8c2e4 100644 --- a/src/real-numbers/binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md @@ -22,6 +22,9 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels +open import group-theory.large-semigroups +open import group-theory.semigroups + open import metric-spaces.metric-space-of-short-functions-metric-spaces open import metric-spaces.short-functions-metric-spaces @@ -200,6 +203,78 @@ module _ ( is-least-binary-upper-bound-max-ℝ y x))) ``` +### The binary maximum is associative + +```agda +module _ + {lx ly lz : Level} + (x : ℝ lx) (y : ℝ ly) (z : ℝ lz) + where + + abstract + associative-max-ℝ : max-ℝ (max-ℝ x y) z ＝ max-ℝ x (max-ℝ y z) + associative-max-ℝ = + antisymmetric-leq-ℝ + ( max-ℝ (max-ℝ x y) z) + ( max-ℝ x (max-ℝ y z)) + ( leq-max-leq-leq-ℝ + ( max-ℝ x y) + ( z) + ( max-ℝ x (max-ℝ y z)) + ( leq-max-leq-leq-ℝ + ( x) + ( y) + ( max-ℝ x (max-ℝ y z)) + ( leq-left-max-ℝ x (max-ℝ y z)) + ( transitive-leq-ℝ + ( y) + ( max-ℝ y z) + ( max-ℝ x (max-ℝ y z)) + ( leq-right-max-ℝ x (max-ℝ y z)) + ( leq-left-max-ℝ y z))) + ( transitive-leq-ℝ + ( z) + ( max-ℝ y z) + ( max-ℝ x (max-ℝ y z)) + ( leq-right-max-ℝ x (max-ℝ y z)) + ( leq-right-max-ℝ y z))) + ( leq-max-leq-leq-ℝ + ( x) + ( max-ℝ y z) + ( max-ℝ (max-ℝ x y) z) + ( transitive-leq-ℝ + ( x) + ( max-ℝ x y) + ( max-ℝ (max-ℝ x y) z) + ( leq-left-max-ℝ (max-ℝ x y) z) + ( leq-left-max-ℝ x y)) + ( leq-max-leq-leq-ℝ + ( y) + ( z) + ( max-ℝ (max-ℝ x y) z) + ( transitive-leq-ℝ + ( y) + ( max-ℝ x y) + ( max-ℝ (max-ℝ x y) z) + ( leq-left-max-ℝ (max-ℝ x y) z) + ( leq-right-max-ℝ x y)) + ( leq-right-max-ℝ (max-ℝ x y) z))) +``` + +### The large semigroup of real numbers under the maximum operator + +```agda +large-semigroup-max-ℝ : Large-Semigroup lsuc +large-semigroup-max-ℝ = make-Large-Semigroup ℝ-Set max-ℝ associative-max-ℝ +``` + +### The semigroup of real numbers under the maximum operator at a given level + +```agda +semigroup-max-ℝ : (l : Level) → Semigroup (lsuc l) +semigroup-max-ℝ = semigroup-Large-Semigroup large-semigroup-max-ℝ +``` + ### The large poset of real numbers has joins ```agda diff --git a/src/real-numbers/binary-minimum-real-numbers.lagda.md b/src/real-numbers/binary-minimum-real-numbers.lagda.md index f156bb46744..dc7deece3e7 100644 --- a/src/real-numbers/binary-minimum-real-numbers.lagda.md +++ b/src/real-numbers/binary-minimum-real-numbers.lagda.md @@ -19,6 +19,9 @@ open import foundation.logical-equivalences open import foundation.transport-along-identifications open import foundation.universe-levels +open import group-theory.large-semigroups +open import group-theory.semigroups + open import order-theory.greatest-lower-bounds-large-posets open import order-theory.large-meet-semilattices open import order-theory.meet-semilattices @@ -132,6 +135,78 @@ module _ ( is-greatest-binary-lower-bound-min-ℝ x y)) ``` +### The binary minimum is associative + +```agda +module _ + {lx ly lz : Level} + (x : ℝ lx) (y : ℝ ly) (z : ℝ lz) + where + + abstract + associative-min-ℝ : min-ℝ (min-ℝ x y) z ＝ min-ℝ x (min-ℝ y z) + associative-min-ℝ = + antisymmetric-leq-ℝ + ( min-ℝ (min-ℝ x y) z) + ( min-ℝ x (min-ℝ y z)) + ( leq-min-leq-leq-ℝ + ( x) + ( min-ℝ y z) + ( min-ℝ (min-ℝ x y) z) + ( transitive-leq-ℝ + ( min-ℝ (min-ℝ x y) z) + ( min-ℝ x y) + ( x) + ( leq-left-min-ℝ x y) + ( leq-left-min-ℝ (min-ℝ x y) z)) + ( leq-min-leq-leq-ℝ + ( y) + ( z) + ( min-ℝ ( min-ℝ x y) z) + ( transitive-leq-ℝ + ( min-ℝ (min-ℝ x y) z) + ( min-ℝ x y) + ( y) + ( leq-right-min-ℝ x y) + ( leq-left-min-ℝ (min-ℝ x y) z)) + ( leq-right-min-ℝ (min-ℝ x y) z))) + ( leq-min-leq-leq-ℝ + ( min-ℝ x y) + ( z) + ( min-ℝ x (min-ℝ y z)) + ( leq-min-leq-leq-ℝ + ( x) + ( y) + ( min-ℝ x (min-ℝ y z)) + ( leq-left-min-ℝ x (min-ℝ y z)) + ( transitive-leq-ℝ + ( min-ℝ x (min-ℝ y z)) + ( min-ℝ y z) + ( y) + ( leq-left-min-ℝ y z) + ( leq-right-min-ℝ x (min-ℝ y z)))) + ( transitive-leq-ℝ + ( min-ℝ x (min-ℝ y z)) + ( min-ℝ y z) + ( z) + ( leq-right-min-ℝ y z) + ( leq-right-min-ℝ x (min-ℝ y z)))) +``` + +### The large semigroup of real numbers under the minimum operator + +```agda +large-semigroup-min-ℝ : Large-Semigroup lsuc +large-semigroup-min-ℝ = make-Large-Semigroup ℝ-Set min-ℝ associative-min-ℝ +``` + +### The semigroup of real numbers under the minimum operator at a given level + +```agda +semigroup-min-ℝ : (l : Level) → Semigroup (lsuc l) +semigroup-min-ℝ = semigroup-Large-Semigroup large-semigroup-min-ℝ +``` + ### The large poset of real numbers has meets ```agda From f91436d57c1be2543acd909e9db1770b0de2cb81 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 30 Oct 2025 02:21:35 +0100 Subject: [PATCH 2/3] Update src/real-numbers/binary-maximum-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/binary-maximum-real-numbers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md index ef34da8c2e4..339cfb5970d 100644 --- a/src/real-numbers/binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md @@ -207,8 +207,8 @@ module _ ```agda module _ - {lx ly lz : Level} - (x : ℝ lx) (y : ℝ ly) (z : ℝ lz) + {l1 l2 l3 : Level} + (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract From 4c4751532468824d214e40a1ca7aa45f56c378b5 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 30 Oct 2025 02:21:48 +0100 Subject: [PATCH 3/3] Update src/real-numbers/binary-minimum-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/binary-minimum-real-numbers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/binary-minimum-real-numbers.lagda.md b/src/real-numbers/binary-minimum-real-numbers.lagda.md index dc7deece3e7..519a7fab77e 100644 --- a/src/real-numbers/binary-minimum-real-numbers.lagda.md +++ b/src/real-numbers/binary-minimum-real-numbers.lagda.md @@ -139,8 +139,8 @@ module _ ```agda module _ - {lx ly lz : Level} - (x : ℝ lx) (y : ℝ ly) (z : ℝ lz) + {l1 l2 l3 : Level} + (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract