From 03bf44ad7a0a2f1cedef740c7b79932569cb3dfd Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 8 Feb 2025 19:38:46 -0800 Subject: [PATCH 01/73] Do syntax for elim-exists chains, including application to strict real inequality --- .../existential-quantification.lagda.md | 18 +++ .../strict-inequality-real-numbers.lagda.md | 152 +++++++----------- 2 files changed, 79 insertions(+), 91 deletions(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index a15d2258a9..1cd6eb79f9 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -331,6 +331,24 @@ module _ eq-distributive-product-exists-structure P ``` +## Existential quantification `do` syntax + +When eliminating a chain of existential quantifications, which may be +interdependent, Agda's `do` syntax can eliminate many levels of nesting. + +```agda +module elim-exists-do + {l : Level} + (P : Prop l) + where + + _>>=_ : + {l1 l2 : Level} {A : UU l1} {B : A -> UU l2} → + exists-structure A B → + (Σ A B -> type-Prop P) -> type-Prop P + x >>= f = elim-exists P (ev-pair f) x +``` + ## See also - Existential quantification is the indexed counterpart to diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md index c37393a0ca..da7259e97c 100644 --- a/src/real-numbers/strict-inequality-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md @@ -20,10 +20,12 @@ open import foundation.disjunction open import foundation.empty-types open import foundation.existential-quantification open import foundation.function-types +open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation open import foundation.propositions +open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels @@ -90,28 +92,24 @@ module _ asymmetric-le-ℝ : le-ℝ x y → ¬ (le-ℝ y x) asymmetric-le-ℝ x Date: Sat, 8 Feb 2025 19:42:58 -0800 Subject: [PATCH 02/73] Simplifications and indentation --- .../strict-inequality-real-numbers.lagda.md | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md index da7259e97c..d4ff970765 100644 --- a/src/real-numbers/strict-inequality-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md @@ -96,18 +96,14 @@ module _ p , x

Date: Sat, 8 Feb 2025 19:44:11 -0800 Subject: [PATCH 03/73] make pre-commit --- src/foundation/existential-quantification.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index 1cd6eb79f9..eaf1a65d1c 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -343,7 +343,7 @@ module elim-exists-do where _>>=_ : - {l1 l2 : Level} {A : UU l1} {B : A -> UU l2} → + {l1 l2 : Level} {A : UU l1} {B : A -> UU l2} → exists-structure A B → (Σ A B -> type-Prop P) -> type-Prop P x >>= f = elim-exists P (ev-pair f) x From 5481940316c92867e55b94c467eb6c4187b9009b Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 09:25:08 -0800 Subject: [PATCH 04/73] Updates --- .../existential-quantification.lagda.md | 26 +++++++++++++++-- .../strict-inequality-real-numbers.lagda.md | 28 +++++++++---------- 2 files changed, 38 insertions(+), 16 deletions(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index eaf1a65d1c..23d53d9417 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -334,10 +334,32 @@ module _ ## Existential quantification `do` syntax When eliminating a chain of existential quantifications, which may be -interdependent, Agda's `do` syntax can eliminate many levels of nesting. +interdependent, [Agda's `do` syntax](https://agda.readthedocs.io/en/stable/language/syntactic-sugar.html#do-notation) can eliminate many levels of nesting. + +For example, suppose we have + +```text +R : Prop l + +exists-a-p : exists A P +a-p-implies-b-q-exists : (a : A) → P a → exists B Q +a-b-p-q-implies-r : (a : A) (b : B) → P a → Q b → R +``` + +To deduce `R`, we could write + +```text +do + a , pa ← exists-a-p + b , qb ← a-p-implies-b-q-exists a pa + a-b-p-q-implies-r a b pa qb +where open do-syntax-elim-exists R +``` + +instead of a nested chain of `elim-exists`. ```agda -module elim-exists-do +module do-syntax-elim-exists {l : Level} (P : Prop l) where diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md index d4ff970765..e6c6041f4b 100644 --- a/src/real-numbers/strict-inequality-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md @@ -105,7 +105,7 @@ module _ ( q) ( le-lower-upper-cut-ℝ y p q p Date: Sun, 9 Feb 2025 09:26:52 -0800 Subject: [PATCH 05/73] make pre-commit --- src/foundation/existential-quantification.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index 23d53d9417..04483c575f 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -334,7 +334,9 @@ module _ ## Existential quantification `do` syntax When eliminating a chain of existential quantifications, which may be -interdependent, [Agda's `do` syntax](https://agda.readthedocs.io/en/stable/language/syntactic-sugar.html#do-notation) can eliminate many levels of nesting. +interdependent, +[Agda's `do` syntax](https://agda.readthedocs.io/en/stable/language/syntactic-sugar.html#do-notation) +can eliminate many levels of nesting. For example, suppose we have From e84f3ce826860e6f38873509b2a003be10f799a2 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 10:22:00 -0800 Subject: [PATCH 06/73] Define Minkowski multiplication for semigroups --- ...nkowski-multiplication-semigroups.lagda.md | 144 ++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 src/group-theory/minkowski-multiplication-semigroups.lagda.md diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md new file mode 100644 index 0000000000..1978d3b786 --- /dev/null +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -0,0 +1,144 @@ +# Minkowski multiplication of semigroup subtypes + +```agda +module group-theory.minkowski-multiplication-semigroups where +``` + +

Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.semigroups +``` + +
+ +## Idea + +For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of `A` and `B` is the set +of elements that can be formed by multiplying an element of `A` and an element +of `B`. (This is more usually referred to as a Minkowski sum, but as the +operation on semigroups is referred to as `mul`, we use multiplicative +terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (G : Semigroup l1) + (A : subtype l2 (type-Semigroup G)) + (B : subtype l3 (type-Semigroup G)) + where + + minkowski-mul-Semigroup : subtype (l1 ⊔ l2 ⊔ l3) (type-Semigroup G) + minkowski-mul-Semigroup c = + ∃ + ( type-Semigroup G × type-Semigroup G) + ( λ (a , b) → + A a ∧ B b ∧ Id-Prop (set-Semigroup G) c (mul-Semigroup G a b)) +``` + +## Properties + +### Minkowski multiplication of semigroup subtypes is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (A : subtype l2 (type-Semigroup G)) + (B : subtype l3 (type-Semigroup G)) + (C : subtype l4 (type-Semigroup G)) + where + + associative-minkowski-mul-has-same-elements-subtype-Semigroup : + has-same-elements-subtype + ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) + ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) + pr1 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + elim-exists + ( claim) + ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) → + elim-exists + ( claim) + ( λ (a , b) (a∈A , b∈B , ab=a*b) → + intro-exists + ( a , mul-Semigroup G b c) + ( a∈A , + intro-exists (b , c) (b∈B , c∈C , refl) , + ( equational-reasoning + x + = mul-Semigroup G ab c by x=ab*c + = mul-Semigroup G (mul-Semigroup G a b) c + by ap (mul-Semigroup' G c) ab=a*b + = mul-Semigroup G a (mul-Semigroup G b c) + by associative-mul-Semigroup G a b c))) + ( ab∈AB)) + where + claim = + minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x + pr2 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + elim-exists + ( claim) + ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) → + elim-exists + ( claim) + ( λ (b , c) (b∈B , c∈C , bc=b*c) → + intro-exists + ( mul-Semigroup G a b , c) + ( intro-exists (a , b) (a∈A , b∈B , refl) , + c∈C , + ( equational-reasoning + x + = mul-Semigroup G a bc by x=a*bc + = mul-Semigroup G a (mul-Semigroup G b c) + by ap (mul-Semigroup G a) bc=b*c + = mul-Semigroup G (mul-Semigroup G a b) c + by inv (associative-mul-Semigroup G a b c)))) + ( bc∈BC)) + where + claim = + minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C x + + associative-minkowski-mul-Semigroup : + minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C = + minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) + associative-minkowski-mul-Semigroup = + eq-has-same-elements-subtype + ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) + ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) + ( associative-minkowski-mul-has-same-elements-subtype-Semigroup) +``` + +### Minkowski multiplication of subtypes of a semigroup forms a semigroup + +```agda +module _ + {l1 : Level} + (G : Semigroup l1) + where + + semigroup-minkowski-mul-Semigroup : + (l : Level) → Semigroup (lsuc l1 ⊔ lsuc l) + pr1 (semigroup-minkowski-mul-Semigroup l) = + subtype-Set (l1 ⊔ l) (type-Semigroup G) + pr1 (pr2 (semigroup-minkowski-mul-Semigroup l)) = minkowski-mul-Semigroup G + pr2 (pr2 (semigroup-minkowski-mul-Semigroup l)) = + associative-minkowski-mul-Semigroup G +``` + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia From 4f547c83691fc800d61a68d06f0518ac0ad1b514 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 10:22:39 -0800 Subject: [PATCH 07/73] make pre-commit --- src/group-theory.lagda.md | 1 + .../minkowski-multiplication-semigroups.lagda.md | 10 +++++----- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 962a96a816..1233b0af98 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -116,6 +116,7 @@ open import group-theory.large-semigroups public open import group-theory.loop-groups-sets public open import group-theory.mere-equivalences-concrete-group-actions public open import group-theory.mere-equivalences-group-actions public +open import group-theory.minkowski-multiplication-semigroups public open import group-theory.monoid-actions public open import group-theory.monoids public open import group-theory.monomorphisms-concrete-groups public diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 1978d3b786..e4a81a386c 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -25,11 +25,11 @@ open import group-theory.semigroups ## Idea -For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of `A` and `B` is the set -of elements that can be formed by multiplying an element of `A` and an element -of `B`. (This is more usually referred to as a Minkowski sum, but as the -operation on semigroups is referred to as `mul`, we use multiplicative -terminology.) +For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on semigroups is referred to as `mul`, we use +multiplicative terminology.) ## Definition From ab87dac060d95050de28e5aa81fd4830ceb99c50 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:15:39 -0800 Subject: [PATCH 08/73] Add monoids and commutative monoids --- ...ultiplication-commutative-monoids.lagda.md | 116 +++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 138 ++++++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 17 +-- src/group-theory/monoids.lagda.md | 6 + 4 files changed, 268 insertions(+), 9 deletions(-) create mode 100644 src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md create mode 100644 src/group-theory/minkowski-multiplication-monoids.lagda.md diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md new file mode 100644 index 0000000000..f85d234c4a --- /dev/null +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -0,0 +1,116 @@ +# Minkowski multiplication of commutative monoid subtypes + +```agda +module group-theory.minkowski-multiplication-commutative-monoids where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.powersets +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.minkowski-multiplication-monoids +open import group-theory.commutative-monoids +open import group-theory.monoids +``` + +
+ +## Idea + +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on commutative monoids is referred to as `mul`, we use +multiplicative terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + minkowski-mul-Commutative-Monoid : + subtype (l1 ⊔ l2 ⊔ l3) (type-Commutative-Monoid M) + minkowski-mul-Commutative-Monoid = + minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B +``` + +## Properties + +### Minkowski multiplication on a commutative monoid is commutative + +```agda +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + commutative-minkowski-mul-leq-Commutative-Monoid : + minkowski-mul-Commutative-Monoid M A B ⊆ + minkowski-mul-Commutative-Monoid M B A + commutative-minkowski-mul-leq-Commutative-Monoid x = + elim-exists + (minkowski-mul-Commutative-Monoid M B A x) + ( λ (a , b) (a∈A , b∈B , x=ab) → + intro-exists + ( b , a) + ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b)) + +module _ + {l1 l2 l3 : Level} + (M : Commutative-Monoid l1) + (A : subtype l2 (type-Commutative-Monoid M)) + (B : subtype l3 (type-Commutative-Monoid M)) + where + + commutative-minkowski-mul-Commutative-Monoid : + minkowski-mul-Commutative-Monoid M A B = + minkowski-mul-Commutative-Monoid M B A + commutative-minkowski-mul-Commutative-Monoid = + antisymmetric-sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M B A) + ( commutative-minkowski-mul-leq-Commutative-Monoid M A B , + commutative-minkowski-mul-leq-Commutative-Monoid M B A) +``` + +### Minkowski multiplication on a commutative monoid is a commutative monoid + +```agda +module _ + {l : Level} + (M : Commutative-Monoid l) + where + + commutative-monoid-minkowski-mul-Commutative-Monoid : + Commutative-Monoid (lsuc l) + pr1 commutative-monoid-minkowski-mul-Commutative-Monoid = + monoid-minkowski-mul-Monoid (monoid-Commutative-Monoid M) + pr2 commutative-monoid-minkowski-mul-Commutative-Monoid = + commutative-minkowski-mul-Commutative-Monoid M +``` + +## See also + +- Minkowski multiplication on semigroups is defined in + [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). +- Minkowski multiplication on monoids is defined in + [`group-theory.minkowski-multiplication-monoids`](group-theory.minkowski-multiplication-monoids.md). + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md new file mode 100644 index 0000000000..88de396de6 --- /dev/null +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -0,0 +1,138 @@ +# Minkowski multiplication of monoid subtypes + +```agda +module group-theory.minkowski-multiplication-monoids where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.powersets +open import foundation.unital-binary-operations +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import group-theory.minkowski-multiplication-semigroups +open import group-theory.monoids +open import group-theory.semigroups +``` + +
+ +## Idea + +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of +`A` and `B` is the set of elements that can be formed by multiplying an element +of `A` and an element of `B`. (This is more usually referred to as a Minkowski +sum, but as the operation on monoids is referred to as `mul`, we use +multiplicative terminology.) + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} + (M : Monoid l1) + (A : subtype l2 (type-Monoid M)) + (B : subtype l3 (type-Monoid M)) + where + + minkowski-mul-Monoid : subtype (l1 ⊔ l2 ⊔ l3) (type-Monoid M) + minkowski-mul-Monoid = minkowski-mul-Semigroup (semigroup-Monoid M) A B +``` + +## Properties + +### Unit laws for Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 : Level} + (M : Monoid l1) + (A : subtype l2 (type-Monoid M)) + where + + left-unit-law-minkowski-mul-Monoid : + sim-subtype (minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A) A + pr1 left-unit-law-minkowski-mul-Monoid a = + elim-exists + ( A a) + ( λ (z , a') (z=1 , a'∈A , a=za') → + tr + ( is-in-subtype A) + ( inv + ( equational-reasoning + a + = mul-Monoid M z a' by a=za' + = mul-Monoid M (unit-Monoid M) a' by ap (mul-Monoid' M a') z=1 + = a' by left-unit-law-mul-Monoid M a')) + ( a'∈A)) + pr2 left-unit-law-minkowski-mul-Monoid a a∈A = + intro-exists + ( unit-Monoid M , a) + ( refl , a∈A , inv (left-unit-law-mul-Monoid M a)) + + right-unit-law-minkowski-mul-Monoid : + sim-subtype (minkowski-mul-Monoid M A (is-unit-Monoid-Prop M)) A + pr1 right-unit-law-minkowski-mul-Monoid a = + elim-exists + ( A a) + ( λ (a' , z) (a'∈A , z=1 , a=a'z) → + tr + ( is-in-subtype A) + ( inv + ( equational-reasoning + a + = mul-Monoid M a' z by a=a'z + = mul-Monoid M a' (unit-Monoid M) by ap (mul-Monoid M a') z=1 + = a' by right-unit-law-mul-Monoid M a')) + ( a'∈A)) + pr2 right-unit-law-minkowski-mul-Monoid a a∈A = + intro-exists + ( a , unit-Monoid M) + ( a∈A , refl , inv (right-unit-law-mul-Monoid M a)) +``` + +### Minkowski multiplication of subtypes of a monoid forms a monoid + +```agda +module _ + {l : Level} + (M : Monoid l) + where + + is-unital-minkowski-mul-Monoid : + is-unital (minkowski-mul-Monoid {l} {l} {l} M) + pr1 is-unital-minkowski-mul-Monoid = is-unit-Monoid-Prop M + pr1 (pr2 is-unital-minkowski-mul-Monoid) A = + antisymmetric-sim-subtype + ( minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A) + ( A) + ( left-unit-law-minkowski-mul-Monoid M A) + pr2 (pr2 is-unital-minkowski-mul-Monoid) A = + antisymmetric-sim-subtype + ( minkowski-mul-Monoid M A (is-unit-Monoid-Prop M)) + ( A) + ( right-unit-law-minkowski-mul-Monoid M A) + + monoid-minkowski-mul-Monoid : Monoid (lsuc l) + pr1 monoid-minkowski-mul-Monoid = + semigroup-minkowski-mul-Semigroup (semigroup-Monoid M) + pr2 monoid-minkowski-mul-Monoid = is-unital-minkowski-mul-Monoid +``` + +## See also + +- Minkowski multiplication on semigroups is defined in + [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). + +## External links + +- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at + Wikipedia diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index e4a81a386c..4fd589d0d2 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -25,7 +25,8 @@ open import group-theory.semigroups ## Idea -For two subtypes `A`, `B` of a semigroup `S`, the Minkowski multiplication of +For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, but as the operation on semigroups is referred to as `mul`, we use @@ -125,16 +126,14 @@ module _ ```agda module _ - {l1 : Level} - (G : Semigroup l1) + {l : Level} + (G : Semigroup l) where - semigroup-minkowski-mul-Semigroup : - (l : Level) → Semigroup (lsuc l1 ⊔ lsuc l) - pr1 (semigroup-minkowski-mul-Semigroup l) = - subtype-Set (l1 ⊔ l) (type-Semigroup G) - pr1 (pr2 (semigroup-minkowski-mul-Semigroup l)) = minkowski-mul-Semigroup G - pr2 (pr2 (semigroup-minkowski-mul-Semigroup l)) = + semigroup-minkowski-mul-Semigroup : Semigroup (lsuc l) + pr1 semigroup-minkowski-mul-Semigroup = subtype-Set l (type-Semigroup G) + pr1 (pr2 semigroup-minkowski-mul-Semigroup) = minkowski-mul-Semigroup G + pr2 (pr2 semigroup-minkowski-mul-Semigroup) = associative-minkowski-mul-Semigroup G ``` diff --git a/src/group-theory/monoids.lagda.md b/src/group-theory/monoids.lagda.md index 1e76dbc225..6a0c542cfc 100644 --- a/src/group-theory/monoids.lagda.md +++ b/src/group-theory/monoids.lagda.md @@ -82,6 +82,12 @@ module _ unit-Monoid : type-Monoid unit-Monoid = pr1 has-unit-Monoid + is-unit-Monoid-Prop : type-Monoid → Prop l + is-unit-Monoid-Prop x = Id-Prop set-Monoid x unit-Monoid + + is-unit-Monoid : type-Monoid → UU l + is-unit-Monoid x = x = unit-Monoid + left-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid unit-Monoid x = x left-unit-law-mul-Monoid = pr1 (pr2 has-unit-Monoid) From 1f8bb30ec86e99692a98eecfcc9f829029aa45ac Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:16:52 -0800 Subject: [PATCH 09/73] make pre-commit --- src/group-theory.lagda.md | 2 ++ ...owski-multiplication-commutative-monoids.lagda.md | 12 ++++++------ .../minkowski-multiplication-monoids.lagda.md | 12 ++++++------ .../minkowski-multiplication-semigroups.lagda.md | 8 ++++---- 4 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 1233b0af98..3c4fb0e591 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -116,6 +116,8 @@ open import group-theory.large-semigroups public open import group-theory.loop-groups-sets public open import group-theory.mere-equivalences-concrete-group-actions public open import group-theory.mere-equivalences-group-actions public +open import group-theory.minkowski-multiplication-commutative-monoids public +open import group-theory.minkowski-multiplication-monoids public open import group-theory.minkowski-multiplication-semigroups public open import group-theory.monoid-actions public open import group-theory.monoids public diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index f85d234c4a..90d8c9c2a6 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -14,8 +14,8 @@ open import foundation.powersets open import foundation.subtypes open import foundation.universe-levels -open import group-theory.minkowski-multiplication-monoids open import group-theory.commutative-monoids +open import group-theory.minkowski-multiplication-monoids open import group-theory.monoids ``` @@ -24,11 +24,11 @@ open import group-theory.monoids ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on commutative monoids is referred to as `mul`, we use -multiplicative terminology.) +[commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski +multiplication of `A` and `B` is the set of elements that can be formed by +multiplying an element of `A` and an element of `B`. (This is more usually +referred to as a Minkowski sum, but as the operation on commutative monoids is +referred to as `mul`, we use multiplicative terminology.) ## Definition diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 88de396de6..34ceb6b961 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -12,9 +12,9 @@ open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets -open import foundation.unital-binary-operations open import foundation.subtypes open import foundation.transport-along-identifications +open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.minkowski-multiplication-semigroups @@ -27,11 +27,11 @@ open import group-theory.semigroups ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on monoids is referred to as `mul`, we use -multiplicative terminology.) +[monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of `A` and +`B` is the set of elements that can be formed by multiplying an element of `A` +and an element of `B`. (This is more usually referred to as a Minkowski sum, but +as the operation on monoids is referred to as `mul`, we use multiplicative +terminology.) ## Definition diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 4fd589d0d2..3c6e307454 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -26,10 +26,10 @@ open import group-theory.semigroups ## Idea For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a -[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of -`A` and `B` is the set of elements that can be formed by multiplying an element -of `A` and an element of `B`. (This is more usually referred to as a Minkowski -sum, but as the operation on semigroups is referred to as `mul`, we use +[semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` +and `B` is the set of elements that can be formed by multiplying an element of +`A` and an element of `B`. (This is more usually referred to as a Minkowski sum, +but as the operation on semigroups is referred to as `mul`, we use multiplicative terminology.) ## Definition From 4581333c10e4b668df65a2f0a33378d7c1e28e78 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:27:12 -0800 Subject: [PATCH 10/73] Use subset syntax --- ...ultiplication-commutative-monoids.lagda.md | 17 +++++----- .../minkowski-multiplication-monoids.lagda.md | 13 ++++---- ...nkowski-multiplication-semigroups.lagda.md | 32 ++++++++++--------- 3 files changed, 33 insertions(+), 29 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 90d8c9c2a6..1d5453d267 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -17,13 +17,14 @@ open import foundation.universe-levels open import group-theory.commutative-monoids open import group-theory.minkowski-multiplication-monoids open import group-theory.monoids +open import group-theory.subsets-commutative-monoids ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-commutative-monoids.md) `A`, `B` of a [commutative monoid](group-theory.commutative-monoids.md) `M`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually @@ -36,12 +37,12 @@ referred to as `mul`, we use multiplicative terminology.) module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where minkowski-mul-Commutative-Monoid : - subtype (l1 ⊔ l2 ⊔ l3) (type-Commutative-Monoid M) + subset-Commutative-Monoid (l1 ⊔ l2 ⊔ l3) M minkowski-mul-Commutative-Monoid = minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B ``` @@ -54,8 +55,8 @@ module _ module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where commutative-minkowski-mul-leq-Commutative-Monoid : @@ -72,8 +73,8 @@ module _ module _ {l1 l2 l3 : Level} (M : Commutative-Monoid l1) - (A : subtype l2 (type-Commutative-Monoid M)) - (B : subtype l3 (type-Commutative-Monoid M)) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) where commutative-minkowski-mul-Commutative-Monoid : diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 34ceb6b961..6d51224108 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -20,13 +20,14 @@ open import foundation.universe-levels open import group-theory.minkowski-multiplication-semigroups open import group-theory.monoids open import group-theory.semigroups +open import group-theory.subsets-monoids ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-monoids.md) `A`, `B` of a [monoid](group-theory.monoids.md) `M`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, but @@ -39,23 +40,23 @@ terminology.) module _ {l1 l2 l3 : Level} (M : Monoid l1) - (A : subtype l2 (type-Monoid M)) - (B : subtype l3 (type-Monoid M)) + (A : subset-Monoid l2 M) + (B : subset-Monoid l3 M) where - minkowski-mul-Monoid : subtype (l1 ⊔ l2 ⊔ l3) (type-Monoid M) + minkowski-mul-Monoid : subset-Monoid (l1 ⊔ l2 ⊔ l3) M minkowski-mul-Monoid = minkowski-mul-Semigroup (semigroup-Monoid M) A B ``` ## Properties -### Unit laws for Minkowski multiplication of semigroup subtypes +### Unit laws for Minkowski multiplication of monoid subsets ```agda module _ {l1 l2 : Level} (M : Monoid l1) - (A : subtype l2 (type-Monoid M)) + (A : subset-Monoid l2 M) where left-unit-law-minkowski-mul-Monoid : diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 3c6e307454..0587640fe3 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -13,19 +13,21 @@ open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels open import group-theory.semigroups +open import group-theory.subsets-semigroups ``` ## Idea -For two [subtypes](foundation-core.subtypes.md) `A`, `B` of a +For two [subsets](group-theory.subsets-semigroups.md) `A`, `B` of a [semigroup](group-theory.semigroups.md) `S`, the Minkowski multiplication of `A` and `B` is the set of elements that can be formed by multiplying an element of `A` and an element of `B`. (This is more usually referred to as a Minkowski sum, @@ -38,11 +40,11 @@ multiplicative terminology.) module _ {l1 l2 l3 : Level} (G : Semigroup l1) - (A : subtype l2 (type-Semigroup G)) - (B : subtype l3 (type-Semigroup G)) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) where - minkowski-mul-Semigroup : subtype (l1 ⊔ l2 ⊔ l3) (type-Semigroup G) + minkowski-mul-Semigroup : subset-Semigroup (l1 ⊔ l2 ⊔ l3) G minkowski-mul-Semigroup c = ∃ ( type-Semigroup G × type-Semigroup G) @@ -52,22 +54,22 @@ module _ ## Properties -### Minkowski multiplication of semigroup subtypes is associative +### Minkowski multiplication of semigroup subsets is associative ```agda module _ {l1 l2 l3 l4 : Level} (G : Semigroup l1) - (A : subtype l2 (type-Semigroup G)) - (B : subtype l3 (type-Semigroup G)) - (C : subtype l4 (type-Semigroup G)) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) + (C : subset-Semigroup l4 G) where - associative-minkowski-mul-has-same-elements-subtype-Semigroup : - has-same-elements-subtype + associative-minkowski-mul-sim-Semigroup : + sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - pr1 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + pr1 associative-minkowski-mul-sim-Semigroup x = elim-exists ( claim) ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) → @@ -89,7 +91,7 @@ module _ where claim = minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x - pr2 (associative-minkowski-mul-has-same-elements-subtype-Semigroup x) = + pr2 associative-minkowski-mul-sim-Semigroup x = elim-exists ( claim) ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) → @@ -116,13 +118,13 @@ module _ minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C = minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) associative-minkowski-mul-Semigroup = - eq-has-same-elements-subtype + antisymmetric-sim-subtype ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C) ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)) - ( associative-minkowski-mul-has-same-elements-subtype-Semigroup) + ( associative-minkowski-mul-sim-Semigroup) ``` -### Minkowski multiplication of subtypes of a semigroup forms a semigroup +### Minkowski multiplication of subsets of a semigroup forms a semigroup ```agda module _ From 6a9f8370e6b7eeb750fce2777014954461265d16 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:54:20 -0800 Subject: [PATCH 11/73] Define lower Dedekind cuts/reals --- .../lower-dedekind-real-numbers.lagda.md | 115 ++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 src/real-numbers/lower-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..58b8384159 --- /dev/null +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -0,0 +1,115 @@ +# Lower Dedekind real numbers + +```agda +module real-numbers.lower-dedekind-real-numbers where +``` + +
Imports +```agda +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.subtypes +open import foundation.conjunction +open import foundation.identity-types +open import foundation.existential-quantification +open import foundation.propositions +open import foundation.logical-equivalences +open import foundation.universe-levels +open import foundation.universal-quantification +``` + +
+## Idea + +A lower +{{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} +consists of a +[subtype](foundation-core.subtypes.md) `L` of +[the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, +satisfying the following two conditions: + +1. _Inhabitedness_. `L` is [inhabited](foundation.inhabited-subtypes.md). +2. _Roundedness_. A rational number `q` is in `L` + [if and only if](foundation.logical-equivalences.md) there + [exists](foundation.existential-quantification.md) `q < r` such that `r ∈ L`. + +The type of all lower Dedekind real numbers is the type of all lower Dedekind cuts. +A lower Dedekind cut is part of a [Dedekind real number](real-numbers.dedekind-real-numbers.md) + +## Definition + +### Lower Dedekind cuts + +```agda +module _ + {l : Level} + (L : subtype l ℚ) + where + + is-lower-dedekind-cut-Prop : Prop l + is-lower-dedekind-cut-Prop = + (∃ ℚ L) ∧ + (∀' ℚ (λ q → L q ⇔ (∃ ℚ (λ r → le-ℚ-Prop q r ∧ L r)))) + + is-lower-dedekind-cut : UU l + is-lower-dedekind-cut = type-Prop is-lower-dedekind-cut-Prop +``` + +## The lower Dedekind real numbers + +```agda +lower-ℝ : (l : Level) → UU (lsuc l) +lower-ℝ l = Σ (subtype l ℚ) is-lower-dedekind-cut + +module _ + {l : Level} + (x : lower-ℝ l) + where + + cut-lower-ℝ : subtype l ℚ + cut-lower-ℝ = pr1 x + + is-in-cut-lower-ℝ : ℚ → UU l + is-in-cut-lower-ℝ = is-in-subtype cut-lower-ℝ + + is-inhabited-lower-ℝ : exists ℚ cut-lower-ℝ + is-inhabited-lower-ℝ = pr1 (pr2 x) + + is-rounded-lower-ℝ : + (q : ℚ) → + is-in-cut-lower-ℝ q ↔ exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-lower-ℝ r) + is-rounded-lower-ℝ = pr2 (pr2 x) +``` + +## Properties + +### Lower Dedekind cuts are closed under the standard ordering on the rationals + +```agda +module _ + {l : Level} (x : lower-ℝ l) (p q : ℚ) + where + + le-cut-lower-ℝ : le-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p + le-cut-lower-ℝ p Date: Sun, 9 Feb 2025 11:54:56 -0800 Subject: [PATCH 12/73] make pre-commit --- src/real-numbers.lagda.md | 1 + .../lower-dedekind-real-numbers.lagda.md | 22 ++++++++++--------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index b2aaa1a1f4..6fc691eef0 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -8,6 +8,7 @@ module real-numbers where open import real-numbers.arithmetically-located-dedekind-cuts public open import real-numbers.dedekind-real-numbers public open import real-numbers.inequality-real-numbers public +open import real-numbers.lower-dedekind-real-numbers public open import real-numbers.metric-space-of-real-numbers public open import real-numbers.negation-real-numbers public open import real-numbers.rational-real-numbers public diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 58b8384159..5d99526167 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -5,19 +5,20 @@ module real-numbers.lower-dedekind-real-numbers where ```
Imports + ```agda open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers -open import foundation.dependent-pair-types -open import foundation.subtypes open import foundation.conjunction -open import foundation.identity-types +open import foundation.dependent-pair-types open import foundation.existential-quantification -open import foundation.propositions +open import foundation.identity-types open import foundation.logical-equivalences -open import foundation.universe-levels +open import foundation.propositions +open import foundation.subtypes open import foundation.universal-quantification +open import foundation.universe-levels ```
@@ -25,8 +26,7 @@ open import foundation.universal-quantification A lower {{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} -consists of a -[subtype](foundation-core.subtypes.md) `L` of +consists of a [subtype](foundation-core.subtypes.md) `L` of [the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, satisfying the following two conditions: @@ -35,8 +35,9 @@ satisfying the following two conditions: [if and only if](foundation.logical-equivalences.md) there [exists](foundation.existential-quantification.md) `q < r` such that `r ∈ L`. -The type of all lower Dedekind real numbers is the type of all lower Dedekind cuts. -A lower Dedekind cut is part of a [Dedekind real number](real-numbers.dedekind-real-numbers.md) +The type of all lower Dedekind real numbers is the type of all lower Dedekind +cuts. A lower Dedekind cut is part of a +[Dedekind real number](real-numbers.dedekind-real-numbers.md) ## Definition @@ -110,6 +111,7 @@ module _ ## References -This page follows the terminology used in the exercises of Section 11 in {{#cite UF13}}. +This page follows the terminology used in the exercises of Section 11 in +{{#cite UF13}}. {{#bibliography}} From 59195c9edc8dfc2117df76628621a2767981ea31 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 11:59:55 -0800 Subject: [PATCH 13/73] Define upper Dedekind reals --- .../lower-dedekind-real-numbers.lagda.md | 10 +- .../upper-dedekind-real-numbers.lagda.md | 124 ++++++++++++++++++ 2 files changed, 132 insertions(+), 2 deletions(-) create mode 100644 src/real-numbers/upper-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 5d99526167..f603657ab7 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -36,8 +36,7 @@ satisfying the following two conditions: [exists](foundation.existential-quantification.md) `q < r` such that `r ∈ L`. The type of all lower Dedekind real numbers is the type of all lower Dedekind -cuts. A lower Dedekind cut is part of a -[Dedekind real number](real-numbers.dedekind-real-numbers.md) +cuts. ## Definition @@ -109,6 +108,13 @@ module _ eq-eq-cut-lower-ℝ = eq-type-subtype is-lower-dedekind-cut-Prop ``` +## See also + +- Upper Dedekind cuts, the dual structure, are defined in + [`real-numbers.upper-dedekind-real-numbers`](real-numbers.upper-dedekind-real-numbers.md). +- Dedekind cuts, which form the usual real numbers, are defined in + [`real-numbers.dedekind-real-numbers`](real-numbers.dedekind-real-numbers.md) + ## References This page follows the terminology used in the exercises of Section 11 in diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..bdf0a5525f --- /dev/null +++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md @@ -0,0 +1,124 @@ +# Upper Dedekind real numbers + +```agda +module real-numbers.upper-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.subtypes +open import foundation.universal-quantification +open import foundation.universe-levels +``` + +
+ +## Idea + +A upper +{{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} +consists of a [subtype](foundation-core.subtypes.md) `U` of +[the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, +satisfying the following two conditions: + +1. _Inhabitedness_. `U` is [inhabited](foundation.inhabited-subtypes.md). +2. _Roundedness_. A rational number `q` is in `U` + [if and only if](foundation.logical-equivalences.md) there + [exists](foundation.existential-quantification.md) `p < q` such that `p ∈ U`. + +The type of all upper Dedekind real numbers is the type of all upper Dedekind +cuts. + +## Definition + +### Upper Dedekind cuts + +```agda +module _ + {l : Level} + (U : subtype l ℚ) + where + + is-upper-dedekind-cut-Prop : Prop l + is-upper-dedekind-cut-Prop = + (∃ ℚ U) ∧ + (∀' ℚ (λ q → U q ⇔ (∃ ℚ (λ p → le-ℚ-Prop p q ∧ U p)))) + + is-upper-dedekind-cut : UU l + is-upper-dedekind-cut = type-Prop is-upper-dedekind-cut-Prop +``` + +## The upper Dedekind real numbers + +```agda +upper-ℝ : (l : Level) → UU (lsuc l) +upper-ℝ l = Σ (subtype l ℚ) is-upper-dedekind-cut + +module _ + {l : Level} + (x : upper-ℝ l) + where + + cut-upper-ℝ : subtype l ℚ + cut-upper-ℝ = pr1 x + + is-in-cut-upper-ℝ : ℚ → UU l + is-in-cut-upper-ℝ = is-in-subtype cut-upper-ℝ + + is-inhabited-upper-ℝ : exists ℚ cut-upper-ℝ + is-inhabited-upper-ℝ = pr1 (pr2 x) + + is-rounded-upper-ℝ : + (q : ℚ) → + is-in-cut-upper-ℝ q ↔ exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-upper-ℝ p) + is-rounded-upper-ℝ = pr2 (pr2 x) +``` + +## Properties + +### Upper Dedekind cuts are closed under the standard ordering on the rationals + +```agda +module _ + {l : Level} (x : upper-ℝ l) (p q : ℚ) + where + + le-cut-upper-ℝ : le-ℚ p q → is-in-cut-upper-ℝ x p → is-in-cut-upper-ℝ x q + le-cut-upper-ℝ p Date: Sun, 9 Feb 2025 12:00:27 -0800 Subject: [PATCH 14/73] make pre-commit --- src/real-numbers.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 6fc691eef0..b110b77299 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -14,4 +14,5 @@ open import real-numbers.negation-real-numbers public open import real-numbers.rational-real-numbers public open import real-numbers.similarity-real-numbers public open import real-numbers.strict-inequality-real-numbers public +open import real-numbers.upper-dedekind-real-numbers public ``` From 0bd35b87219cd5d8601ed56d78fe283e9015b258 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:08:53 -0800 Subject: [PATCH 15/73] Start defining lower addition --- ...dditive-group-of-rational-numbers.lagda.md | 7 ++- ...ition-lower-dedekind-real-numbers.lagda.md | 58 +++++++++++++++++++ .../lower-dedekind-real-numbers.lagda.md | 1 + 3 files changed, 65 insertions(+), 1 deletion(-) create mode 100644 src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md diff --git a/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md index 60aeaf1fb9..e0e8513c49 100644 --- a/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md @@ -17,6 +17,7 @@ open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.abelian-groups +open import group-theory.commutative-monoids open import group-theory.groups open import group-theory.monoids open import group-theory.semigroups @@ -60,9 +61,13 @@ pr2 (pr2 (pr2 (pr2 group-add-ℚ))) = right-inverse-law-add-ℚ ## Properties -### Tha additive group of rational numbers is commutative +### The additive group of rational numbers is commutative ```agda +commutative-monoid-add-ℚ : Commutative-Monoid lzero +pr1 commutative-monoid-add-ℚ = monoid-add-ℚ +pr2 commutative-monoid-add-ℚ = commutative-add-ℚ + abelian-group-add-ℚ : Ab lzero pr1 abelian-group-add-ℚ = group-add-ℚ pr2 abelian-group-add-ℚ = commutative-add-ℚ diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..03096f38d0 --- /dev/null +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -0,0 +1,58 @@ +# Addition of lower Dedekind real numbers + +```agda +module real-numbers.addition-lower-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.existential-quantification +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.minkowski-multiplication-commutative-monoids + +open import real-numbers.lower-dedekind-real-numbers +``` + +
+ +## Idea + +The sum of two [lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md) +is the Minkowski sum of their cuts. + +```agda +module _ + {l1 l2 : Level} + (x : lower-ℝ l1) + (y : lower-ℝ l2) + where + + cut-add-lower-ℝ : subtype (l1 ⊔ l2) ℚ + cut-add-lower-ℝ = + minkowski-mul-Commutative-Monoid + ( commutative-monoid-add-ℚ) + ( cut-lower-ℝ x) + ( cut-lower-ℝ y) + + is-in-add-lower-ℝ-cut : ℚ → UU (l1 ⊔ l2) + is-in-add-lower-ℝ-cut = is-in-subtype cut-add-lower-ℝ + + -- is-inhabited-add-lower-ℝ : exists ℚ cut-add-lower-ℝ + -- is-inhabited-add-lower-ℝ +``` + +## Properties + +### Addition of lower Dedekind real numbers is commutative + +```agda +-- commutative-add-lower-ℝ : +``` diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index f603657ab7..58c0fa6a7b 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -22,6 +22,7 @@ open import foundation.universe-levels ``` + ## Idea A lower From 258ec997f9af6eddb40b6ff3afbe6f53dfb53537 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:19:23 -0800 Subject: [PATCH 16/73] Inhabitedness --- ...ultiplication-commutative-monoids.lagda.md | 20 ++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 21 ++++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 24 +++++++++++++++++++ 3 files changed, 65 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1d5453d267..1500a3439a 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -11,6 +11,7 @@ open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets +open import foundation.inhabited-subtypes open import foundation.subtypes open import foundation.universe-levels @@ -104,6 +105,25 @@ module _ commutative-minkowski-mul-Commutative-Monoid M ``` +### The Minkowski multiplication of two inhabited subsets of a commutative monoid is inhabited + +```agda +module _ + {l1 : Level} + (M : Commutative-Monoid l1) + where + + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid : + {l2 l3 : Level} → + (A : subset-Commutative-Monoid l2 M) → + (B : subset-Commutative-Monoid l3 M) → + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Commutative-Monoid M A B) + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid = + minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M) +``` + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 6d51224108..5152319062 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -13,6 +13,7 @@ open import foundation.existential-quantification open import foundation.identity-types open import foundation.powersets open import foundation.subtypes +open import foundation.inhabited-subtypes open import foundation.transport-along-identifications open import foundation.unital-binary-operations open import foundation.universe-levels @@ -128,6 +129,26 @@ module _ pr2 monoid-minkowski-mul-Monoid = is-unital-minkowski-mul-Monoid ``` +### The Minkowski multiplication of two inhabited subsets of a monoid is inhabited + +```agda +module _ + {l1 : Level} + (M : Monoid l1) + where + + minkowski-mul-inhabited-is-inhabited-Monoid : + {l2 l3 : Level} → + (A : subset-Monoid l2 M) → + (B : subset-Monoid l3 M) → + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Monoid M A B) + minkowski-mul-inhabited-is-inhabited-Monoid = + minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) +``` + + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index 0587640fe3..ea819dde6b 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -13,12 +13,15 @@ open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels +open import logic.functoriality-existential-quantification + open import group-theory.semigroups open import group-theory.subsets-semigroups ``` @@ -139,6 +142,27 @@ module _ associative-minkowski-mul-Semigroup G ``` +### The Minkowski multiplication of two inhabited subsets of a semigroup is inhabited + +```agda +module _ + {l1 l2 l3 : Level} + (G : Semigroup l1) + (A : subset-Semigroup l2 G) + (B : subset-Semigroup l3 G) + where + + minkowski-mul-inhabited-is-inhabited-Semigroup : + is-inhabited-subtype A → + is-inhabited-subtype B → + is-inhabited-subtype (minkowski-mul-Semigroup G A B) + minkowski-mul-inhabited-is-inhabited-Semigroup = + map-binary-exists + ( is-in-subtype (minkowski-mul-Semigroup G A B)) + ( mul-Semigroup G) + λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl) +``` + ## External links - [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at From 40a9e33195feaa76211760edcf9138d3b4d5f192 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:20:00 -0800 Subject: [PATCH 17/73] make pre-commit --- .../minkowski-multiplication-commutative-monoids.lagda.md | 2 +- src/group-theory/minkowski-multiplication-monoids.lagda.md | 3 +-- src/group-theory/minkowski-multiplication-semigroups.lagda.md | 4 ++-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1500a3439a..1e0ad307f4 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -10,8 +10,8 @@ module group-theory.minkowski-multiplication-commutative-monoids where open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types -open import foundation.powersets open import foundation.inhabited-subtypes +open import foundation.powersets open import foundation.subtypes open import foundation.universe-levels diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index 5152319062..b2e67b3464 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -11,9 +11,9 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types +open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.subtypes -open import foundation.inhabited-subtypes open import foundation.transport-along-identifications open import foundation.unital-binary-operations open import foundation.universe-levels @@ -148,7 +148,6 @@ module _ minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) ``` - ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index ea819dde6b..dae5ef51d5 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -20,10 +20,10 @@ open import foundation.sets open import foundation.subtypes open import foundation.universe-levels -open import logic.functoriality-existential-quantification - open import group-theory.semigroups open import group-theory.subsets-semigroups + +open import logic.functoriality-existential-quantification ``` From f9006be947c95c2221923825e11ebf1c55351921 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:22:27 -0800 Subject: [PATCH 18/73] Progress --- .../addition-lower-dedekind-real-numbers.lagda.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 03096f38d0..c0aa126a41 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -45,8 +45,14 @@ module _ is-in-add-lower-ℝ-cut : ℚ → UU (l1 ⊔ l2) is-in-add-lower-ℝ-cut = is-in-subtype cut-add-lower-ℝ - -- is-inhabited-add-lower-ℝ : exists ℚ cut-add-lower-ℝ - -- is-inhabited-add-lower-ℝ + is-inhabited-add-lower-ℝ : exists ℚ cut-add-lower-ℝ + is-inhabited-add-lower-ℝ = + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid + ( commutative-monoid-add-ℚ) + (cut-lower-ℝ x) + (cut-lower-ℝ y) + {! is-inhabited-cut-lower-ℝ x !} + {! !} ``` ## Properties From 6ad62d519db2b3740365e3f0695413940e5850f8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 12:23:46 -0800 Subject: [PATCH 19/73] Rename things --- .../lower-dedekind-real-numbers.lagda.md | 10 +++++----- .../upper-dedekind-real-numbers.lagda.md | 12 +++++++----- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index f603657ab7..6608478238 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -74,13 +74,13 @@ module _ is-in-cut-lower-ℝ : ℚ → UU l is-in-cut-lower-ℝ = is-in-subtype cut-lower-ℝ - is-inhabited-lower-ℝ : exists ℚ cut-lower-ℝ - is-inhabited-lower-ℝ = pr1 (pr2 x) + is-inhabited-cut-lower-ℝ : exists ℚ cut-lower-ℝ + is-inhabited-cut-lower-ℝ = pr1 (pr2 x) - is-rounded-lower-ℝ : + is-rounded-cut-lower-ℝ : (q : ℚ) → is-in-cut-lower-ℝ q ↔ exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-lower-ℝ r) - is-rounded-lower-ℝ = pr2 (pr2 x) + is-rounded-cut-lower-ℝ = pr2 (pr2 x) ``` ## Properties @@ -94,7 +94,7 @@ module _ le-cut-lower-ℝ : le-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p le-cut-lower-ℝ p Date: Sun, 9 Feb 2025 13:43:23 -0800 Subject: [PATCH 20/73] Finish defining addition on lower reals --- .../positive-rational-numbers.lagda.md | 28 ++-- ...trict-inequality-rational-numbers.lagda.md | 32 +++-- src/group-theory/abelian-groups.lagda.md | 23 ++-- ...ition-lower-dedekind-real-numbers.lagda.md | 128 +++++++++++++++++- 4 files changed, 165 insertions(+), 46 deletions(-) diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md index 63ae446cfa..88b15da00e 100644 --- a/src/elementary-number-theory/positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md @@ -190,13 +190,14 @@ module _ (x y : ℚ) (H : le-ℚ x y) where - is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x) - is-positive-diff-le-ℚ = - is-positive-le-zero-ℚ - ( y -ℚ x) - ( backward-implication - ( iff-translate-diff-le-zero-ℚ x y) - ( H)) + abstract + is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x) + is-positive-diff-le-ℚ = + is-positive-le-zero-ℚ + ( y -ℚ x) + ( backward-implication + ( iff-translate-diff-le-zero-ℚ x y) + ( H)) positive-diff-le-ℚ : ℚ⁺ positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ @@ -539,12 +540,13 @@ mediant-zero-ℚ⁺ x = ( rational-ℚ⁺ x) ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x)))) -le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x -le-mediant-zero-ℚ⁺ x = - le-right-mediant-ℚ - ( zero-ℚ) - ( rational-ℚ⁺ x) - ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x)) +abstract + le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x + le-mediant-zero-ℚ⁺ x = + le-right-mediant-ℚ + ( zero-ℚ) + ( rational-ℚ⁺ x) + ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x)) ``` ### Any positive rational number is the sum of two positive rational numbers diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index 99d4619055..53e20051b7 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -122,12 +122,13 @@ module _ (x y z : ℚ) where - transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z - transitive-le-ℚ = - transitive-le-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z) + abstract + transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z + transitive-le-ℚ = + transitive-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) ``` ### Concatenation rules for inequality and strict inequality on the rational numbers @@ -315,15 +316,16 @@ module _ ### Addition on the rational numbers preserves strict inequality ```agda -preserves-le-add-ℚ : - {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d) -preserves-le-add-ℚ {a} {b} {c} {d} H K = - transitive-le-ℚ - ( a +ℚ c) - ( b +ℚ c) - ( b +ℚ d) - ( preserves-le-right-add-ℚ b c d K) - ( preserves-le-left-add-ℚ c a b H) +abstract + preserves-le-add-ℚ : + {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d) + preserves-le-add-ℚ {a} {b} {c} {d} H K = + transitive-le-ℚ + ( a +ℚ c) + ( b +ℚ c) + ( b +ℚ d) + ( preserves-le-right-add-ℚ b c d K) + ( preserves-le-left-add-ℚ c a b H) ``` ### The rational numbers have no lower or upper bound diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md index 6023e6276d..7033d0b8db 100644 --- a/src/group-theory/abelian-groups.lagda.md +++ b/src/group-theory/abelian-groups.lagda.md @@ -612,17 +612,18 @@ module _ {l : Level} (A : Ab l) where - is-identity-left-conjugation-Ab : - (x : type-Ab A) → left-conjugation-Ab A x ~ id - is-identity-left-conjugation-Ab x y = - ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙ - ( is-retraction-right-subtraction-Ab A x y) - - is-identity-right-conjugation-Ab : - (x : type-Ab A) → right-conjugation-Ab A x ~ id - is-identity-right-conjugation-Ab x = - inv-htpy (left-right-conjugation-Ab A x) ∙h - is-identity-left-conjugation-Ab x + abstract + is-identity-left-conjugation-Ab : + (x : type-Ab A) → left-conjugation-Ab A x ~ id + is-identity-left-conjugation-Ab x y = + ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙ + ( is-retraction-right-subtraction-Ab A x y) + + is-identity-right-conjugation-Ab : + (x : type-Ab A) → right-conjugation-Ab A x ~ id + is-identity-right-conjugation-Ab x = + inv-htpy (left-right-conjugation-Ab A x) ∙h + is-identity-left-conjugation-Ab x is-identity-conjugation-Ab : (x : type-Ab A) → conjugation-Ab A x ~ id diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index c0aa126a41..573b1e9ec3 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -1,6 +1,8 @@ # Addition of lower Dedekind real numbers ```agda +{-# OPTIONS --lossy-unification #-} + module real-numbers.addition-lower-dedekind-real-numbers where ``` @@ -9,13 +11,27 @@ module real-numbers.addition-lower-dedekind-real-numbers where ```agda open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences open import foundation.subtypes +open import foundation.transport-along-identifications open import foundation.universe-levels +open import logic.functoriality-existential-quantification + +open import group-theory.abelian-groups +open import group-theory.groups open import group-theory.minkowski-multiplication-commutative-monoids open import real-numbers.lower-dedekind-real-numbers @@ -42,17 +58,111 @@ module _ ( cut-lower-ℝ x) ( cut-lower-ℝ y) - is-in-add-lower-ℝ-cut : ℚ → UU (l1 ⊔ l2) - is-in-add-lower-ℝ-cut = is-in-subtype cut-add-lower-ℝ + is-in-cut-add-lower-ℝ : ℚ → UU (l1 ⊔ l2) + is-in-cut-add-lower-ℝ = is-in-subtype cut-add-lower-ℝ is-inhabited-add-lower-ℝ : exists ℚ cut-add-lower-ℝ is-inhabited-add-lower-ℝ = minkowski-mul-inhabited-is-inhabited-Commutative-Monoid ( commutative-monoid-add-ℚ) - (cut-lower-ℝ x) - (cut-lower-ℝ y) - {! is-inhabited-cut-lower-ℝ x !} - {! !} + ( cut-lower-ℝ x) + ( cut-lower-ℝ y) + ( is-inhabited-cut-lower-ℝ x) + ( is-inhabited-cut-lower-ℝ y) + + abstract + is-rounded-cut-add-lower-ℝ : + (q : ℚ) → + is-in-cut-add-lower-ℝ q ↔ + exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r) + pr1 (is-rounded-cut-add-lower-ℝ q) = + elim-exists + ( ∃ ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r)) + ( λ (lx , ly) (lx Date: Sun, 9 Feb 2025 13:44:27 -0800 Subject: [PATCH 21/73] Fix naming --- .../addition-lower-dedekind-real-numbers.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 573b1e9ec3..6ec4f92d57 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -61,8 +61,8 @@ module _ is-in-cut-add-lower-ℝ : ℚ → UU (l1 ⊔ l2) is-in-cut-add-lower-ℝ = is-in-subtype cut-add-lower-ℝ - is-inhabited-add-lower-ℝ : exists ℚ cut-add-lower-ℝ - is-inhabited-add-lower-ℝ = + is-inhabited-cut-add-lower-ℝ : exists ℚ cut-add-lower-ℝ + is-inhabited-cut-add-lower-ℝ = minkowski-mul-inhabited-is-inhabited-Commutative-Monoid ( commutative-monoid-add-ℚ) ( cut-lower-ℝ x) @@ -161,7 +161,7 @@ module _ add-lower-ℝ : lower-ℝ (l1 ⊔ l2) pr1 add-lower-ℝ = cut-add-lower-ℝ - pr1 (pr2 add-lower-ℝ) = is-inhabited-add-lower-ℝ + pr1 (pr2 add-lower-ℝ) = is-inhabited-cut-add-lower-ℝ pr2 (pr2 add-lower-ℝ) = is-rounded-cut-add-lower-ℝ ``` From d7f6e2d518fec56f063419e9c8cefb022ce51c8a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:09:53 -0800 Subject: [PATCH 22/73] Similarity and containment --- ...ultiplication-commutative-monoids.lagda.md | 80 +++++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 66 +++++++++++++++ ...nkowski-multiplication-semigroups.lagda.md | 75 +++++++++++++++++ 3 files changed, 221 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 1e0ad307f4..8956fa2608 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -124,6 +124,86 @@ module _ minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M) ``` +### Containment is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (B : subset-Commutative-Monoid l2 M) + (A : subset-Commutative-Monoid l3 M) + (A' : subset-Commutative-Monoid l4 M) + where + + preserves-leq-left-minkowski-mul-Commutative-Monoid : + A ⊆ A' → + minkowski-mul-Commutative-Monoid M A B ⊆ + minkowski-mul-Commutative-Monoid M A' B + preserves-leq-left-minkowski-mul-Commutative-Monoid = + preserves-leq-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A' + + preserves-leq-right-minkowski-mul-Commutative-Monoid : + A ⊆ A' → + minkowski-mul-Commutative-Monoid M B A ⊆ + minkowski-mul-Commutative-Monoid M B A' + preserves-leq-right-minkowski-mul-Commutative-Monoid = + preserves-leq-right-minkowski-mul-Monoid + ( monoid-Commutative-Monoid M) + ( B) + ( A) + ( A') +``` + +### Similarity is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (B : subset-Commutative-Monoid l2 M) + (A : subset-Commutative-Monoid l3 M) + (A' : subset-Commutative-Monoid l4 M) + where + + preserves-sim-left-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M A' B) + preserves-sim-left-minkowski-mul-Commutative-Monoid = + preserves-sim-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A' + + preserves-sim-right-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M B A) + ( minkowski-mul-Commutative-Monoid M B A') + preserves-sim-right-minkowski-mul-Commutative-Monoid = + preserves-sim-right-minkowski-mul-Monoid + ( monoid-Commutative-Monoid M) + ( B) + ( A) + ( A') + +module _ + {l1 l2 l3 l4 l5 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + (A' : subset-Commutative-Monoid l3 M) + (B : subset-Commutative-Monoid l4 M) + (B' : subset-Commutative-Monoid l5 M) + where + + preserves-sim-minkowski-mul-Commutative-Monoid : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Commutative-Monoid M A B) + ( minkowski-mul-Commutative-Monoid M A' B') + preserves-sim-minkowski-mul-Commutative-Monoid = + preserves-sim-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A A' B B' +``` + ## See also - Minkowski multiplication on semigroups is defined in diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index b2e67b3464..a9302b06e3 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -148,10 +148,76 @@ module _ minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M) ``` +### Containment is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (B : subset-Monoid l2 M) + (A : subset-Monoid l3 M) + (A' : subset-Monoid l4 M) + where + + preserves-leq-left-minkowski-mul-Monoid : + A ⊆ A' → minkowski-mul-Monoid M A B ⊆ minkowski-mul-Monoid M A' B + preserves-leq-left-minkowski-mul-Monoid = + preserves-leq-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + + preserves-leq-right-minkowski-mul-Monoid : + A ⊆ A' → minkowski-mul-Monoid M B A ⊆ minkowski-mul-Monoid M B A' + preserves-leq-right-minkowski-mul-Monoid = + preserves-leq-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' +``` + +### Similarity is preserved by Minkowski multiplication of monoid subsets + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (B : subset-Monoid l2 M) + (A : subset-Monoid l3 M) + (A' : subset-Monoid l4 M) + where + + preserves-sim-left-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype (minkowski-mul-Monoid M A B) (minkowski-mul-Monoid M A' B) + preserves-sim-left-minkowski-mul-Monoid = + preserves-sim-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + + preserves-sim-right-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype (minkowski-mul-Monoid M B A) (minkowski-mul-Monoid M B A') + preserves-sim-right-minkowski-mul-Monoid = + preserves-sim-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A' + +module _ + {l1 l2 l3 l4 l5 : Level} + (M : Monoid l1) + (A : subset-Monoid l2 M) + (A' : subset-Monoid l3 M) + (B : subset-Monoid l4 M) + (B' : subset-Monoid l5 M) + where + + preserves-sim-minkowski-mul-Monoid : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Monoid M A B) + ( minkowski-mul-Monoid M A' B') + preserves-sim-minkowski-mul-Monoid = + preserves-sim-minkowski-mul-Semigroup (semigroup-Monoid M) A A' B B' +``` + ## See also - Minkowski multiplication on semigroups is defined in [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md). +- Minkowski multiplication on commutative monoids is defined in + [`group-theory.minkowski-multiplication-commutative-monoids`](group-theory.minkowski-multiplication-commutative-monoids.md). ## External links diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md index dae5ef51d5..8b233f4d0e 100644 --- a/src/group-theory/minkowski-multiplication-semigroups.lagda.md +++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md @@ -12,6 +12,8 @@ open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.powersets @@ -163,6 +165,79 @@ module _ λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl) ``` +### Containment is preserved by Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (B : subset-Semigroup l2 G) + (A : subset-Semigroup l3 G) + (A' : subset-Semigroup l4 G) + where + + preserves-leq-left-minkowski-mul-Semigroup : + A ⊆ A' → minkowski-mul-Semigroup G A B ⊆ minkowski-mul-Semigroup G A' B + preserves-leq-left-minkowski-mul-Semigroup A⊆A' x = + map-tot-exists (λ (a , b) → map-product (A⊆A' a) id) + + preserves-leq-right-minkowski-mul-Semigroup : + A ⊆ A' → minkowski-mul-Semigroup G B A ⊆ minkowski-mul-Semigroup G B A' + preserves-leq-right-minkowski-mul-Semigroup A⊆A' x = + map-tot-exists (λ (b , a) → map-product id (map-product (A⊆A' a) id)) +``` + +### Similarity is preserved by Minkowski multiplication of semigroup subtypes + +```agda +module _ + {l1 l2 l3 l4 : Level} + (G : Semigroup l1) + (B : subset-Semigroup l2 G) + (A : subset-Semigroup l3 G) + (A' : subset-Semigroup l4 G) + where + + preserves-sim-left-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype (minkowski-mul-Semigroup G A B) (minkowski-mul-Semigroup G A' B) + pr1 (preserves-sim-left-minkowski-mul-Semigroup (A⊆A' , _)) = + preserves-leq-left-minkowski-mul-Semigroup G B A A' A⊆A' + pr2 (preserves-sim-left-minkowski-mul-Semigroup (_ , A'⊆A)) = + preserves-leq-left-minkowski-mul-Semigroup G B A' A A'⊆A + + preserves-sim-right-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype (minkowski-mul-Semigroup G B A) (minkowski-mul-Semigroup G B A') + pr1 (preserves-sim-right-minkowski-mul-Semigroup (A⊆A' , _)) = + preserves-leq-right-minkowski-mul-Semigroup G B A A' A⊆A' + pr2 (preserves-sim-right-minkowski-mul-Semigroup (_ , A'⊆A)) = + preserves-leq-right-minkowski-mul-Semigroup G B A' A A'⊆A + +module _ + {l1 l2 l3 l4 l5 : Level} + (G : Semigroup l1) + (A : subset-Semigroup l2 G) + (A' : subset-Semigroup l3 G) + (B : subset-Semigroup l4 G) + (B' : subset-Semigroup l5 G) + where + + preserves-sim-minkowski-mul-Semigroup : + sim-subtype A A' → + sim-subtype B B' → + sim-subtype + ( minkowski-mul-Semigroup G A B) + ( minkowski-mul-Semigroup G A' B') + preserves-sim-minkowski-mul-Semigroup A≈A' B≈B' = + transitive-sim-subtype + ( minkowski-mul-Semigroup G A B) + ( minkowski-mul-Semigroup G A B') + ( minkowski-mul-Semigroup G A' B') + ( preserves-sim-left-minkowski-mul-Semigroup G B' A A' A≈A') + ( preserves-sim-right-minkowski-mul-Semigroup G A B B' B≈B') +``` + ## External links - [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at From fd4d1929dfe44d5f950237950629e2c22f37affe Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:22:00 -0800 Subject: [PATCH 23/73] Progress --- ...ition-lower-dedekind-real-numbers.lagda.md | 32 ++++++++++++++++--- 1 file changed, 27 insertions(+), 5 deletions(-) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 6ec4f92d57..40fcfc78da 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -159,10 +159,10 @@ module _ ( q)))) ( r Date: Sun, 9 Feb 2025 14:30:13 -0800 Subject: [PATCH 24/73] Propagate properties --- ...ultiplication-commutative-monoids.lagda.md | 69 +++++++++++++++++++ .../minkowski-multiplication-monoids.lagda.md | 18 +++++ 2 files changed, 87 insertions(+) diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md index 8956fa2608..ad3624e6ed 100644 --- a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md @@ -13,6 +13,7 @@ open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.powersets open import foundation.subtypes +open import foundation.unital-binary-operations open import foundation.universe-levels open import group-theory.commutative-monoids @@ -50,6 +51,74 @@ module _ ## Properties +### Minkowski multiplication of commutative monoid subsets is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + (B : subset-Commutative-Monoid l3 M) + (C : subset-Commutative-Monoid l4 M) + where + + associative-minkowski-mul-Commutative-Monoid : + minkowski-mul-Commutative-Monoid + ( M) + ( minkowski-mul-Commutative-Monoid M A B) + ( C) = + minkowski-mul-Commutative-Monoid + ( M) + ( A) + ( minkowski-mul-Commutative-Monoid M B C) + associative-minkowski-mul-Commutative-Monoid = + associative-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B C +``` + +### Minkowski multiplication of commutative monoid subsets is unital + +```agda +module _ + {l1 l2 : Level} + (M : Commutative-Monoid l1) + (A : subset-Commutative-Monoid l2 M) + where + + left-unit-law-minkowski-mul-Commutative-Monoid : + sim-subtype + ( minkowski-mul-Commutative-Monoid + ( M) + ( is-unit-prop-Commutative-Monoid M) + ( A)) + ( A) + left-unit-law-minkowski-mul-Commutative-Monoid = + left-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A + + right-unit-law-minkowski-mul-Commutative-Monoid : + sim-subtype + ( minkowski-mul-Commutative-Monoid + ( M) + ( A) + ( is-unit-prop-Commutative-Monoid M)) + ( A) + right-unit-law-minkowski-mul-Commutative-Monoid = + right-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A +``` + +### Minkowski multiplication on a commutative monoid is unital + +```agda +module _ + {l : Level} + (M : Commutative-Monoid l) + where + + is-unital-minkowski-mul-Commutative-Monoid : + is-unital (minkowski-mul-Commutative-Monoid {l} {l} {l} M) + is-unital-minkowski-mul-Commutative-Monoid = + is-unital-minkowski-mul-Monoid (monoid-Commutative-Monoid M) +``` + ### Minkowski multiplication on a commutative monoid is commutative ```agda diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md index a9302b06e3..b9f33264cf 100644 --- a/src/group-theory/minkowski-multiplication-monoids.lagda.md +++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md @@ -51,6 +51,24 @@ module _ ## Properties +### Minkowski multiplication of monoid subsets is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + (M : Monoid l1) + (A : subset-Monoid l2 M) + (B : subset-Monoid l3 M) + (C : subset-Monoid l4 M) + where + + associative-minkowski-mul-Monoid : + minkowski-mul-Monoid M (minkowski-mul-Monoid M A B) C = + minkowski-mul-Monoid M A (minkowski-mul-Monoid M B C) + associative-minkowski-mul-Monoid = + associative-minkowski-mul-Semigroup (semigroup-Monoid M) A B C +``` + ### Unit laws for Minkowski multiplication of monoid subsets ```agda From 1a5f82f4610bac227d74f89f2b4b638ba4b598fb Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:32:24 -0800 Subject: [PATCH 25/73] Addition on lower reals is associative and commutative --- .../addition-lower-dedekind-real-numbers.lagda.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 40fcfc78da..c45c75d99b 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -191,10 +191,16 @@ module _ module _ {l1 l2 l3 : Level} (x : lower-ℝ l1) (y : lower-ℝ l2) (z : lower-ℝ l3) where -{- + associative-add-lower-ℝ : add-lower-ℝ (add-lower-ℝ x y) z = add-lower-ℝ x (add-lower-ℝ y z) associative-add-lower-ℝ = eq-eq-cut-lower-ℝ - --(add-lower-ℝ (add-lower-ℝ -} + ( add-lower-ℝ (add-lower-ℝ x y) z) + ( add-lower-ℝ x (add-lower-ℝ y z)) + ( associative-minkowski-mul-Commutative-Monoid + ( commutative-monoid-add-ℚ) + ( cut-lower-ℝ x) + ( cut-lower-ℝ y) + ( cut-lower-ℝ z)) ``` From 6bfb61920a9444ea881df44ddd4b2824e9b038dc Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:33:30 -0800 Subject: [PATCH 26/73] Formatting --- src/real-numbers/lower-dedekind-real-numbers.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 6608478238..167a6805a5 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -22,6 +22,7 @@ open import foundation.universe-levels ``` + ## Idea A lower From fd8f3846dafbef038616b7b992081d60ec276300 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 14:44:51 -0800 Subject: [PATCH 27/73] Add new file --- ...ional-lower-dedekind-real-numbers.lagda.md | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..4c9fca0bf0 --- /dev/null +++ b/src/real-numbers/rational-lower-dedekind-real-numbers.lagda.md @@ -0,0 +1,59 @@ +# Rational lower Dedekind real numbers + +```agda +module real-numbers.rational-lower-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.universe-levels + +open import real-numbers.lower-dedekind-real-numbers +``` + +
+ +## Idea + +There is a canonical mapping from the [rational numbers](elementary-number-theory.rational-numbers.md) +to the [lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md). + +## Definition + +```agda +module _ (q : ℚ) where + cut-lower-real-ℚ : subtype lzero ℚ + cut-lower-real-ℚ p = le-ℚ-Prop p q + + is-in-cut-lower-real-ℚ : ℚ → UU lzero + is-in-cut-lower-real-ℚ p = le-ℚ p q + + is-inhabited-cut-lower-real-ℚ : exists ℚ cut-lower-real-ℚ + is-inhabited-cut-lower-real-ℚ = exists-lesser-ℚ q + + is-rounded-cut-lower-real-ℚ : + (p : ℚ) → + le-ℚ p q ↔ exists ℚ (λ r → le-ℚ-Prop p r ∧ le-ℚ-Prop r q) + pr1 (is-rounded-cut-lower-real-ℚ p) p Date: Sun, 9 Feb 2025 14:45:17 -0800 Subject: [PATCH 28/73] Fix line length --- src/real-numbers/lower-dedekind-real-numbers.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 167a6805a5..8d9097a7ec 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -95,7 +95,9 @@ module _ le-cut-lower-ℝ : le-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p le-cut-lower-ℝ p Date: Sun, 9 Feb 2025 14:49:24 -0800 Subject: [PATCH 29/73] Add rational upper reals --- ...ional-upper-dedekind-real-numbers.lagda.md | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..c6e1c589de --- /dev/null +++ b/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md @@ -0,0 +1,59 @@ +# Rational upper Dedekind real numbers + +```agda +module real-numbers.rational-upper-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.universe-levels + +open import real-numbers.upper-dedekind-real-numbers +``` + +
+ +## Idea + +There is a canonical mapping from the [rational numbers](elementary-number-theory.rational-numbers.md) +to the [upper Dedekind real numbers](real-numbers.upper-dedekind-real-numbers.md). + +## Definition + +```agda +module _ (q : ℚ) where + cut-upper-real-ℚ : subtype lzero ℚ + cut-upper-real-ℚ = le-ℚ-Prop q + + is-in-cut-upper-real-ℚ : ℚ → UU lzero + is-in-cut-upper-real-ℚ = le-ℚ q + + is-inhabited-cut-upper-real-ℚ : exists ℚ cut-upper-real-ℚ + is-inhabited-cut-upper-real-ℚ = exists-greater-ℚ q + + is-rounded-cut-upper-real-ℚ : + (p : ℚ) → + le-ℚ q p ↔ exists ℚ (λ r → le-ℚ-Prop r p ∧ le-ℚ-Prop q r) + pr1 (is-rounded-cut-upper-real-ℚ p) q

Date: Sun, 9 Feb 2025 15:00:35 -0800 Subject: [PATCH 30/73] Progress --- ...ality-lower-dedekind-real-numbers.lagda.md | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..4980bd1fdb --- /dev/null +++ b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md @@ -0,0 +1,56 @@ +# Inequality on the lower Dedekind real numbers + +```agda +module real-numbers.inequality-lower-dedekind-real-numbers where +``` + +

Imports + +```agda +open import elementary-number-theory.rational-numbers + +open import foundation.powersets +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.large-posets +open import order-theory.large-preorders + +open import real-numbers.lower-dedekind-real-numbers +``` + +
+ +## Idea + +The {{#concept "standard ordering" Disambiguation="lower Dedekind real numbers" Agda=leq-lower-ℝ}} on +the [lower real numbers](real-numbers.lower-dedekind-real-numbers.md) is defined as the +cut of one being a subset of the cut of the other. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (x : lower-ℝ l1) + (y : lower-ℝ l2) + where + + leq-lower-ℝ-Prop : Prop (l1 ⊔ l2) + leq-lower-ℝ-Prop = leq-prop-subtype (cut-lower-ℝ x) (cut-lower-ℝ y) +``` + +### Inequality on lower Dedekind reals is a large poset + +```agda +lower-ℝ-Large-Preorder : Large-Preorder lsuc _⊔_ +lower-ℝ-Large-Preorder = powerset-Large-Preorder ℚ + +lower-ℝ-Large-Poset : Large-Poset lsuc _⊔_ +lower-ℝ-Large-Poset = powerset-Large-Poset ℚ +``` + +## References + +{{#bibliography}} From fb18a45e9d71a0dc482e958b7bee3aba7dfd9750 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 15:09:04 -0800 Subject: [PATCH 31/73] Preservation of inequality --- ...ality-lower-dedekind-real-numbers.lagda.md | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md index 4980bd1fdb..52dd94fe52 100644 --- a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md @@ -7,8 +7,14 @@ module real-numbers.inequality-lower-dedekind-real-numbers where
Imports ```agda +open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.logical-equivalences open import foundation.powersets open import foundation.propositions open import foundation.subtypes @@ -18,6 +24,7 @@ open import order-theory.large-posets open import order-theory.large-preorders open import real-numbers.lower-dedekind-real-numbers +open import real-numbers.rational-lower-dedekind-real-numbers ```
@@ -39,8 +46,13 @@ module _ leq-lower-ℝ-Prop : Prop (l1 ⊔ l2) leq-lower-ℝ-Prop = leq-prop-subtype (cut-lower-ℝ x) (cut-lower-ℝ y) + + leq-lower-ℝ : UU (l1 ⊔ l2) + leq-lower-ℝ = type-Prop leq-lower-ℝ-Prop ``` +## Properties + ### Inequality on lower Dedekind reals is a large poset ```agda @@ -51,6 +63,25 @@ lower-ℝ-Large-Poset : Large-Poset lsuc _⊔_ lower-ℝ-Large-Poset = powerset-Large-Poset ℚ ``` +### The canonical map from the rational numbers to the lower reals preserves inequality + +```agda +preserves-leq-lower-real-ℚ : + (p q : ℚ) → leq-ℚ p q → leq-lower-ℝ (lower-real-ℚ p) (lower-real-ℚ q) +preserves-leq-lower-real-ℚ p q p≤q r r

Date: Sun, 9 Feb 2025 15:19:08 -0800 Subject: [PATCH 32/73] Define normal Dedekind reals in terms of lower and upper cuts --- .../dedekind-real-numbers.lagda.md | 57 ++++++++----------- 1 file changed, 25 insertions(+), 32 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 929862f718..0824ab205d 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -39,6 +39,9 @@ open import foundation.universe-levels open import foundation-core.truncation-levels open import logic.functoriality-existential-quantification + +open import real-numbers.lower-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers ``` @@ -48,19 +51,12 @@ open import logic.functoriality-existential-quantification A {{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} consists of a [pair](foundation.dependent-pair-types.md) `(L , U)` of -[subtypes](foundation-core.subtypes.md) of -[the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, -satisfying the following four conditions - -1. _Inhabitedness_. Both `L` and `U` are - [inhabited](foundation.inhabited-subtypes.md) subtypes of `ℚ`. -2. _Roundedness_. A rational number `q` is in `L` - [if and only if](foundation.logical-equivalences.md) there - [exists](foundation.existential-quantification.md) `q < r` such that `r ∈ L`, - and a rational number `r` is in `U` if and only if there exists `q < r` such - that `q ∈ U`. -3. _Disjointness_. `L` and `U` are disjoint subsets of `ℚ`. -4. _Locatedness_. If `q < r` then `q ∈ L` or `r ∈ U`. +a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers) +and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers) +that also satisfy the following conditions: + +1. _Disjointness_. `L` and `U` are disjoint subsets of `ℚ`. +2. _Locatedness_. If `q < r` then `q ∈ L` or `r ∈ U`. The type of {{#concept "Dedekind real numbers" Agda=ℝ}} is the type of all Dedekind cuts. The Dedekind real numbers will be taken as the standard @@ -77,15 +73,10 @@ module _ is-dedekind-cut-Prop : Prop (l1 ⊔ l2) is-dedekind-cut-Prop = - conjunction-Prop - ( (∃ ℚ L) ∧ (∃ ℚ U)) - ( conjunction-Prop - ( conjunction-Prop - ( ∀' ℚ ( λ q → L q ⇔ ∃ ℚ (λ r → le-ℚ-Prop q r ∧ L r))) - ( ∀' ℚ ( λ r → U r ⇔ ∃ ℚ (λ q → le-ℚ-Prop q r ∧ U q)))) - ( conjunction-Prop - ( ∀' ℚ (λ q → ¬' (L q ∧ U q))) - ( ∀' ℚ (λ q → ∀' ℚ (λ r → le-ℚ-Prop q r ⇒ (L q ∨ U r)))))) + is-lower-dedekind-cut-Prop L ∧ + is-upper-dedekind-cut-Prop U ∧ + ( ∀' ℚ (λ q → ¬' (L q ∧ U q))) ∧ + ( ∀' ℚ (λ q → ∀' ℚ (λ r → le-ℚ-Prop q r ⇒ (L q ∨ U r)))) is-dedekind-cut : UU (l1 ⊔ l2) is-dedekind-cut = type-Prop is-dedekind-cut-Prop @@ -113,6 +104,12 @@ module _ upper-cut-ℝ : subtype l ℚ upper-cut-ℝ = pr1 (pr2 x) + lower-real-ℝ : lower-ℝ l + lower-real-ℝ = lower-cut-ℝ , pr1 (pr2 (pr2 x)) + + upper-real-ℝ : upper-ℝ l + upper-real-ℝ = upper-cut-ℝ , pr1 (pr2 (pr2 (pr2 x))) + is-in-lower-cut-ℝ : ℚ → UU l is-in-lower-cut-ℝ = is-in-subtype lower-cut-ℝ @@ -123,34 +120,30 @@ module _ is-dedekind-cut-cut-ℝ = pr2 (pr2 x) is-inhabited-lower-cut-ℝ : exists ℚ lower-cut-ℝ - is-inhabited-lower-cut-ℝ = pr1 (pr1 is-dedekind-cut-cut-ℝ) + is-inhabited-lower-cut-ℝ = is-inhabited-cut-lower-ℝ lower-real-ℝ is-inhabited-upper-cut-ℝ : exists ℚ upper-cut-ℝ - is-inhabited-upper-cut-ℝ = pr2 (pr1 is-dedekind-cut-cut-ℝ) + is-inhabited-upper-cut-ℝ = is-inhabited-cut-upper-ℝ upper-real-ℝ is-rounded-lower-cut-ℝ : (q : ℚ) → is-in-lower-cut-ℝ q ↔ exists ℚ (λ r → (le-ℚ-Prop q r) ∧ (lower-cut-ℝ r)) - is-rounded-lower-cut-ℝ = - pr1 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) + is-rounded-lower-cut-ℝ = is-rounded-cut-lower-ℝ lower-real-ℝ is-rounded-upper-cut-ℝ : (r : ℚ) → is-in-upper-cut-ℝ r ↔ exists ℚ (λ q → (le-ℚ-Prop q r) ∧ (upper-cut-ℝ q)) - is-rounded-upper-cut-ℝ = - pr2 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) + is-rounded-upper-cut-ℝ = is-rounded-cut-upper-ℝ upper-real-ℝ is-disjoint-cut-ℝ : (q : ℚ) → ¬ (is-in-lower-cut-ℝ q × is-in-upper-cut-ℝ q) - is-disjoint-cut-ℝ = - pr1 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) + is-disjoint-cut-ℝ = pr1 (pr2 (pr2 (pr2 (pr2 x)))) is-located-lower-upper-cut-ℝ : (q r : ℚ) → le-ℚ q r → type-disjunction-Prop (lower-cut-ℝ q) (upper-cut-ℝ r) - is-located-lower-upper-cut-ℝ = - pr2 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) + is-located-lower-upper-cut-ℝ = pr2 (pr2 (pr2 (pr2 (pr2 x)))) cut-ℝ : subtype l ℚ cut-ℝ q = From 7499c7c9baad51f54cb31f7f4c52733a038fdc22 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 15:21:33 -0800 Subject: [PATCH 33/73] Start negation --- ...lower-upper-dedekind-real-numbers.lagda.md | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..485c61bb9c --- /dev/null +++ b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md @@ -0,0 +1,20 @@ +# Negation of lower and upper Dedekind real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.negation-lower-upper-dedekind-real-numbers where +``` + +

Imports + +```agda +open import foundation.universe-levels + +open import real-numbers.lower-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers +``` + +
+ +## Idea From 2185e189ba4af56d44a7c3d5da0861682d7271de Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 9 Feb 2025 15:26:36 -0800 Subject: [PATCH 34/73] Inequality on upper reals --- ...ality-upper-dedekind-real-numbers.lagda.md | 83 +++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..4e6802b471 --- /dev/null +++ b/src/real-numbers/inequality-upper-dedekind-real-numbers.lagda.md @@ -0,0 +1,83 @@ +# Inequality on the upper Dedekind real numbers + +```agda +module real-numbers.inequality-upper-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.logical-equivalences +open import foundation.powersets +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.large-posets +open import order-theory.large-preorders + +open import real-numbers.upper-dedekind-real-numbers +open import real-numbers.rational-upper-dedekind-real-numbers +``` + +
+ +## Idea + +The {{#concept "standard ordering" Disambiguation="upper Dedekind real numbers" Agda=leq-upper-ℝ}} on +the [upper real numbers](real-numbers.upper-dedekind-real-numbers.md) is defined as the +cut of the second being a subset of the cut of the first. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (x : upper-ℝ l1) + (y : upper-ℝ l2) + where + + leq-upper-ℝ-Prop : Prop (l1 ⊔ l2) + leq-upper-ℝ-Prop = leq-prop-subtype (cut-upper-ℝ y) (cut-upper-ℝ x) + + leq-upper-ℝ : UU (l1 ⊔ l2) + leq-upper-ℝ = type-Prop leq-upper-ℝ-Prop +``` + +## Properties + +### Inequality on upper Dedekind reals is a large poset + +```agda +upper-ℝ-Large-Preorder : Large-Preorder lsuc _⊔_ +upper-ℝ-Large-Preorder = powerset-Large-Preorder ℚ + +upper-ℝ-Large-Poset : Large-Poset lsuc _⊔_ +upper-ℝ-Large-Poset = powerset-Large-Poset ℚ +``` + +### The canonical map from the rational numbers to the upper reals preserves inequality + +```agda +preserves-leq-upper-real-ℚ : + (p q : ℚ) → leq-ℚ p q → leq-upper-ℝ (upper-real-ℚ p) (upper-real-ℚ q) +preserves-leq-upper-real-ℚ p q p≤q r = concatenate-leq-le-ℚ p q r p≤q + +reflects-leq-upper-real-ℚ : + (p q : ℚ) → leq-upper-ℝ (upper-real-ℚ p) (upper-real-ℚ q) → leq-ℚ p q +reflects-leq-upper-real-ℚ p q q Date: Mon, 10 Feb 2025 08:32:11 -0800 Subject: [PATCH 35/73] overhaul --- src/real-numbers.lagda.md | 5 + ...thmetically-located-dedekind-cuts.lagda.md | 76 +++---- .../dedekind-real-numbers.lagda.md | 33 ++- ...ality-lower-dedekind-real-numbers.lagda.md | 21 +- .../inequality-real-numbers.lagda.md | 31 +-- ...ality-upper-dedekind-real-numbers.lagda.md | 23 +- .../lower-dedekind-real-numbers.lagda.md | 3 + ...lower-upper-dedekind-real-numbers.lagda.md | 205 ++++++++++++++++++ .../negation-real-numbers.lagda.md | 88 ++------ ...ional-lower-dedekind-real-numbers.lagda.md | 5 +- .../rational-real-numbers.lagda.md | 31 +-- ...ional-upper-dedekind-real-numbers.lagda.md | 5 +- .../upper-dedekind-real-numbers.lagda.md | 3 + 13 files changed, 362 insertions(+), 167 deletions(-) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index b110b77299..1cd86ceaa3 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -7,11 +7,16 @@ module real-numbers where open import real-numbers.arithmetically-located-dedekind-cuts public open import real-numbers.dedekind-real-numbers public +open import real-numbers.inequality-lower-dedekind-real-numbers public open import real-numbers.inequality-real-numbers public +open import real-numbers.inequality-upper-dedekind-real-numbers public open import real-numbers.lower-dedekind-real-numbers public open import real-numbers.metric-space-of-real-numbers public +open import real-numbers.negation-lower-upper-dedekind-real-numbers public open import real-numbers.negation-real-numbers public +open import real-numbers.rational-lower-dedekind-real-numbers public open import real-numbers.rational-real-numbers public +open import real-numbers.rational-upper-dedekind-real-numbers public open import real-numbers.similarity-real-numbers public open import real-numbers.strict-inequality-real-numbers public open import real-numbers.upper-dedekind-real-numbers public diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index b33f8a86fc..31d707215b 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -17,6 +17,7 @@ open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers +open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types @@ -31,18 +32,23 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.abelian-groups + +open import real-numbers.lower-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers +open import real-numbers.dedekind-real-numbers ``` ## Definition -A [Dedekind cut](real-numbers.dedekind-real-numbers.md) `(L, U)` is -{{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for any -positive [rational number](elementary-number-theory.rational-numbers.md) +A pair of a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) +`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U` +is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for +any positive [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ`, there exist `p, q : ℚ` such that `0 < q - p < ε`, `p ∈ L`, and `q ∈ U`. -Intuitively, when `L , U` represent the Dedekind cuts of a real number `x`, `p` -and `q` are rational approximations of `x` to within `ε`. This follows parts of +Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` +are rational approximations of `x` to within `ε`. This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ## Definitions @@ -51,16 +57,17 @@ Section 11 in {{#cite BauerTaylor2009}}. ```agda module _ - {l : Level} (L : subtype l ℚ) (U : subtype l ℚ) + {l : Level} (L : lower-ℝ l) (U : upper-ℝ l) where - is-arithmetically-located-pair-of-subtypes-ℚ : UU l - is-arithmetically-located-pair-of-subtypes-ℚ = - (ε : ℚ) → - is-positive-ℚ ε → + is-arithmetically-located-pair-of-cuts-ℚ : UU l + is-arithmetically-located-pair-of-cuts-ℚ = + (ε⁺ : ℚ⁺) → exists ( ℚ × ℚ) - ( λ (p , q) → le-ℚ-Prop p q ∧ le-ℚ-Prop q (p +ℚ ε) ∧ L p ∧ U q) + ( λ (p , q) → le-ℚ-Prop q (p +ℚ rational-ℚ⁺ ε⁺) ∧ + cut-lower-ℝ L p ∧ + cut-upper-ℝ U q) ``` ## Properties @@ -72,50 +79,37 @@ rational numbers, it is also located. ```agda module _ - {l : Level} (L : subtype l ℚ) (U : subtype l ℚ) + {l : Level} (L : lower-ℝ l) (U : upper-ℝ l) where abstract - is-located-is-arithmetically-located-pair-of-subtypes-ℚ : - is-arithmetically-located-pair-of-subtypes-ℚ L U → - ((p q : ℚ) → le-ℚ p q → is-in-subtype L q → is-in-subtype L p) → - ((p q : ℚ) → le-ℚ p q → is-in-subtype U p → is-in-subtype U q) → - (p q : ℚ) → le-ℚ p q → type-disjunction-Prop (L p) (U q) - is-located-is-arithmetically-located-pair-of-subtypes-ℚ - arithmetically-located lower-closed upper-closed p q p ## Idea -The {{#concept "standard ordering" Disambiguation="upper Dedekind real numbers" Agda=leq-upper-ℝ}} on -the [upper real numbers](real-numbers.upper-dedekind-real-numbers.md) is defined as the -cut of the second being a subset of the cut of the first. +The +{{#concept "standard ordering" Disambiguation="upper Dedekind real numbers" Agda=leq-upper-ℝ}} +on the [upper real numbers](real-numbers.upper-dedekind-real-numbers.md) is +defined as the cut of the second being a subset of the cut of the first. ## Definition @@ -57,10 +58,20 @@ module _ ```agda upper-ℝ-Large-Preorder : Large-Preorder lsuc _⊔_ -upper-ℝ-Large-Preorder = powerset-Large-Preorder ℚ +type-Large-Preorder upper-ℝ-Large-Preorder = upper-ℝ +leq-prop-Large-Preorder upper-ℝ-Large-Preorder = leq-upper-ℝ-Prop +refl-leq-Large-Preorder upper-ℝ-Large-Preorder x = + refl-leq-subtype (cut-upper-ℝ x) +transitive-leq-Large-Preorder upper-ℝ-Large-Preorder x y z y≤z x≤y = + transitive-leq-subtype (cut-upper-ℝ z) (cut-upper-ℝ y) (cut-upper-ℝ x) x≤y y≤z upper-ℝ-Large-Poset : Large-Poset lsuc _⊔_ -upper-ℝ-Large-Poset = powerset-Large-Poset ℚ +large-preorder-Large-Poset upper-ℝ-Large-Poset = upper-ℝ-Large-Preorder +antisymmetric-leq-Large-Poset upper-ℝ-Large-Poset x y x≤y y≤x = + eq-eq-cut-upper-ℝ + ( x) + ( y) + ( antisymmetric-leq-subtype (cut-upper-ℝ x) (cut-upper-ℝ y) y≤x x≤y) ``` ### The canonical map from the rational numbers to the upper reals preserves inequality diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 8d9097a7ec..6bc94cd66d 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -75,6 +75,9 @@ module _ is-in-cut-lower-ℝ : ℚ → UU l is-in-cut-lower-ℝ = is-in-subtype cut-lower-ℝ + is-lower-dedekind-cut-lower-ℝ : is-lower-dedekind-cut cut-lower-ℝ + is-lower-dedekind-cut-lower-ℝ = pr2 x + is-inhabited-cut-lower-ℝ : exists ℚ cut-lower-ℝ is-inhabited-cut-lower-ℝ = pr1 (pr2 x) diff --git a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md index 485c61bb9c..3f6366d7ac 100644 --- a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md @@ -9,12 +9,217 @@ module real-numbers.negation-lower-upper-dedekind-real-numbers where
Imports ```agda +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.powersets +open import foundation.retractions +open import foundation.sections +open import foundation.subtypes +open import foundation.transport-along-identifications open import foundation.universe-levels +open import logic.functoriality-existential-quantification + open import real-numbers.lower-dedekind-real-numbers open import real-numbers.upper-dedekind-real-numbers +open import real-numbers.rational-lower-dedekind-real-numbers +open import real-numbers.rational-upper-dedekind-real-numbers ```
## Idea + +The negation of a lower Dedekind real is an upper Dedekind real containing +the negations of elements in the lower cut, and vice versa. + +## Definition + +### The negation of a lower Dedekind real, as an upper Dedekind real + +```agda +module _ + {l : Level} (x : lower-ℝ l) + where + + cut-neg-lower-ℝ : subtype l ℚ + cut-neg-lower-ℝ p = cut-lower-ℝ x (neg-ℚ p) + + is-in-cut-neg-lower-ℝ : ℚ → UU l + is-in-cut-neg-lower-ℝ = is-in-subtype cut-neg-lower-ℝ + + abstract + is-inhabited-cut-neg-lower-ℝ : exists ℚ cut-neg-lower-ℝ + is-inhabited-cut-neg-lower-ℝ = + map-exists + ( is-in-cut-neg-lower-ℝ) + ( neg-ℚ) + ( λ p → tr (is-in-cut-lower-ℝ x) (inv (neg-neg-ℚ p))) + ( is-inhabited-cut-lower-ℝ x) + + is-rounded-cut-neg-lower-ℝ : + (q : ℚ) → + is-in-cut-neg-lower-ℝ q ↔ + exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-neg-lower-ℝ p) + pr1 (is-rounded-cut-neg-lower-ℝ q) -q @@ -50,72 +55,17 @@ module _ {l : Level} (x : ℝ l) where + lower-real-neg-ℝ : lower-ℝ l + lower-real-neg-ℝ = neg-upper-ℝ (upper-real-ℝ x) + + upper-real-neg-ℝ : upper-ℝ l + upper-real-neg-ℝ = neg-lower-ℝ (lower-real-ℝ x) + lower-cut-neg-ℝ : subtype l ℚ - lower-cut-neg-ℝ q = upper-cut-ℝ x (neg-ℚ q) + lower-cut-neg-ℝ = cut-lower-ℝ lower-real-neg-ℝ upper-cut-neg-ℝ : subtype l ℚ - upper-cut-neg-ℝ q = lower-cut-ℝ x (neg-ℚ q) - - is-inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ - is-inhabited-lower-cut-neg-ℝ = - map-exists - ( is-in-subtype lower-cut-neg-ℝ) - ( neg-ℚ) - ( λ q → tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ q))) - ( is-inhabited-upper-cut-ℝ x) - - is-inhabited-upper-cut-neg-ℝ : exists ℚ upper-cut-neg-ℝ - is-inhabited-upper-cut-neg-ℝ = - map-exists - ( is-in-subtype upper-cut-neg-ℝ) - ( neg-ℚ) - ( λ q → tr (is-in-lower-cut-ℝ x) (inv (neg-neg-ℚ q))) - ( is-inhabited-lower-cut-ℝ x) - - is-rounded-lower-cut-neg-ℝ : - (q : ℚ) → - is-in-subtype lower-cut-neg-ℝ q ↔ - exists ℚ (λ r → (le-ℚ-Prop q r) ∧ (lower-cut-neg-ℝ r)) - pr1 (is-rounded-lower-cut-neg-ℝ q) in-neg-lower = - map-exists - ( λ r → le-ℚ q r × is-in-subtype lower-cut-neg-ℝ r) - ( neg-ℚ) - ( λ r (r<-q , in-upper-r) → - ( ( tr - ( λ x → le-ℚ x (neg-ℚ r)) - ( neg-neg-ℚ q) - ( neg-le-ℚ r (neg-ℚ q) r<-q)) , - ( tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ r)) in-upper-r))) - ( forward-implication (is-rounded-upper-cut-ℝ x (neg-ℚ q)) in-neg-lower) - pr2 (is-rounded-lower-cut-neg-ℝ q) exists-r = - backward-implication - ( is-rounded-upper-cut-ℝ x (neg-ℚ q)) - ( map-exists - ( λ r → le-ℚ r (neg-ℚ q) × is-in-upper-cut-ℝ x r) - ( neg-ℚ) - ( λ r (q @@ -56,28 +60,13 @@ the [image](foundation.images.md) of this embedding is-dedekind-cut-le-ℚ : (x : ℚ) → is-dedekind-cut - (λ (q : ℚ) → le-ℚ-Prop q x) - (λ (r : ℚ) → le-ℚ-Prop x r) + (cut-lower-real-ℚ x) + (cut-upper-real-ℚ x) is-dedekind-cut-le-ℚ x = - ( exists-lesser-ℚ x , exists-greater-ℚ x) , - ( ( λ (q : ℚ) → - dense-le-ℚ q x , - elim-exists - ( le-ℚ-Prop q x) - ( λ r (H , H') → transitive-le-ℚ q r x H' H)) , - ( λ (r : ℚ) → - α x r ∘ dense-le-ℚ x r , - elim-exists - ( le-ℚ-Prop x r) - ( λ q (H , H') → transitive-le-ℚ x q r H H'))) , - ( λ (q : ℚ) (H , H') → asymmetric-le-ℚ q x H H') , - ( located-le-ℚ x) - where - α : - (a b : ℚ) → - exists ℚ (λ r → le-ℚ-Prop a r ∧ le-ℚ-Prop r b) → - exists ℚ (λ r → le-ℚ-Prop r b ∧ le-ℚ-Prop a r) - α a b = map-tot-exists (λ r (p , q) → (q , p)) + is-lower-dedekind-cut-lower-ℝ (lower-real-ℚ x) , + is-upper-dedekind-cut-upper-ℝ (upper-real-ℚ x) , + (λ q (H , K) → asymmetric-le-ℚ q x H K) , + located-le-ℚ x ``` ### The canonical map from `ℚ` to `ℝ` diff --git a/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md index c6e1c589de..9761287d50 100644 --- a/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/rational-upper-dedekind-real-numbers.lagda.md @@ -24,8 +24,9 @@ open import real-numbers.upper-dedekind-real-numbers ## Idea -There is a canonical mapping from the [rational numbers](elementary-number-theory.rational-numbers.md) -to the [upper Dedekind real numbers](real-numbers.upper-dedekind-real-numbers.md). +There is a canonical mapping from the +[rational numbers](elementary-number-theory.rational-numbers.md) to the +[upper Dedekind real numbers](real-numbers.upper-dedekind-real-numbers.md). ## Definition diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md index c9dbf0f8f4..264bf07633 100644 --- a/src/real-numbers/upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md @@ -75,6 +75,9 @@ module _ is-in-cut-upper-ℝ : ℚ → UU l is-in-cut-upper-ℝ = is-in-subtype cut-upper-ℝ + is-upper-dedekind-cut-upper-ℝ : is-upper-dedekind-cut cut-upper-ℝ + is-upper-dedekind-cut-upper-ℝ = pr2 x + is-inhabited-cut-upper-ℝ : exists ℚ cut-upper-ℝ is-inhabited-cut-upper-ℝ = pr1 (pr2 x) From 70f181c77d39b461ed5a3b79376f9f685fb70508 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 08:58:26 -0800 Subject: [PATCH 36/73] make pre-commit --- .../arithmetically-located-dedekind-cuts.lagda.md | 6 +++--- src/real-numbers/inequality-real-numbers.lagda.md | 6 +++--- ...egation-lower-upper-dedekind-real-numbers.lagda.md | 11 ++++++----- src/real-numbers/negation-real-numbers.lagda.md | 4 ++-- src/real-numbers/rational-real-numbers.lagda.md | 2 +- 5 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 31d707215b..06174ce77c 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -33,9 +33,9 @@ open import foundation.universe-levels open import group-theory.abelian-groups +open import real-numbers.dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.upper-dedekind-real-numbers -open import real-numbers.dedekind-real-numbers ``` @@ -48,8 +48,8 @@ is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for any positive [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ`, there exist `p, q : ℚ` such that `0 < q - p < ε`, `p ∈ L`, and `q ∈ U`. Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` -are rational approximations of `x` to within `ε`. This follows parts of -Section 11 in {{#cite BauerTaylor2009}}. +are rational approximations of `x` to within `ε`. This follows parts of Section +11 in {{#cite BauerTaylor2009}}. ## Definitions diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md index 83978ab7da..579ef75be4 100644 --- a/src/real-numbers/inequality-real-numbers.lagda.md +++ b/src/real-numbers/inequality-real-numbers.lagda.md @@ -27,14 +27,14 @@ open import order-theory.large-preorders open import order-theory.posets open import order-theory.preorders +open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-lower-dedekind-real-numbers open import real-numbers.inequality-upper-dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers -open import real-numbers.upper-dedekind-real-numbers -open import real-numbers.negation-real-numbers open import real-numbers.negation-lower-upper-dedekind-real-numbers -open import real-numbers.dedekind-real-numbers +open import real-numbers.negation-real-numbers open import real-numbers.rational-real-numbers +open import real-numbers.upper-dedekind-real-numbers ``` diff --git a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md index 3f6366d7ac..25081b1abe 100644 --- a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md @@ -29,17 +29,17 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification open import real-numbers.lower-dedekind-real-numbers -open import real-numbers.upper-dedekind-real-numbers open import real-numbers.rational-lower-dedekind-real-numbers open import real-numbers.rational-upper-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers ``` ## Idea -The negation of a lower Dedekind real is an upper Dedekind real containing -the negations of elements in the lower cut, and vice versa. +The negation of a lower Dedekind real is an upper Dedekind real containing the +negations of elements in the lower cut, and vice versa. ## Definition @@ -126,7 +126,7 @@ module _ ( λ x → le-ℚ x (neg-ℚ p)) ( neg-neg-ℚ q) ( neg-le-ℚ p (neg-ℚ q) p<-q) , - tr (is-in-cut-upper-ℝ x) (inv (neg-neg-ℚ p)) x

diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index d3829df34b..69ec475e2a 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -37,9 +37,9 @@ open import logic.functoriality-existential-quantification open import real-numbers.dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers -open import real-numbers.upper-dedekind-real-numbers open import real-numbers.rational-lower-dedekind-real-numbers open import real-numbers.rational-upper-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers ``` From 926877950f77ce8f137452df3e56bbc22ad573bc Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 09:08:37 -0800 Subject: [PATCH 37/73] a -> an --- src/real-numbers/upper-dedekind-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md index 264bf07633..01625b8046 100644 --- a/src/real-numbers/upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md @@ -25,7 +25,7 @@ open import foundation.universe-levels ## Idea -A upper +An upper {{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} consists of a [subtype](foundation-core.subtypes.md) `U` of [the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, From 1b9d81b2b52a68c6093186f8b12facffc089ed53 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 09:10:52 -0800 Subject: [PATCH 38/73] Rename some things --- src/real-numbers/inequality-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md index 579ef75be4..098feec9e9 100644 --- a/src/real-numbers/inequality-real-numbers.lagda.md +++ b/src/real-numbers/inequality-real-numbers.lagda.md @@ -62,7 +62,7 @@ module _ ## Properties -### Equivalence with reversed containment of upper cuts +### Equivalence with inequality on upper cuts ```agda module _ From f75209b769526ce9b5c6f17f50b75c823ba3481f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 17:08:28 -0800 Subject: [PATCH 39/73] Some more theorems --- ...uality-lower-dedekind-real-numbers.lagda.md | 18 ++++++++++++++++++ ...uality-upper-dedekind-real-numbers.lagda.md | 18 ++++++++++++++++++ ...-lower-upper-dedekind-real-numbers.lagda.md | 2 ++ 3 files changed, 38 insertions(+) diff --git a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md index 9cd1a90e4c..7a0a1d476b 100644 --- a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md @@ -14,7 +14,9 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types +open import foundation.existential-quantification open import foundation.logical-equivalences +open import foundation.negation open import foundation.powersets open import foundation.propositions open import foundation.subtypes @@ -74,6 +76,22 @@ antisymmetric-leq-Large-Poset lower-ℝ-Large-Poset x y x≤y y≤x = ( antisymmetric-leq-subtype (cut-lower-ℝ x) (cut-lower-ℝ y) x≤y y≤x) ``` +### If a rational is in a lower Dedekind cut, its projections is less than or equal to the corresponding lower real + +```agda +module _ + {l : Level} + (x : lower-ℝ l) + (q : ℚ) + where + + leq-is-in-cut-lower-real-ℚ : is-in-cut-lower-ℝ x q → leq-lower-ℝ (lower-real-ℚ q) x + leq-is-in-cut-lower-real-ℚ q∈L p p From 098d4e88a48b3e1b87da820e5af988c4adc43399 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 17:20:47 -0800 Subject: [PATCH 40/73] Finish gaps --- .../inequality-rational-numbers.lagda.md | 256 +++++++++--------- .../rational-numbers.lagda.md | 17 +- ...thmetically-located-dedekind-cuts.lagda.md | 5 +- ...ality-lower-dedekind-real-numbers.lagda.md | 3 +- ...ality-upper-dedekind-real-numbers.lagda.md | 4 +- ...lower-upper-dedekind-real-numbers.lagda.md | 4 +- 6 files changed, 152 insertions(+), 137 deletions(-) diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index a945128fad..12ddd6f34a 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -103,33 +103,35 @@ refl-leq-ℚ x = ### Inequality on the rational numbers is antisymmetric ```agda -antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x = y -antisymmetric-leq-ℚ x y H H' = - ( inv (is-retraction-rational-fraction-ℚ x)) ∙ - ( eq-ℚ-sim-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( is-sim-antisymmetric-leq-fraction-ℤ +abstract + antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x = y + antisymmetric-leq-ℚ x y H H' = + ( inv (is-retraction-rational-fraction-ℚ x)) ∙ + ( eq-ℚ-sim-fraction-ℤ ( fraction-ℚ x) ( fraction-ℚ y) - ( H) - ( H'))) ∙ - ( is-retraction-rational-fraction-ℚ y) + ( is-sim-antisymmetric-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( H) + ( H'))) ∙ + ( is-retraction-rational-fraction-ℚ y) ``` ### Inequality on the rational numbers is linear ```agda -linear-leq-ℚ : (x y : ℚ) → (leq-ℚ x y) + (leq-ℚ y x) -linear-leq-ℚ x y = - map-coproduct - ( id) - ( is-nonnegative-eq-ℤ - (distributive-neg-diff-ℤ - ( numerator-ℚ y *ℤ denominator-ℚ x) - ( numerator-ℚ x *ℤ denominator-ℚ y))) - ( decide-is-nonnegative-is-nonnegative-neg-ℤ - { cross-mul-diff-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)}) +abstract + linear-leq-ℚ : (x y : ℚ) → (leq-ℚ x y) + (leq-ℚ y x) + linear-leq-ℚ x y = + map-coproduct + ( id) + ( is-nonnegative-eq-ℤ + (distributive-neg-diff-ℤ + ( numerator-ℚ y *ℤ denominator-ℚ x) + ( numerator-ℚ x *ℤ denominator-ℚ y))) + ( decide-is-nonnegative-is-nonnegative-neg-ℤ + { cross-mul-diff-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)}) ``` ### Inequality on the rational numbers is transitive @@ -139,12 +141,13 @@ module _ (x y z : ℚ) where - transitive-leq-ℚ : leq-ℚ y z → leq-ℚ x y → leq-ℚ x z - transitive-leq-ℚ = - transitive-leq-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z) + abstract + transitive-leq-ℚ : leq-ℚ y z → leq-ℚ x y → leq-ℚ x z + transitive-leq-ℚ = + transitive-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) ``` ### The partially ordered set of rational numbers ordered by inequality @@ -165,43 +168,45 @@ module _ (p q : fraction-ℤ) where - preserves-leq-rational-fraction-ℤ : - leq-fraction-ℤ p q → leq-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q) - preserves-leq-rational-fraction-ℤ = - preserves-leq-sim-fraction-ℤ - ( p) - ( q) - ( reduce-fraction-ℤ p) - ( reduce-fraction-ℤ q) - ( sim-reduced-fraction-ℤ p) - ( sim-reduced-fraction-ℤ q) + abstract + preserves-leq-rational-fraction-ℤ : + leq-fraction-ℤ p q → leq-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q) + preserves-leq-rational-fraction-ℤ = + preserves-leq-sim-fraction-ℤ + ( p) + ( q) + ( reduce-fraction-ℤ p) + ( reduce-fraction-ℤ q) + ( sim-reduced-fraction-ℤ p) + ( sim-reduced-fraction-ℤ q) module _ (x : ℚ) (p : fraction-ℤ) where - preserves-leq-right-rational-fraction-ℤ : - leq-fraction-ℤ (fraction-ℚ x) p → leq-ℚ x (rational-fraction-ℤ p) - preserves-leq-right-rational-fraction-ℤ H = - concatenate-leq-sim-fraction-ℤ - ( fraction-ℚ x) - ( p) - ( fraction-ℚ ( rational-fraction-ℤ p)) - ( H) - ( sim-reduced-fraction-ℤ p) - - reflects-leq-right-rational-fraction-ℤ : - leq-ℚ x (rational-fraction-ℤ p) → leq-fraction-ℤ (fraction-ℚ x) p - reflects-leq-right-rational-fraction-ℤ H = - concatenate-leq-sim-fraction-ℤ - ( fraction-ℚ x) - ( reduce-fraction-ℤ p) - ( p) - ( H) - ( symmetric-sim-fraction-ℤ + abstract + preserves-leq-right-rational-fraction-ℤ : + leq-fraction-ℤ (fraction-ℚ x) p → leq-ℚ x (rational-fraction-ℤ p) + preserves-leq-right-rational-fraction-ℤ H = + concatenate-leq-sim-fraction-ℤ + ( fraction-ℚ x) ( p) + ( fraction-ℚ ( rational-fraction-ℤ p)) + ( H) + ( sim-reduced-fraction-ℤ p) + + reflects-leq-right-rational-fraction-ℤ : + leq-ℚ x (rational-fraction-ℤ p) → leq-fraction-ℤ (fraction-ℚ x) p + reflects-leq-right-rational-fraction-ℤ H = + concatenate-leq-sim-fraction-ℤ + ( fraction-ℚ x) ( reduce-fraction-ℤ p) - ( sim-reduced-fraction-ℤ p)) + ( p) + ( H) + ( symmetric-sim-fraction-ℤ + ( p) + ( reduce-fraction-ℤ p) + ( sim-reduced-fraction-ℤ p)) iff-leq-right-rational-fraction-ℤ : leq-fraction-ℤ (fraction-ℚ x) p ↔ leq-ℚ x (rational-fraction-ℤ p) @@ -209,26 +214,27 @@ module _ preserves-leq-right-rational-fraction-ℤ pr2 iff-leq-right-rational-fraction-ℤ = reflects-leq-right-rational-fraction-ℤ - preserves-leq-left-rational-fraction-ℤ : - leq-fraction-ℤ p (fraction-ℚ x) → leq-ℚ (rational-fraction-ℤ p) x - preserves-leq-left-rational-fraction-ℤ = - concatenate-sim-leq-fraction-ℤ - ( fraction-ℚ ( rational-fraction-ℤ p)) - ( p) - ( fraction-ℚ x) - ( symmetric-sim-fraction-ℤ - ( p) + abstract + preserves-leq-left-rational-fraction-ℤ : + leq-fraction-ℤ p (fraction-ℚ x) → leq-ℚ (rational-fraction-ℤ p) x + preserves-leq-left-rational-fraction-ℤ = + concatenate-sim-leq-fraction-ℤ ( fraction-ℚ ( rational-fraction-ℤ p)) - ( sim-reduced-fraction-ℤ p)) - - reflects-leq-left-rational-fraction-ℤ : - leq-ℚ (rational-fraction-ℤ p) x → leq-fraction-ℤ p (fraction-ℚ x) - reflects-leq-left-rational-fraction-ℤ = - concatenate-sim-leq-fraction-ℤ - ( p) - ( reduce-fraction-ℤ p) - ( fraction-ℚ x) - ( sim-reduced-fraction-ℤ p) + ( p) + ( fraction-ℚ x) + ( symmetric-sim-fraction-ℤ + ( p) + ( fraction-ℚ ( rational-fraction-ℤ p)) + ( sim-reduced-fraction-ℤ p)) + + reflects-leq-left-rational-fraction-ℤ : + leq-ℚ (rational-fraction-ℤ p) x → leq-fraction-ℤ p (fraction-ℚ x) + reflects-leq-left-rational-fraction-ℤ = + concatenate-sim-leq-fraction-ℤ + ( p) + ( reduce-fraction-ℤ p) + ( fraction-ℚ x) + ( sim-reduced-fraction-ℤ p) iff-leq-left-rational-fraction-ℤ : leq-fraction-ℤ p (fraction-ℚ x) ↔ leq-ℚ (rational-fraction-ℤ p) x @@ -243,26 +249,29 @@ module _ (x y : ℚ) where - iff-translate-diff-leq-zero-ℚ : leq-ℚ zero-ℚ (y -ℚ x) ↔ leq-ℚ x y - iff-translate-diff-leq-zero-ℚ = - logical-equivalence-reasoning - leq-ℚ zero-ℚ (y -ℚ x) - ↔ leq-fraction-ℤ - ( zero-fraction-ℤ) - ( add-fraction-ℤ (fraction-ℚ y) (neg-fraction-ℤ (fraction-ℚ x))) - by - inv-iff - ( iff-leq-right-rational-fraction-ℤ - ( zero-ℚ) - ( add-fraction-ℤ (fraction-ℚ y) (neg-fraction-ℤ (fraction-ℚ x)))) - ↔ leq-ℚ x y - by - inv-tr - ( _↔ leq-ℚ x y) - ( eq-translate-diff-leq-zero-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y)) - ( id-iff) + abstract + iff-translate-diff-leq-zero-ℚ : leq-ℚ zero-ℚ (y -ℚ x) ↔ leq-ℚ x y + iff-translate-diff-leq-zero-ℚ = + logical-equivalence-reasoning + leq-ℚ zero-ℚ (y -ℚ x) + ↔ leq-fraction-ℤ + ( zero-fraction-ℤ) + ( add-fraction-ℤ (fraction-ℚ y) (neg-fraction-ℤ (fraction-ℚ x))) + by + inv-iff + ( iff-leq-right-rational-fraction-ℤ + ( zero-ℚ) + ( add-fraction-ℤ + ( fraction-ℚ y) + ( neg-fraction-ℤ (fraction-ℚ x)))) + ↔ leq-ℚ x y + by + inv-tr + ( _↔ leq-ℚ x y) + ( eq-translate-diff-leq-zero-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y)) + ( id-iff) ``` ### Inequality on the rational numbers is invariant by translation @@ -272,34 +281,35 @@ module _ (z x y : ℚ) where - iff-translate-left-leq-ℚ : leq-ℚ (z +ℚ x) (z +ℚ y) ↔ leq-ℚ x y - iff-translate-left-leq-ℚ = - logical-equivalence-reasoning - leq-ℚ (z +ℚ x) (z +ℚ y) - ↔ leq-ℚ zero-ℚ ((z +ℚ y) -ℚ (z +ℚ x)) - by (inv-iff (iff-translate-diff-leq-zero-ℚ (z +ℚ x) (z +ℚ y))) - ↔ leq-ℚ zero-ℚ (y -ℚ x) - by - ( inv-tr - ( _↔ leq-ℚ zero-ℚ (y -ℚ x)) - ( ap (leq-ℚ zero-ℚ) (left-translation-diff-ℚ y x z)) - ( id-iff)) - ↔ leq-ℚ x y - by (iff-translate-diff-leq-zero-ℚ x y) - - iff-translate-right-leq-ℚ : leq-ℚ (x +ℚ z) (y +ℚ z) ↔ leq-ℚ x y - iff-translate-right-leq-ℚ = - logical-equivalence-reasoning - leq-ℚ (x +ℚ z) (y +ℚ z) - ↔ leq-ℚ zero-ℚ ((y +ℚ z) -ℚ (x +ℚ z)) - by (inv-iff (iff-translate-diff-leq-zero-ℚ (x +ℚ z) (y +ℚ z))) - ↔ leq-ℚ zero-ℚ (y -ℚ x) - by - ( inv-tr - ( _↔ leq-ℚ zero-ℚ (y -ℚ x)) - ( ap (leq-ℚ zero-ℚ) (right-translation-diff-ℚ y x z)) - ( id-iff)) - ↔ leq-ℚ x y by (iff-translate-diff-leq-zero-ℚ x y) + abstract + iff-translate-left-leq-ℚ : leq-ℚ (z +ℚ x) (z +ℚ y) ↔ leq-ℚ x y + iff-translate-left-leq-ℚ = + logical-equivalence-reasoning + leq-ℚ (z +ℚ x) (z +ℚ y) + ↔ leq-ℚ zero-ℚ ((z +ℚ y) -ℚ (z +ℚ x)) + by (inv-iff (iff-translate-diff-leq-zero-ℚ (z +ℚ x) (z +ℚ y))) + ↔ leq-ℚ zero-ℚ (y -ℚ x) + by + ( inv-tr + ( _↔ leq-ℚ zero-ℚ (y -ℚ x)) + ( ap (leq-ℚ zero-ℚ) (left-translation-diff-ℚ y x z)) + ( id-iff)) + ↔ leq-ℚ x y + by (iff-translate-diff-leq-zero-ℚ x y) + + iff-translate-right-leq-ℚ : leq-ℚ (x +ℚ z) (y +ℚ z) ↔ leq-ℚ x y + iff-translate-right-leq-ℚ = + logical-equivalence-reasoning + leq-ℚ (x +ℚ z) (y +ℚ z) + ↔ leq-ℚ zero-ℚ ((y +ℚ z) -ℚ (x +ℚ z)) + by (inv-iff (iff-translate-diff-leq-zero-ℚ (x +ℚ z) (y +ℚ z))) + ↔ leq-ℚ zero-ℚ (y -ℚ x) + by + ( inv-tr + ( _↔ leq-ℚ zero-ℚ (y -ℚ x)) + ( ap (leq-ℚ zero-ℚ) (right-translation-diff-ℚ y x z)) + ( id-iff)) + ↔ leq-ℚ x y by (iff-translate-diff-leq-zero-ℚ x y) preserves-leq-left-add-ℚ : leq-ℚ x y → leq-ℚ (x +ℚ z) (y +ℚ z) preserves-leq-left-add-ℚ = backward-implication iff-translate-right-leq-ℚ diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index f4b630199a..461cb3854d 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -155,14 +155,15 @@ mediant-ℚ x y = ### The rational images of two similar integer fractions are equal ```agda -eq-ℚ-sim-fraction-ℤ : - (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) → - rational-fraction-ℤ x = rational-fraction-ℤ y -eq-ℚ-sim-fraction-ℤ x y H = - eq-pair-Σ' - ( pair - ( unique-reduce-fraction-ℤ x y H) - ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (reduce-fraction-ℤ y)))) +abstract + eq-ℚ-sim-fraction-ℤ : + (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) → + rational-fraction-ℤ x = rational-fraction-ℤ y + eq-ℚ-sim-fraction-ℤ x y H = + eq-pair-Σ' + ( pair + ( unique-reduce-fraction-ℤ x y H) + ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (reduce-fraction-ℤ y)))) ``` ### The type of rationals is a set diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 06174ce77c..3df7d7cd6d 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -106,7 +106,10 @@ module _ ( p' +ℚ (q -ℚ p)) ( q) ( q' From b3b72b244d870facf903ebbd95993c18881cde0b Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 10 Feb 2025 19:28:57 -0800 Subject: [PATCH 41/73] Progress --- ...thmetically-located-dedekind-cuts.lagda.md | 10 +- .../dedekind-real-numbers.lagda.md | 222 +++++++++++------- .../lower-dedekind-real-numbers.lagda.md | 32 ++- .../upper-dedekind-real-numbers.lagda.md | 32 ++- 4 files changed, 199 insertions(+), 97 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 3df7d7cd6d..f4b8c30560 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -60,8 +60,8 @@ module _ {l : Level} (L : lower-ℝ l) (U : upper-ℝ l) where - is-arithmetically-located-pair-of-cuts-ℚ : UU l - is-arithmetically-located-pair-of-cuts-ℚ = + arithmetically-located-lower-upper-ℝ : UU l + arithmetically-located-lower-upper-ℝ = (ε⁺ : ℚ⁺) → exists ( ℚ × ℚ) @@ -79,13 +79,13 @@ rational numbers, it is also located. ```agda module _ - {l : Level} (L : lower-ℝ l) (U : upper-ℝ l) + {l : Level} (x : lower-ℝ l) (y : upper-ℝ l) where abstract is-located-is-arithmetically-located-pair-of-cuts-ℚ : - is-arithmetically-located-pair-of-cuts-ℚ L U → - is-located-cut (cut-lower-ℝ L) (cut-upper-ℝ U) + arithmetically-located-upper-real x y → + is-located-cut (cut-lower-ℝ x) (cut-upper-ℝ y) is-located-is-arithmetically-located-pair-of-cuts-ℚ arithmetically-located p q p

Imports ```agda +open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.conjunction +open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions +open import foundation.sets open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels open import foundation.universal-quantification open import foundation.universe-levels ``` @@ -89,7 +95,18 @@ module _ ## Properties -### Lower Dedekind cuts are closed under the standard ordering on the rationals +### The lower Dedekind reals form a set + +```agda +abstract + is-set-lower-ℝ : (l : Level) → is-set (lower-ℝ l) + is-set-lower-ℝ l = + is-set-Σ + ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋)) + ( λ q → is-set-is-prop (is-prop-type-Prop (is-lower-dedekind-cut-Prop q))) +``` + +### Lower Dedekind cuts are closed under strict inequality on the rationals ```agda module _ @@ -103,6 +120,19 @@ module _ ( intro-exists q (pImports ```agda +open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.conjunction +open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions +open import foundation.sets open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels open import foundation.universal-quantification open import foundation.universe-levels ``` @@ -89,7 +95,18 @@ module _ ## Properties -### Upper Dedekind cuts are closed under the standard ordering on the rationals +### The upper Dedekind reals form a set + +```agda +abstract + is-set-upper-ℝ : (l : Level) → is-set (upper-ℝ l) + is-set-upper-ℝ l = + is-set-Σ + ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋)) + ( λ q → is-set-is-prop (is-prop-type-Prop (is-upper-dedekind-cut-Prop q))) +``` + +### Upper Dedekind cuts are closed under strict inequality on the rationals ```agda module _ @@ -103,6 +120,19 @@ module _ ( intro-exists p (p Date: Mon, 10 Feb 2025 19:45:56 -0800 Subject: [PATCH 42/73] Recover all the previous results --- .../dedekind-real-numbers.lagda.md | 104 +++++------------- 1 file changed, 27 insertions(+), 77 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index d4ec0c3e69..c973a7b3cc 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -21,6 +21,7 @@ open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.embeddings open import foundation.empty-types +open import foundation.equivalences open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types @@ -397,6 +398,14 @@ module _ ( upper-cut-ℝ y) ( H))) + eq-lower-real-eq-upper-real-ℝ : + upper-real-ℝ x = upper-real-ℝ y → lower-real-ℝ x = lower-real-ℝ y + eq-lower-real-eq-upper-real-ℝ ux=uy = + eq-eq-cut-lower-ℝ + ( lower-real-ℝ x) + ( lower-real-ℝ y) + ( eq-lower-cut-eq-upper-cut-ℝ (ap cut-upper-ℝ ux=uy)) + eq-upper-cut-eq-lower-cut-ℝ : lower-cut-ℝ x = lower-cut-ℝ y → upper-cut-ℝ x = upper-cut-ℝ y eq-upper-cut-eq-lower-cut-ℝ H = @@ -413,6 +422,14 @@ module _ ( lower-cut-ℝ x) ( lower-cut-ℝ y) ( H))) + + eq-upper-real-eq-lower-real-ℝ : + lower-real-ℝ x = lower-real-ℝ y → upper-real-ℝ x = upper-real-ℝ y + eq-upper-real-eq-lower-real-ℝ lx=ly = + eq-eq-cut-upper-ℝ + ( upper-real-ℝ x) + ( upper-real-ℝ y) + ( eq-upper-cut-eq-lower-cut-ℝ (ap cut-lower-ℝ lx=ly)) ``` ### The map from a real number to its lower real is an embedding @@ -439,93 +456,26 @@ is-emb-lower-real : {l : Level} → is-emb (lower-real-ℝ {l}) is-emb-lower-real = is-emb-inclusion-subtype has-upper-real-Prop ``` -### The map from a real number to its upper real is an embedding +### Two real numbers with the same lower/upper real are equal ```agda module _ - {l : Level} - (uy : upper-ℝ l) - where - - has-lower-real-Prop : Prop (lsuc l) - pr1 has-lower-real-Prop = - Σ (lower-ℝ l) (λ lx → is-dedekind-lower-upper-ℝ lx uy) - pr2 has-lower-real-Prop = - ( is-prop-all-elements-equal) - ( λ lx lx' → - eq-type-subtype - ( λ l → is-dedekind-prop-lower-upper-ℝ l uy) - ( eq-eq-cut-lower-ℝ - ( pr1 lx) - ( pr1 lx') - ( eq-lower-cut-eq-upper-cut-ℝ - ( pr1 lx , uy , pr2 lx) - ( pr1 lx' , uy , pr2 lx') - ( refl)))) - -is-emb-upper-real : {l : Level} → is-emb (upper-real-ℝ {l}) -pr1 (pr1 (is-emb-upper-real (lx , ux , Hx) (ly , uy , Hy))) ux=uy = - ap - ( λ (uz , lz , Hz) → (lz , uz , Hz)) - ( pr1 - ( pr1 - ( is-emb-inclusion-subtype - ( has-lower-real-Prop) - ( ux , lx , Hx) - ( uy , ly , Hy))) - ( ux=uy)) -pr2 (pr1 (is-emb-upper-real (lx , ux , Hx) (ly , uy , Hy))) ux=uy = - {! (pr2 (pr1 (is-emb-inclusion-subtype has-lower-real-Prop (ux , lx , Hx) (uy , ly , Hy))) ux=uy) !} -pr1 (pr2 (is-emb-upper-real (lx , ux , Hx) (ly , uy , Hy))) ux=uy = - ap - ( λ (uz , lz , Hz) → (lz , uz , Hz)) - ( pr1 - (pr2 - (is-emb-inclusion-subtype - ( has-lower-real-Prop) - ( ux , lx , Hx) - ( uy , ly , Hy))) - ux=uy) -pr2 (pr2 (is-emb-upper-real (lx , ux , Hx) (ly , uy , Hy))) x=y = - {! pr2 (pr2 (is-emb-inclusion-subtype has-lower-real-Prop (ux , lx , Hx) (uy , ly , Hy))) (ap (λ (lz , uz , Hz) → (uz , lz , Hz)) x=y) !} -``` - -### The map from a real number to its lower cut is an embedding - -```agda -{- module _ - {l : Level} (L : subtype l ℚ) + {l : Level} (x y : ℝ l) where - has-upper-cut-Prop : Prop (lsuc l) - has-upper-cut-Prop = - pair - ( Σ (subtype l ℚ) (is-dedekind-cut L)) - ( is-prop-all-elements-equal - ( λ U U' → - eq-type-subtype - ( is-dedekind-cut-Prop L) - ( eq-upper-cut-eq-lower-cut-ℝ - ( pair L U) - ( pair L U') - ( refl)))) - -is-emb-lower-cut : {l : Level} → is-emb (lower-cut-ℝ {l}) -is-emb-lower-cut = is-emb-inclusion-subtype has-upper-cut-Prop -} -``` - -### Two real numbers with the same lower/upper cut are equal + eq-eq-lower-real-ℝ : lower-real-ℝ x = lower-real-ℝ y → x = y + eq-eq-lower-real-ℝ = eq-type-subtype has-upper-real-Prop -```agda -{- module _ - {l : Level} (x y : ℝ l) - where + eq-eq-upper-real-ℝ : upper-real-ℝ x = upper-real-ℝ y → x = y + eq-eq-upper-real-ℝ = eq-eq-lower-real-ℝ ∘ (eq-lower-real-eq-upper-real-ℝ x y) eq-eq-lower-cut-ℝ : lower-cut-ℝ x = lower-cut-ℝ y → x = y - eq-eq-lower-cut-ℝ = eq-type-subtype has-upper-cut-Prop + eq-eq-lower-cut-ℝ lcx=lcy = + eq-eq-lower-real-ℝ + ( eq-eq-cut-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y) lcx=lcy) eq-eq-upper-cut-ℝ : upper-cut-ℝ x = upper-cut-ℝ y → x = y - eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y) -} + eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y) ``` ## References From 263f367ecf3f72d4c45766fcacf734c7e7eceda7 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 11 Feb 2025 15:40:17 -0800 Subject: [PATCH 43/73] make pre-commit --- ...ithmetically-located-dedekind-cuts.lagda.md | 14 +++++++------- .../dedekind-real-numbers.lagda.md | 16 +++++++--------- .../rational-real-numbers.lagda.md | 18 ++++++------------ 3 files changed, 20 insertions(+), 28 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index f4b8c30560..ee15d2d9c1 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -83,22 +83,22 @@ module _ where abstract - is-located-is-arithmetically-located-pair-of-cuts-ℚ : - arithmetically-located-upper-real x y → - is-located-cut (cut-lower-ℝ x) (cut-upper-ℝ y) - is-located-is-arithmetically-located-pair-of-cuts-ℚ + is-located-is-arithmetically-located-lower-upper-ℝ : + arithmetically-located-lower-upper-ℝ x y → + is-located-lower-upper-ℝ x y + is-located-is-arithmetically-located-lower-upper-ℝ arithmetically-located p q p Date: Tue, 11 Feb 2025 15:47:49 -0800 Subject: [PATCH 44/73] Remove empty bibliography --- .../inequality-lower-dedekind-real-numbers.lagda.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md index 7a73363b9c..26abd2fb42 100644 --- a/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/inequality-lower-dedekind-real-numbers.lagda.md @@ -111,7 +111,3 @@ iff-leq-lower-real-ℚ : pr1 (iff-leq-lower-real-ℚ p q) = preserves-leq-lower-real-ℚ p q pr2 (iff-leq-lower-real-ℚ p q) = reflects-leq-lower-real-ℚ p q ``` - -## References - -{{#bibliography}} From 827111e46a69879d9d18e743bfc0e3de068f73b7 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 11 Feb 2025 15:58:20 -0800 Subject: [PATCH 45/73] Review changes --- .../lower-dedekind-real-numbers.lagda.md | 28 ++++++++++++------- .../upper-dedekind-real-numbers.lagda.md | 28 ++++++++++++------- 2 files changed, 36 insertions(+), 20 deletions(-) diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index 948f6e60bd..db4cf96ad6 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -15,8 +15,10 @@ open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtypes @@ -31,9 +33,8 @@ open import foundation.universe-levels ## Idea -A lower -{{#concept "Dedekind cut" Agda=is-dedekind-cut WD="dedekind cut" WDID=Q851333}} -consists of a [subtype](foundation-core.subtypes.md) `L` of +A {{#concept "lower Dedekind cut" Agda=is-lower-dedekind-cut}} consists of a +[subtype](foundation-core.subtypes.md) `L` of [the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, satisfying the following two conditions: @@ -42,8 +43,8 @@ satisfying the following two conditions: [if and only if](foundation.logical-equivalences.md) there [exists](foundation.existential-quantification.md) `q < r` such that `r ∈ L`. -The type of all lower Dedekind real numbers is the type of all lower Dedekind -cuts. +The {{#concept "lower Dedekind real numbers" Agda=lower-ℝ}} is the type of all +lower Dedekind cuts. ## Definition @@ -113,8 +114,9 @@ module _ {l : Level} (x : lower-ℝ l) (p q : ℚ) where - le-cut-lower-ℝ : le-ℚ p q → is-in-cut-lower-ℝ x q → is-in-cut-lower-ℝ x p - le-cut-lower-ℝ p Date: Tue, 11 Feb 2025 16:15:25 -0800 Subject: [PATCH 46/73] Fix names --- .../arithmetically-located-dedekind-cuts.lagda.md | 4 ++-- src/real-numbers/dedekind-real-numbers.lagda.md | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index ee15d2d9c1..38e39bfb9e 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -94,10 +94,10 @@ module _ rec-coproduct ( λ p Date: Tue, 11 Feb 2025 21:07:48 -0800 Subject: [PATCH 47/73] Fix links --- src/real-numbers/dedekind-real-numbers.lagda.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 76134fd985..3e6695ebce 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -51,8 +51,9 @@ open import real-numbers.upper-dedekind-real-numbers ## Idea A Dedekind real number consists of a [pair](foundation.dependent-pair-types.md) -`(lx , uy)` of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers) -and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers) that also +`(lx , uy)` of a +[lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) and an +[upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) that also satisfy the following conditions: 1. _Disjointness_. The cuts of `lx` and `uy` are disjoint subsets of `ℚ`. From 71479cac22d2f14bac981f0d66592b74e1d85048 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 12 Feb 2025 11:20:08 -0800 Subject: [PATCH 48/73] Fix naming --- .../arithmetically-located-dedekind-cuts.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 38e39bfb9e..fe8f273ea0 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -42,8 +42,8 @@ open import real-numbers.upper-dedekind-real-numbers ## Definition -A pair of a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) -`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U` +A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) +`L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) `U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for any positive [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ`, there exist `p, q : ℚ` such that `0 < q - p < ε`, `p ∈ L`, and `q ∈ U`. From 9f12eee4548ad0a47f816c940993fbbd0b9b948e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 12 Feb 2025 11:31:14 -0800 Subject: [PATCH 49/73] Progress on upper addition --- ...ition-upper-dedekind-real-numbers.lagda.md | 208 ++++++++++++++++++ 1 file changed, 208 insertions(+) create mode 100644 src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md diff --git a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md new file mode 100644 index 0000000000..bc9d4da02a --- /dev/null +++ b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md @@ -0,0 +1,208 @@ +# Addition of upper Dedekind real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.addition-upper-dedekind-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import group-theory.abelian-groups +open import group-theory.groups +open import group-theory.minkowski-multiplication-commutative-monoids + +open import real-numbers.upper-dedekind-real-numbers +``` + +
+ +## Idea + +The sum of two [upper Dedekind real numbers](real-numbers.upper-dedekind-real-numbers.md) +is the Minkowski sum of their cuts. + +```agda +module _ + {l1 l2 : Level} + (x : upper-ℝ l1) + (y : upper-ℝ l2) + where + + cut-add-upper-ℝ : subtype (l1 ⊔ l2) ℚ + cut-add-upper-ℝ = + minkowski-mul-Commutative-Monoid + ( commutative-monoid-add-ℚ) + ( cut-upper-ℝ x) + ( cut-upper-ℝ y) + + is-in-cut-add-upper-ℝ : ℚ → UU (l1 ⊔ l2) + is-in-cut-add-upper-ℝ = is-in-subtype cut-add-upper-ℝ + + is-inhabited-cut-add-upper-ℝ : exists ℚ cut-add-upper-ℝ + is-inhabited-cut-add-upper-ℝ = + minkowski-mul-inhabited-is-inhabited-Commutative-Monoid + ( commutative-monoid-add-ℚ) + ( cut-upper-ℝ x) + ( cut-upper-ℝ y) + ( is-inhabited-cut-upper-ℝ x) + ( is-inhabited-cut-upper-ℝ y) + + abstract + is-rounded-cut-add-upper-ℝ : + (q : ℚ) → + is-in-cut-add-upper-ℝ q ↔ + exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p) + pr1 (is-rounded-cut-add-upper-ℝ q) = + elim-exists + ( ∃ ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p)) + ( λ (ux , uy) (x Date: Wed, 12 Feb 2025 11:31:45 -0800 Subject: [PATCH 50/73] make pre-commit --- .../arithmetically-located-dedekind-cuts.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index fe8f273ea0..405a77a7e2 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -43,9 +43,9 @@ open import real-numbers.upper-dedekind-real-numbers ## Definition A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) -`L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) `U` -is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for -any positive [rational number](elementary-number-theory.rational-numbers.md) +`L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) +`U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if +for any positive [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ`, there exist `p, q : ℚ` such that `0 < q - p < ε`, `p ∈ L`, and `q ∈ U`. Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows parts of Section From 74a4defe05d5e9546041eaf5e2253dba830ee7db Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 12 Feb 2025 12:15:35 -0800 Subject: [PATCH 51/73] make pre-commit --- src/real-numbers.lagda.md | 2 + ...ition-lower-dedekind-real-numbers.lagda.md | 15 ++- ...ition-upper-dedekind-real-numbers.lagda.md | 117 ++++++++---------- 3 files changed, 66 insertions(+), 68 deletions(-) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 1cd86ceaa3..ce1bcaf270 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -5,6 +5,8 @@ ```agda module real-numbers where +open import real-numbers.addition-lower-dedekind-real-numbers public +open import real-numbers.addition-upper-dedekind-real-numbers public open import real-numbers.arithmetically-located-dedekind-cuts public open import real-numbers.dedekind-real-numbers public open import real-numbers.inequality-lower-dedekind-real-numbers public diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index c45c75d99b..0073594d5b 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -28,12 +28,12 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels -open import logic.functoriality-existential-quantification - open import group-theory.abelian-groups open import group-theory.groups open import group-theory.minkowski-multiplication-commutative-monoids +open import logic.functoriality-existential-quantification + open import real-numbers.lower-dedekind-real-numbers ``` @@ -41,8 +41,11 @@ open import real-numbers.lower-dedekind-real-numbers ## Idea -The sum of two [lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md) -is the Minkowski sum of their cuts. +The sum of two +[lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md) is +the +[Minkowski sum](group-theory.minkowski-multiplication-commutative-monoids.md) of +their cuts. ```agda module _ @@ -109,13 +112,13 @@ module _ in intro-exists ( rx -ℚ ε , q -ℚ (rx -ℚ ε)) - ( le-cut-lower-ℝ + ( is-in-cut-le-ℚ-lower-ℝ ( x) ( rx -ℚ ε) ( rx) ( le-diff-rational-ℚ⁺ rx ε⁺) ( rx Date: Wed, 12 Feb 2025 22:14:37 -0800 Subject: [PATCH 52/73] Rewrite in terms of propositional truncation --- .../existential-quantification.lagda.md | 42 ------------- .../propositional-truncations.lagda.md | 59 +++++++++++++++++++ .../strict-inequality-real-numbers.lagda.md | 11 ++-- 3 files changed, 65 insertions(+), 47 deletions(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index 04483c575f..a15d2258a9 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -331,48 +331,6 @@ module _ eq-distributive-product-exists-structure P ``` -## Existential quantification `do` syntax - -When eliminating a chain of existential quantifications, which may be -interdependent, -[Agda's `do` syntax](https://agda.readthedocs.io/en/stable/language/syntactic-sugar.html#do-notation) -can eliminate many levels of nesting. - -For example, suppose we have - -```text -R : Prop l - -exists-a-p : exists A P -a-p-implies-b-q-exists : (a : A) → P a → exists B Q -a-b-p-q-implies-r : (a : A) (b : B) → P a → Q b → R -``` - -To deduce `R`, we could write - -```text -do - a , pa ← exists-a-p - b , qb ← a-p-implies-b-q-exists a pa - a-b-p-q-implies-r a b pa qb -where open do-syntax-elim-exists R -``` - -instead of a nested chain of `elim-exists`. - -```agda -module do-syntax-elim-exists - {l : Level} - (P : Prop l) - where - - _>>=_ : - {l1 l2 : Level} {A : UU l1} {B : A -> UU l2} → - exists-structure A B → - (Σ A B -> type-Prop P) -> type-Prop P - x >>= f = elim-exists P (ev-pair f) x -``` - ## See also - Existential quantification is the indexed counterpart to diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 1181cc2572..5f2cfd7bb5 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -446,6 +446,65 @@ module _ is-equiv-map-inv-trunc-Prop-diagonal-coproduct ``` +## `do` syntax for propositional truncation + +[Agda's `do` syntax](https://agda.readthedocs.io/en/v2.7.0/language/syntactic-sugar.html#do-notation) +is a handy tool to avoid deeply nesting calls to the same lambda-based function. +For example, consider a case where you are trying to prove a proposition, +`motive : Prop l`, from a chain of truncated propositions `P` and `Q`, where +showing `Q` requires having a value of `type-Prop P`: + +```text +rec-trunc-Prop + ( motive) + ( λ q → + rec-trunc-Prop + ( motive) + ( λ q → derive-motive-from p q) + ( truncated-prop-Q p)) + ( truncated-prop-P) +``` + +The tower of indentation, with many layers of indentation in the innermost +derivation, is painful; there are many duplicated lines of +`rec-trunc-Prop motive`. Agda's `do` syntax offers us an alternative. + +```agda +module do-syntax-trunc-Prop {l : Level} (motive : Prop l) where + _>>=_ : + {l : Level} {A : UU l} → + type-trunc-Prop A → (A → type-Prop motive) → + type-Prop motive + trunc-prop-a >>= k = rec-trunc-Prop motive k trunc-prop-a +``` + +This allows us to rewrite the deeply nested chain above + +```text +do + p ← truncated-prop-P + q ← truncated-prop-Q p + derive-motive-from p q +where open do-syntax-trunc-Prop motive +``` + +Note that the last line, `where open do-syntax-trunc-Prop motive`, is required +to make this syntax possible. + +In general, you can read the `p ← truncated-prop-P` as an _instruction_ saying, +"Get the value `p` out of its truncation `truncated-prop-Q`." We obviously +cannot get values out of truncations in general, but conceptually, we can do it +in the service of proving a proposition, and that's what we're doing here. The +following line `q ← truncated-prop-Q p` says, "Get the value `q` out of the +truncation `truncated-prop-Q p`" -- noticing that we can make use of `p` in that +line. Finally, `derive-motive-from p q` must give us a value of type +`type-Prop motive` from `p` and `q`. The result of the entire `do` block is the +value of type `type-Prop motive`, which is internally constructed with an +appropriate chain of `rec-trunc-Prop` from the intermediate steps. + +While we had each line depend on all the values from the lines above it, this is +not at all required. + ## Table of files about propositional logic The following table gives an overview of basic constructions in propositional diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md index e6c6041f4b..1cf4481302 100644 --- a/src/real-numbers/strict-inequality-real-numbers.lagda.md +++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md @@ -24,6 +24,7 @@ open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation +open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.transport-along-identifications @@ -105,7 +106,7 @@ module _ ( q) ( le-lower-upper-cut-ℝ y p q p Date: Wed, 12 Feb 2025 22:22:58 -0800 Subject: [PATCH 53/73] More words --- src/foundation/propositional-truncations.lagda.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 5f2cfd7bb5..87986c98ab 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -466,8 +466,11 @@ rec-trunc-Prop ``` The tower of indentation, with many layers of indentation in the innermost -derivation, is painful; there are many duplicated lines of -`rec-trunc-Prop motive`. Agda's `do` syntax offers us an alternative. +derivation, is a little awkward even at two levels, let alone more. In +particular, we have the many duplicated lines of +`rec-trunc-Prop motive`, and the increasing distance between the +`rec-trunc-Prop` and the `trunc-Prop` being recursed on. +Agda's `do` syntax offers us an alternative. ```agda module do-syntax-trunc-Prop {l : Level} (motive : Prop l) where @@ -478,7 +481,7 @@ module do-syntax-trunc-Prop {l : Level} (motive : Prop l) where trunc-prop-a >>= k = rec-trunc-Prop motive k trunc-prop-a ``` -This allows us to rewrite the deeply nested chain above +This allows us to rewrite the nested chain above as ```text do From e510c3d10b7d37a49fa96bab3302b37e69a184a2 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 12 Feb 2025 22:23:29 -0800 Subject: [PATCH 54/73] make pre-commit --- src/foundation/propositional-truncations.lagda.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 87986c98ab..5c6123e515 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -466,11 +466,10 @@ rec-trunc-Prop ``` The tower of indentation, with many layers of indentation in the innermost -derivation, is a little awkward even at two levels, let alone more. In -particular, we have the many duplicated lines of -`rec-trunc-Prop motive`, and the increasing distance between the -`rec-trunc-Prop` and the `trunc-Prop` being recursed on. -Agda's `do` syntax offers us an alternative. +derivation, is a little awkward even at two levels, let alone more. In +particular, we have the many duplicated lines of `rec-trunc-Prop motive`, and +the increasing distance between the `rec-trunc-Prop` and the `trunc-Prop` being +recursed on. Agda's `do` syntax offers us an alternative. ```agda module do-syntax-trunc-Prop {l : Level} (motive : Prop l) where From b4e7234f8a96af9dff8fa8c28abe883de6253c62 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 12 Feb 2025 22:25:44 -0800 Subject: [PATCH 55/73] Reorganize --- .../propositional-truncations.lagda.md | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 5c6123e515..1a38564da6 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -490,22 +490,22 @@ do where open do-syntax-trunc-Prop motive ``` -Note that the last line, `where open do-syntax-trunc-Prop motive`, is required -to make this syntax possible. - -In general, you can read the `p ← truncated-prop-P` as an _instruction_ saying, -"Get the value `p` out of its truncation `truncated-prop-Q`." We obviously -cannot get values out of truncations in general, but conceptually, we can do it -in the service of proving a proposition, and that's what we're doing here. The -following line `q ← truncated-prop-Q p` says, "Get the value `q` out of the -truncation `truncated-prop-Q p`" -- noticing that we can make use of `p` in that -line. Finally, `derive-motive-from p q` must give us a value of type -`type-Prop motive` from `p` and `q`. The result of the entire `do` block is the -value of type `type-Prop motive`, which is internally constructed with an -appropriate chain of `rec-trunc-Prop` from the intermediate steps. - -While we had each line depend on all the values from the lines above it, this is -not at all required. +Going through each line: + +1. You can read the `p ← truncated-prop-P` as an _instruction_ saying, "Get the + value `p` out of its truncation `truncated-prop-Q`." We obviously cannot get + values out of truncations in general, but conceptually, we can do it in the + service of proving a proposition, and that's what we're doing here. +2. `q ← truncated-prop-Q p` says, "Get the value `q` out of the truncation + `truncated-prop-Q p`" -- noticing that we can make use of `p` in that line. +3. `derive-motive-from p q` must give us a value of type `type-Prop motive` from + `p` and `q`. +4. `where open do-syntax-trunc-Prop motive` is required to allow us to use the + `do` syntax. + +The result of the entire `do` block is the value of type `type-Prop motive`, +which is internally constructed with an appropriate chain of `rec-trunc-Prop` +from the intermediate steps. ## Table of files about propositional logic From 6cd9e60a6d17c1639fd6d03945c76bd8f9f33ea7 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 14:38:04 -0800 Subject: [PATCH 56/73] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- src/foundation/propositional-truncations.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 1a38564da6..6d4d6c259e 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -446,7 +446,7 @@ module _ is-equiv-map-inv-trunc-Prop-diagonal-coproduct ``` -## `do` syntax for propositional truncation +## `do` syntax for propositional truncation { #do-syntax } [Agda's `do` syntax](https://agda.readthedocs.io/en/v2.7.0/language/syntactic-sugar.html#do-notation) is a handy tool to avoid deeply nesting calls to the same lambda-based function. From 45f47a805d65d39b85f5859043e23e8d5a9f97e2 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 14:59:08 -0800 Subject: [PATCH 57/73] Formatting --- .../existential-quantification.lagda.md | 5 ++ .../propositional-truncations.lagda.md | 59 ++++++++++++------- 2 files changed, 43 insertions(+), 21 deletions(-) diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md index a15d2258a9..07e29f4bb7 100644 --- a/src/foundation/existential-quantification.lagda.md +++ b/src/foundation/existential-quantification.lagda.md @@ -202,6 +202,11 @@ module _ ( elim-exists Q) ``` +Note that since existential quantification is implemented using propositional +truncation, the associated +[do syntax](foundation.propositional-truncations.md#do-syntax) can be used to +simplify deeply nested chains of `elim-exists`. + ### The existential quantification satisfies the universal property of existential quantification ```agda diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 1a38564da6..5f59a9bafc 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -446,23 +446,23 @@ module _ is-equiv-map-inv-trunc-Prop-diagonal-coproduct ``` -## `do` syntax for propositional truncation +## `do` syntax for propositional truncation {#do-syntax} [Agda's `do` syntax](https://agda.readthedocs.io/en/v2.7.0/language/syntactic-sugar.html#do-notation) is a handy tool to avoid deeply nesting calls to the same lambda-based function. For example, consider a case where you are trying to prove a proposition, -`motive : Prop l`, from a chain of truncated propositions `P` and `Q`, where -showing `Q` requires having a value of `type-Prop P`: +`motive : Prop l`, from witnesses of propositional truncations of types `P` and +`Q`: ```text rec-trunc-Prop ( motive) - ( λ q → + ( λ (p : P) → rec-trunc-Prop ( motive) - ( λ q → derive-motive-from p q) - ( truncated-prop-Q p)) - ( truncated-prop-P) + ( λ (q : Q) → witness-motive-P-Q p q) + ( witness-truncated-prop-Q p)) + ( witness-truncated-prop-P) ``` The tower of indentation, with many layers of indentation in the innermost @@ -484,23 +484,40 @@ This allows us to rewrite the nested chain above as ```text do - p ← truncated-prop-P - q ← truncated-prop-Q p - derive-motive-from p q + p ← witness-truncated-prop-P + q ← witness-truncated-prop-Q p + witness-motive-P-Q p q where open do-syntax-trunc-Prop motive ``` -Going through each line: - -1. You can read the `p ← truncated-prop-P` as an _instruction_ saying, "Get the - value `p` out of its truncation `truncated-prop-Q`." We obviously cannot get - values out of truncations in general, but conceptually, we can do it in the - service of proving a proposition, and that's what we're doing here. -2. `q ← truncated-prop-Q p` says, "Get the value `q` out of the truncation - `truncated-prop-Q p`" -- noticing that we can make use of `p` in that line. -3. `derive-motive-from p q` must give us a value of type `type-Prop motive` from - `p` and `q`. -4. `where open do-syntax-trunc-Prop motive` is required to allow us to use the +Since Agda's `do` syntax desugars to calls to `>>=`, this is simply syntactic +sugar for + +```text +witness-truncated-prop-P >>= + ( λ p → witness-truncated-prop-Q p >>= + ( λ q → witness-motive-P-Q p q)) +``` + +which, inlining the definition of `>>=`, becomes exactly the chain of +`rec-trunc-Prop` used above. + +To read the `do` syntax, it may help to go through each line: + +1. `do` simply indicates that we will be using Agda's syntactic sugar for the + `>>=` function defined in the `do-syntax-trunc-Prop` module. +1. You can read the `p ← witness-truncated-prop-P` as an _instruction_ saying, + "Get the value `p` out of the witness of `trunc-Prop P`." We cannot extract + elements out of witnesses of propositionally truncated types, but since we're + eliminating into a proposition, the universal property of the truncation + allows us to lift a map from the untruncated type to a map from its + truncation. +1. `q ← witness-truncated-prop-Q p` says, "Get the value `q` out of the witness + for the truncation `witness-truncated-prop-Q p`" -- noticing that we can make + use of `p : P` in that line. +1. `witness-motive-P-Q p q` must give us a witness of `motive` -- that is, a + value of type `type-Prop motive` -- from `p` and `q`. +1. `where open do-syntax-trunc-Prop motive` is required to allow us to use the `do` syntax. The result of the entire `do` block is the value of type `type-Prop motive`, From 23a33d354e3d0c034e5cec8180b9c058a04d6db9 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 15:07:01 -0800 Subject: [PATCH 58/73] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- ...rithmetically-located-dedekind-cuts.lagda.md | 2 +- src/real-numbers/dedekind-real-numbers.lagda.md | 17 ++++++++--------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 405a77a7e2..aaba62504f 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -46,7 +46,7 @@ A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) `L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) `U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for any positive [rational number](elementary-number-theory.rational-numbers.md) -`ε : ℚ`, there exist `p, q : ℚ` such that `0 < q - p < ε`, `p ∈ L`, and `q ∈ U`. +`ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows parts of Section 11 in {{#cite BauerTaylor2009}}. diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 3e6695ebce..e68152a823 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -50,22 +50,21 @@ open import real-numbers.upper-dedekind-real-numbers ## Idea -A Dedekind real number consists of a [pair](foundation.dependent-pair-types.md) -`(lx , uy)` of a -[lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) and an -[upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) that also -satisfy the following conditions: +A {{#concept "Dedekind real number" WD="real number" WDID=Q12916 Agda=ℝ}} `x` consists of a [pair](foundation.dependent-pair-types.md) + of _cuts_ `(L , U)` of [rational numbers](elementary-number-theory.rational-numbers.md), a +[lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) `L` and an +[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. These cuts present lower and upper bounds on the Dedekind real number, and must satisfy the conditions -1. _Disjointness_. The cuts of `lx` and `uy` are disjoint subsets of `ℚ`. -2. _Locatedness_. If `q < r` then `q` is in the cut of `lx` or `r` is in the cut - of `uy`. +1. _Disjointness_. The cuts `lx` and `uy` are disjoint subsets of `ℚ`. +2. _Locatedness_. If `q < r` then `q` is in the cut `L` or `r` is in the cut `U`. +The {{#concept "collection of all Dedekind real numbers" WD="set of real numbers" WDID=Q1174982 Agda=ℝ}} is denoted `ℝ`. The Dedekind real numbers will be taken as the standard definition of the real numbers in the agda-unimath library. ## Definition -### Dedekind real numbers +### Dedekind cuts ```agda module _ From f2c3f7646486d0f5b5894418ea4baa08847a3f65 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 15:13:49 -0800 Subject: [PATCH 59/73] renaming --- src/real-numbers/dedekind-real-numbers.lagda.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index e68152a823..4c2e2f5a10 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -438,10 +438,11 @@ module _ (lx : lower-ℝ l) where - has-upper-real-Prop : Prop (lsuc l) - pr1 has-upper-real-Prop = Σ (upper-ℝ l) (is-dedekind-lower-upper-ℝ lx) - pr2 has-upper-real-Prop = - ( is-prop-all-elements-equal) + is-dedekind-cut-lower-ℝ-Prop : Prop (lsuc l) + pr1 is-dedekind-cut-lower-ℝ-Prop = + Σ (upper-ℝ l) (is-dedekind-lower-upper-ℝ lx) + pr2 is-dedekind-cut-lower-ℝ-Prop = + is-prop-all-elements-equal ( λ uy uy' → eq-type-subtype ( is-dedekind-prop-lower-upper-ℝ lx) @@ -451,7 +452,7 @@ module _ ( eq-upper-cut-eq-lower-cut-ℝ (lx , uy) (lx , uy') refl))) is-emb-lower-real : {l : Level} → is-emb (lower-real-ℝ {l}) -is-emb-lower-real = is-emb-inclusion-subtype has-upper-real-Prop +is-emb-lower-real = is-emb-inclusion-subtype is-dedekind-cut-lower-ℝ-Prop ``` ### Two real numbers with the same lower/upper real are equal @@ -462,7 +463,7 @@ module _ where eq-eq-lower-real-ℝ : lower-real-ℝ x = lower-real-ℝ y → x = y - eq-eq-lower-real-ℝ = eq-type-subtype has-upper-real-Prop + eq-eq-lower-real-ℝ = eq-type-subtype is-dedekind-cut-lower-ℝ-Prop eq-eq-upper-real-ℝ : upper-real-ℝ x = upper-real-ℝ y → x = y eq-eq-upper-real-ℝ = eq-eq-lower-real-ℝ ∘ (eq-lower-real-eq-upper-real-ℝ x y) From 36731631bde357cfda2527326f45a3d388ab945f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 15:58:03 -0800 Subject: [PATCH 60/73] make pre-commit --- ...thmetically-located-dedekind-cuts.lagda.md | 8 ++++---- .../dedekind-real-numbers.lagda.md | 19 ++++++++++++------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index aaba62504f..f290bbe754 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -46,10 +46,10 @@ A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) `L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) `U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if for any positive [rational number](elementary-number-theory.rational-numbers.md) -`ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. -Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` -are rational approximations of `x` to within `ε`. This follows parts of Section -11 in {{#cite BauerTaylor2009}}. +`ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that +`0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number +`x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows +parts of Section 11 in {{#cite BauerTaylor2009}}. ## Definitions diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 4c2e2f5a10..3b6c9ce2bc 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -50,17 +50,22 @@ open import real-numbers.upper-dedekind-real-numbers ## Idea -A {{#concept "Dedekind real number" WD="real number" WDID=Q12916 Agda=ℝ}} `x` consists of a [pair](foundation.dependent-pair-types.md) - of _cuts_ `(L , U)` of [rational numbers](elementary-number-theory.rational-numbers.md), a +A {{#concept "Dedekind real number" WD="real number" WDID=Q12916 Agda=ℝ}} `x` +consists of a [pair](foundation.dependent-pair-types.md) of _cuts_ `(L , U)` of +[rational numbers](elementary-number-theory.rational-numbers.md), a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) `L` and an -[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. These cuts present lower and upper bounds on the Dedekind real number, and must satisfy the conditions +[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. These +cuts present lower and upper bounds on the Dedekind real number, and must +satisfy the conditions 1. _Disjointness_. The cuts `lx` and `uy` are disjoint subsets of `ℚ`. -2. _Locatedness_. If `q < r` then `q` is in the cut `L` or `r` is in the cut `U`. +2. _Locatedness_. If `q < r` then `q` is in the cut `L` or `r` is in the cut + `U`. -The {{#concept "collection of all Dedekind real numbers" WD="set of real numbers" WDID=Q1174982 Agda=ℝ}} is denoted `ℝ`. -The Dedekind real numbers will be taken as the standard definition of the real -numbers in the agda-unimath library. +The +{{#concept "collection of all Dedekind real numbers" WD="set of real numbers" WDID=Q1174982 Agda=ℝ}} +is denoted `ℝ`. The Dedekind real numbers will be taken as the standard +definition of the real numbers in the agda-unimath library. ## Definition From 324595aba9740dec0caaae65e69922c4fb08631e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:02:06 -0800 Subject: [PATCH 61/73] Respond to review comments --- src/real-numbers/lower-dedekind-real-numbers.lagda.md | 8 ++++---- src/real-numbers/upper-dedekind-real-numbers.lagda.md | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md index db4cf96ad6..ddae49559d 100644 --- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md @@ -33,10 +33,10 @@ open import foundation.universe-levels ## Idea -A {{#concept "lower Dedekind cut" Agda=is-lower-dedekind-cut}} consists of a -[subtype](foundation-core.subtypes.md) `L` of -[the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, -satisfying the following two conditions: +A [subtype](foundation-core.subtypes.md) `L` of +[the rational numbers](elementary-number-theory.rational-numbers.md) is a +{{#concept "lower Dedekind cut" Agda=is-lower-dedekind-cut}} if it satisfies the +following two conditions: 1. _Inhabitedness_. `L` is [inhabited](foundation.inhabited-subtypes.md). 2. _Roundedness_. A rational number `q` is in `L` diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md index 83d2328e84..da99075a67 100644 --- a/src/real-numbers/upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md @@ -33,10 +33,10 @@ open import foundation.universe-levels ## Idea -An {{#concept "upper Dedekind cut" Agda=is-upper-dedekind-cut}} consists of a -[subtype](foundation-core.subtypes.md) `U` of -[the rational numbers](elementary-number-theory.rational-numbers.md) `ℚ`, -satisfying the following two conditions: +A [subtype](foundation-core.subtypes.md) `U` of +[the rational numbers](elementary-number-theory.rational-numbers.md) is an +{{#concept "upper Dedekind cut" Agda=is-upper-dedekind-cut}} if it satisfies the +following two conditions: 1. _Inhabitedness_. `U` is [inhabited](foundation.inhabited-subtypes.md). 2. _Roundedness_. A rational number `q` is in `U` From 10a0a3612d92e4893433fcbdedf8d7a8d23d58c1 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:06:06 -0800 Subject: [PATCH 62/73] Inline explanations of lower and upper cuts --- src/real-numbers/dedekind-real-numbers.lagda.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 3b6c9ce2bc..912f8f9676 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -54,8 +54,15 @@ A {{#concept "Dedekind real number" WD="real number" WDID=Q12916 Agda=ℝ}} `x` consists of a [pair](foundation.dependent-pair-types.md) of _cuts_ `(L , U)` of [rational numbers](elementary-number-theory.rational-numbers.md), a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) `L` and an -[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. These -cuts present lower and upper bounds on the Dedekind real number, and must +[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. A lower +Dedekind cut `L` is a subtype of the rational numbers that is +[inhabited](foundation.inhabited-subtypes.md) and rounded, meaning that `q ∈ L` +[if and only if](foundation.logical-equivalences.md) there exists `r`, with +`q < r` and `r ∈ L`. An upper Dedekind cut is a subtype of the rational numbers +that is inhabited and rounded "in the other direction": `q ∈ U` if and only if +there is a `p < q` where `p ∈ U`. + +These cuts present lower and upper bounds on the Dedekind real number, and must satisfy the conditions 1. _Disjointness_. The cuts `lx` and `uy` are disjoint subsets of `ℚ`. From 6430f86be2f1172423b78799be52cbdfc11075c5 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:07:55 -0800 Subject: [PATCH 63/73] Reword --- .../dedekind-real-numbers.lagda.md | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 912f8f9676..3f83f4b510 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -54,13 +54,18 @@ A {{#concept "Dedekind real number" WD="real number" WDID=Q12916 Agda=ℝ}} `x` consists of a [pair](foundation.dependent-pair-types.md) of _cuts_ `(L , U)` of [rational numbers](elementary-number-theory.rational-numbers.md), a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) `L` and an -[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. A lower -Dedekind cut `L` is a subtype of the rational numbers that is -[inhabited](foundation.inhabited-subtypes.md) and rounded, meaning that `q ∈ L` -[if and only if](foundation.logical-equivalences.md) there exists `r`, with -`q < r` and `r ∈ L`. An upper Dedekind cut is a subtype of the rational numbers -that is inhabited and rounded "in the other direction": `q ∈ U` if and only if -there is a `p < q` where `p ∈ U`. +[upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U`. + +A lower Dedekind cut `L` is a subtype of the rational numbers that is + +1. [Inhabited](foundation.inhabited-subtypes.md), meaning it has at least one + element. +2. Rounded, meaning that `q ∈ L` + [if and only if](foundation.logical-equivalences.md) there exists `r`, with + `q < r` and `r ∈ L`. + +An upper Dedekind cut is analogous, but must be rounded "in the other +direction": `q ∈ U` if and only if there is a `p < q` where `p ∈ U`. These cuts present lower and upper bounds on the Dedekind real number, and must satisfy the conditions From 69430a2f07180d25ca98d501cbfb8d678b8f1c54 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:19:20 -0800 Subject: [PATCH 64/73] Update src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index f290bbe754..4826d54cc4 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -44,7 +44,7 @@ open import real-numbers.upper-dedekind-real-numbers A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) `L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) -`U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut"}} if +`U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut" Agda=arithmetically-located-lower-upper-ℝ}} if for any positive [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number From 8c1ad1108ac8a1b05fc13089c18e82f6cf961a7e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:21:08 -0800 Subject: [PATCH 65/73] Progress --- .../arithmetically-located-dedekind-cuts.lagda.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 4826d54cc4..abd7034a5e 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -42,18 +42,19 @@ open import real-numbers.upper-dedekind-real-numbers ## Definition -A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md) -`L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md) +A pair of a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) +`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut" Agda=arithmetically-located-lower-upper-ℝ}} if -for any positive [rational number](elementary-number-theory.rational-numbers.md) -`ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that +for any [positive](elementary-number-theory.positive-rational-numbers.md) +[rational number](elementary-number-theory.rational-numbers.md) +`ε : ℚ⁺`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ## Definitions -### The predicate of being arithmetically located on pairs of subtypes of rational numbers +### The predicate of being arithmetically located on pairs of lower and upper Dedekind real numbers ```agda module _ @@ -74,8 +75,7 @@ module _ ### Arithmetically located cuts are located -If a cut is arithmetically located and closed under strict inequality on the -rational numbers, it is also located. +If a pair of lower and upper Dedekind cuts is arithmetically located, it is also located. ```agda module _ From 9f4197ca964c339bb510ff2b7849c203b1e2246c Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:21:52 -0800 Subject: [PATCH 66/73] Review comments --- .../arithmetically-located-dedekind-cuts.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index abd7034a5e..5b589d3f7e 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -49,7 +49,9 @@ for any [positive](elementary-number-theory.positive-rational-numbers.md) [rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ⁺`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number -`x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows +`x`, `p` and `q` are rational approximations of `x` to within `ε`. + +This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ## Definitions From d6da82420b1046f383d342b4128edd2bafe5e501 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:24:05 -0800 Subject: [PATCH 67/73] reword negation --- ...thmetically-located-dedekind-cuts.lagda.md | 21 ++++++++++--------- ...lower-upper-dedekind-real-numbers.lagda.md | 6 ++++-- 2 files changed, 15 insertions(+), 12 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index 5b589d3f7e..dc0ce73fc2 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -43,16 +43,16 @@ open import real-numbers.upper-dedekind-real-numbers ## Definition A pair of a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md) -`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) -`U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut" Agda=arithmetically-located-lower-upper-ℝ}} if -for any [positive](elementary-number-theory.positive-rational-numbers.md) -[rational number](elementary-number-theory.rational-numbers.md) -`ε : ℚ⁺`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that -`0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number -`x`, `p` and `q` are rational approximations of `x` to within `ε`. +`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md) `U` +is +{{#concept "arithmetically located" Disambiguation="Dedekind cut" Agda=arithmetically-located-lower-upper-ℝ}} +if for any [positive](elementary-number-theory.positive-rational-numbers.md) +[rational number](elementary-number-theory.rational-numbers.md) `ε : ℚ⁺`, there +exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that `0 < q - p < ε`. +Intuitively, when `L , U` represent the cuts of a real number `x`, `p` and `q` +are rational approximations of `x` to within `ε`. -This follows -parts of Section 11 in {{#cite BauerTaylor2009}}. +This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ## Definitions @@ -77,7 +77,8 @@ module _ ### Arithmetically located cuts are located -If a pair of lower and upper Dedekind cuts is arithmetically located, it is also located. +If a pair of lower and upper Dedekind cuts is arithmetically located, it is also +located. ```agda module _ diff --git a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md index 5c6f4d84f5..b9847a632c 100644 --- a/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/negation-lower-upper-dedekind-real-numbers.lagda.md @@ -40,8 +40,10 @@ open import real-numbers.upper-dedekind-real-numbers ## Idea -The negation of a lower Dedekind real is an upper Dedekind real containing the -negations of elements in the lower cut, and vice versa. +The negation of a +[lower Dedekind real number](real-numbers.lower-dedekind-real-numbers.md) is an +[upper Dedekind real number](real-numbers.upper-dedekind-real-numbers.md) whose +cut contains negations of elements in the lower cut, and vice versa. ## Definition From 0a2691ca5cddb2441a32e7c73cf5133cdec1bb03 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:24:49 -0800 Subject: [PATCH 68/73] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../arithmetically-located-dedekind-cuts.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index dc0ce73fc2..c3d4d59716 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -60,7 +60,7 @@ This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ```agda module _ - {l : Level} (L : lower-ℝ l) (U : upper-ℝ l) + {l1 l2 : Level} (L : lower-ℝ l1) (U : upper-ℝ l2) where arithmetically-located-lower-upper-ℝ : UU l @@ -82,7 +82,7 @@ located. ```agda module _ - {l : Level} (x : lower-ℝ l) (y : upper-ℝ l) + {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2) where abstract From f462be5d7d0007edf17871bde17dcd75435cb29d Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:32:12 -0800 Subject: [PATCH 69/73] Fix compile --- .../arithmetically-located-dedekind-cuts.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md index c3d4d59716..fa5295f6a6 100644 --- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md +++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md @@ -60,17 +60,17 @@ This follows parts of Section 11 in {{#cite BauerTaylor2009}}. ```agda module _ - {l1 l2 : Level} (L : lower-ℝ l1) (U : upper-ℝ l2) + {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2) where - arithmetically-located-lower-upper-ℝ : UU l + arithmetically-located-lower-upper-ℝ : UU (l1 ⊔ l2) arithmetically-located-lower-upper-ℝ = (ε⁺ : ℚ⁺) → exists ( ℚ × ℚ) ( λ (p , q) → le-ℚ-Prop q (p +ℚ rational-ℚ⁺ ε⁺) ∧ - cut-lower-ℝ L p ∧ - cut-upper-ℝ U q) + cut-lower-ℝ x p ∧ + cut-upper-ℝ y q) ``` ## Properties From 5978e1a566b16e416be7efcee630e639ebadc241 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 13 Feb 2025 16:44:22 -0800 Subject: [PATCH 70/73] Review comments --- src/foundation/propositional-truncations.lagda.md | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index f067b32f78..8580a7744a 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -490,8 +490,7 @@ do where open do-syntax-trunc-Prop motive ``` -Since Agda's `do` syntax desugars to calls to `>>=`, this is simply syntactic -sugar for +Since Agda's `do` syntax desugars to calls to `>>=`, this is syntactic sugar for ```text witness-truncated-prop-P >>= @@ -504,8 +503,8 @@ which, inlining the definition of `>>=`, becomes exactly the chain of To read the `do` syntax, it may help to go through each line: -1. `do` simply indicates that we will be using Agda's syntactic sugar for the - `>>=` function defined in the `do-syntax-trunc-Prop` module. +1. `do` indicates that we will be using Agda's syntactic sugar for the `>>=` + function defined in the `do-syntax-trunc-Prop` module. 1. You can read the `p ← witness-truncated-prop-P` as an _instruction_ saying, "Get the value `p` out of the witness of `trunc-Prop P`." We cannot extract elements out of witnesses of propositionally truncated types, but since we're @@ -513,10 +512,10 @@ To read the `do` syntax, it may help to go through each line: allows us to lift a map from the untruncated type to a map from its truncation. 1. `q ← witness-truncated-prop-Q p` says, "Get the value `q` out of the witness - for the truncation `witness-truncated-prop-Q p`" -- noticing that we can make - use of `p : P` in that line. -1. `witness-motive-P-Q p q` must give us a witness of `motive` -- that is, a - value of type `type-Prop motive` -- from `p` and `q`. + for the truncation `witness-truncated-prop-Q p`" --- noticing that we can + make use of `p : P` in that line. +1. `witness-motive-P-Q p q` must give us a witness of `motive` --- that is, a + value of type `type-Prop motive` --- from `p` and `q`. 1. `where open do-syntax-trunc-Prop motive` is required to allow us to use the `do` syntax. From e981a15b8285ee4130b013f3f0a46c0bb542f730 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 14 Feb 2025 11:50:03 -0800 Subject: [PATCH 71/73] Progress --- .../addition-lower-dedekind-real-numbers.lagda.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 0073594d5b..36113fa021 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -207,3 +207,9 @@ module _ ( cut-lower-ℝ y) ( cut-lower-ℝ z)) ``` + +### Unit laws for the addition of lower Dedekind real numbers + +```agda + +``` From d90e459a320fef8aa2e97962d8a5b781d5d78159 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 14 Feb 2025 13:32:26 -0800 Subject: [PATCH 72/73] Unit laws and simplifications --- ...ition-lower-dedekind-real-numbers.lagda.md | 194 ++++++++++-------- ...ition-upper-dedekind-real-numbers.lagda.md | 180 +++++++++------- .../lower-dedekind-real-numbers.lagda.md | 17 ++ .../upper-dedekind-real-numbers.lagda.md | 19 ++ 4 files changed, 250 insertions(+), 160 deletions(-) diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md index 36113fa021..652c87812c 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -24,6 +24,7 @@ open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.propositional-truncations open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels @@ -35,6 +36,7 @@ open import group-theory.minkowski-multiplication-commutative-monoids open import logic.functoriality-existential-quantification open import real-numbers.lower-dedekind-real-numbers +open import real-numbers.rational-lower-dedekind-real-numbers ``` @@ -78,89 +80,67 @@ module _ (q : ℚ) → is-in-cut-add-lower-ℝ q ↔ exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r) - pr1 (is-rounded-cut-add-lower-ℝ q) = - elim-exists - ( ∃ ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r)) - ( λ (lx , ly) (lx @@ -78,81 +78,67 @@ module _ (q : ℚ) → is-in-cut-add-upper-ℝ q ↔ exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p) - pr1 (is-rounded-cut-add-upper-ℝ q) = - elim-exists - ( ∃ ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p)) - ( λ (ux , uy) (xImports ```agda +open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -122,6 +126,19 @@ module _ ( intro-exists q (pImports ```agda +open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -122,6 +124,23 @@ module _ ( intro-exists p (p Date: Fri, 14 Feb 2025 13:38:01 -0800 Subject: [PATCH 73/73] make pre-commit --- src/real-numbers.lagda.md | 2 +- src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 840e17a3da..24d0f66b34 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -5,9 +5,9 @@ ```agda module real-numbers where -open import real-numbers.apartness-real-numbers public open import real-numbers.addition-lower-dedekind-real-numbers public open import real-numbers.addition-upper-dedekind-real-numbers public +open import real-numbers.apartness-real-numbers public open import real-numbers.arithmetically-located-dedekind-cuts public open import real-numbers.dedekind-real-numbers public open import real-numbers.inequality-lower-dedekind-real-numbers public diff --git a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md index 0941ed1a99..33dd0ded7d 100644 --- a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md @@ -33,8 +33,8 @@ open import group-theory.abelian-groups open import group-theory.groups open import group-theory.minkowski-multiplication-commutative-monoids -open import real-numbers.upper-dedekind-real-numbers open import real-numbers.rational-upper-dedekind-real-numbers +open import real-numbers.upper-dedekind-real-numbers ```