Skip to content

Commit 04dd8a8

Browse files
lowasserlowasser
authored
Addition for lower and upper Dedekind reals (#1342)
Depends on #1339, but adds ~500LOC beyond that, and seems like a reasonable sub-PR to break away from #1336 .
1 parent 0af5657 commit 04dd8a8

6 files changed

+590
-0
lines changed

‎src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md

+5
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ open import foundation.unital-binary-operations
1919
open import foundation.universe-levels
2020
2121
open import group-theory.abelian-groups
22+
open import group-theory.commutative-monoids
2223
open import group-theory.groups
2324
open import group-theory.monoids
2425
open import group-theory.semigroups
@@ -65,6 +66,10 @@ pr2 (pr2 (pr2 (pr2 group-add-ℚ))) = right-inverse-law-add-ℚ
6566
### The additive group of rational numbers is commutative
6667

6768
```agda
69+
commutative-monoid-add-ℚ : Commutative-Monoid lzero
70+
pr1 commutative-monoid-add-ℚ = monoid-add-ℚ
71+
pr2 commutative-monoid-add-ℚ = commutative-add-ℚ
72+
6873
abelian-group-add-ℚ : Ab lzero
6974
pr1 abelian-group-add-ℚ = group-add-ℚ
7075
pr2 abelian-group-add-ℚ = commutative-add-ℚ

‎src/real-numbers.lagda.md

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55
```agda
66
module real-numbers where
77
8+
open import real-numbers.addition-lower-dedekind-real-numbers public
9+
open import real-numbers.addition-upper-dedekind-real-numbers public
810
open import real-numbers.apartness-real-numbers public
911
open import real-numbers.arithmetically-located-dedekind-cuts public
1012
open import real-numbers.dedekind-real-numbers public

‎src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md

+279
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,279 @@
1+
# Addition of lower Dedekind real numbers
2+
3+
```agda
4+
{-# OPTIONS --lossy-unification #-}
5+
6+
module real-numbers.addition-lower-dedekind-real-numbers where
7+
```
8+
9+
<details><summary>Imports</summary>
10+
11+
```agda
12+
open import elementary-number-theory.addition-rational-numbers
13+
open import elementary-number-theory.additive-group-of-rational-numbers
14+
open import elementary-number-theory.difference-rational-numbers
15+
open import elementary-number-theory.positive-rational-numbers
16+
open import elementary-number-theory.rational-numbers
17+
open import elementary-number-theory.strict-inequality-rational-numbers
18+
19+
open import foundation.action-on-identifications-functions
20+
open import foundation.binary-transport
21+
open import foundation.cartesian-product-types
22+
open import foundation.conjunction
23+
open import foundation.dependent-pair-types
24+
open import foundation.existential-quantification
25+
open import foundation.identity-types
26+
open import foundation.logical-equivalences
27+
open import foundation.propositional-truncations
28+
open import foundation.sets
29+
open import foundation.subtypes
30+
open import foundation.transport-along-identifications
31+
open import foundation.universe-levels
32+
33+
open import group-theory.abelian-groups
34+
open import group-theory.commutative-monoids
35+
open import group-theory.groups
36+
open import group-theory.minkowski-multiplication-commutative-monoids
37+
open import group-theory.monoids
38+
open import group-theory.semigroups
39+
40+
open import logic.functoriality-existential-quantification
41+
42+
open import real-numbers.lower-dedekind-real-numbers
43+
open import real-numbers.rational-lower-dedekind-real-numbers
44+
```
45+
46+
</details>
47+
48+
## Idea
49+
50+
We introduce
51+
{{#concept "addition" Disambiguation="lower Dedekind real numbers" Agda=add-lower-ℝ}}
52+
of two
53+
[lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md) `x`
54+
and `y`, which is a lower Dedekind real number with cut equal to the
55+
[Minkowski sum](group-theory.minkowski-multiplication-commutative-monoids.md) of
56+
the cuts of `x` and `y`.
57+
58+
```agda
59+
module _
60+
{l1 l2 : Level}
61+
(x : lower-ℝ l1)
62+
(y : lower-ℝ l2)
63+
where
64+
65+
cut-add-lower-ℝ : subtype (l1 ⊔ l2) ℚ
66+
cut-add-lower-ℝ =
67+
minkowski-mul-Commutative-Monoid
68+
( commutative-monoid-add-ℚ)
69+
( cut-lower-ℝ x)
70+
( cut-lower-ℝ y)
71+
72+
is-in-cut-add-lower-ℝ : ℚ → UU (l1 ⊔ l2)
73+
is-in-cut-add-lower-ℝ = is-in-subtype cut-add-lower-ℝ
74+
75+
abstract
76+
is-inhabited-cut-add-lower-ℝ : exists ℚ cut-add-lower-ℝ
77+
is-inhabited-cut-add-lower-ℝ =
78+
minkowski-mul-inhabited-is-inhabited-Commutative-Monoid
79+
( commutative-monoid-add-ℚ)
80+
( cut-lower-ℝ x)
81+
( cut-lower-ℝ y)
82+
( is-inhabited-cut-lower-ℝ x)
83+
( is-inhabited-cut-lower-ℝ y)
84+
85+
forward-implication-is-rounded-cut-add-lower-ℝ :
86+
(q : ℚ) → is-in-cut-add-lower-ℝ q →
87+
exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r)
88+
forward-implication-is-rounded-cut-add-lower-ℝ q q<x+y =
89+
do
90+
((lx , ly) , (lx<x , ly<y , q=lx+ly)) ← q<x+y
91+
(lx' , lx<lx' , lx'<x) ←
92+
forward-implication (is-rounded-cut-lower-ℝ x lx) lx<x
93+
(ly' , ly<ly' , ly'<y) ←
94+
forward-implication (is-rounded-cut-lower-ℝ y ly) ly<y
95+
intro-exists
96+
( lx' +ℚ ly')
97+
( inv-tr
98+
( λ p → le-ℚ p (lx' +ℚ ly'))
99+
( q=lx+ly)
100+
( preserves-le-add-ℚ {lx} {lx'} {ly} {ly'} lx<lx' ly<ly') ,
101+
intro-exists (lx' , ly') (lx'<x , ly'<y , refl))
102+
where
103+
open
104+
do-syntax-trunc-Prop (∃ ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r))
105+
106+
backward-implication-is-rounded-cut-add-lower-ℝ :
107+
(q : ℚ) → exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r) →
108+
is-in-cut-add-lower-ℝ q
109+
backward-implication-is-rounded-cut-add-lower-ℝ q ∃r =
110+
do
111+
(r , q<r , r<x+y) ← ∃r
112+
((rx , ry) , (rx<x , ry<y , r=rx+ry)) ← r<x+y
113+
let
114+
r-q⁺ = positive-diff-le-ℚ q r q<r
115+
ε⁺@(ε , _) = mediant-zero-ℚ⁺ r-q⁺
116+
intro-exists
117+
( rx -ℚ ε , q -ℚ (rx -ℚ ε))
118+
( is-in-cut-diff-rational-ℚ⁺-lower-ℝ x rx ε⁺ rx<x ,
119+
is-in-cut-le-ℚ-lower-ℝ
120+
( y)
121+
( q -ℚ (rx -ℚ ε))
122+
( ry)
123+
( binary-tr
124+
( le-ℚ)
125+
( equational-reasoning
126+
(q -ℚ rx) +ℚ ε
127+
＝ q +ℚ (neg-ℚ rx +ℚ ε)
128+
by associative-add-ℚ q (neg-ℚ rx) ε
129+
＝ q +ℚ (ε -ℚ rx)
130+
by ap (q +ℚ_) (commutative-add-ℚ (neg-ℚ rx) ε)
131+
＝ q -ℚ (rx -ℚ ε)
132+
by ap (q +ℚ_) (inv (distributive-neg-diff-ℚ rx ε)))
133+
( equational-reasoning
134+
(q -ℚ rx) +ℚ (r -ℚ q)
135+
＝ (q -ℚ rx) -ℚ (q -ℚ r)
136+
by ap ((q -ℚ rx) +ℚ_) (inv (distributive-neg-diff-ℚ q r))
137+
＝ neg-ℚ rx -ℚ neg-ℚ r
138+
by left-translation-diff-ℚ (neg-ℚ rx) (neg-ℚ r) q
139+
＝ neg-ℚ rx +ℚ (rx +ℚ ry)
140+
by ap (neg-ℚ rx +ℚ_) (neg-neg-ℚ r ∙ r=rx+ry)
141+
＝ ry
142+
by is-retraction-left-div-Group group-add-ℚ rx ry)
143+
( preserves-le-right-add-ℚ
144+
( q -ℚ rx)
145+
( ε)
146+
( r -ℚ q)
147+
( le-mediant-zero-ℚ⁺ r-q⁺)))
148+
( ry<y) ,
149+
inv ( is-identity-right-conjugation-add-ℚ (rx -ℚ ε) q))
150+
where open do-syntax-trunc-Prop (cut-add-lower-ℝ q)
151+
152+
is-rounded-cut-add-lower-ℝ :
153+
(q : ℚ) →
154+
is-in-cut-add-lower-ℝ q ↔
155+
exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r)
156+
is-rounded-cut-add-lower-ℝ q =
157+
forward-implication-is-rounded-cut-add-lower-ℝ q ,
158+
backward-implication-is-rounded-cut-add-lower-ℝ q
159+
160+
add-lower-ℝ : lower-ℝ (l1 ⊔ l2)
161+
pr1 add-lower-ℝ = cut-add-lower-ℝ
162+
pr1 (pr2 add-lower-ℝ) = is-inhabited-cut-add-lower-ℝ
163+
pr2 (pr2 add-lower-ℝ) = is-rounded-cut-add-lower-ℝ
164+
```
165+
166+
## Properties
167+
168+
### Addition of lower Dedekind real numbers is commutative
169+
170+
```agda
171+
module _
172+
{l1 l2 : Level} (x : lower-ℝ l1) (y : lower-ℝ l2)
173+
where
174+
175+
abstract
176+
commutative-add-lower-ℝ : add-lower-ℝ x y ＝ add-lower-ℝ y x
177+
commutative-add-lower-ℝ =
178+
eq-eq-cut-lower-ℝ
179+
( add-lower-ℝ x y)
180+
( add-lower-ℝ y x)
181+
( commutative-minkowski-mul-Commutative-Monoid
182+
( commutative-monoid-add-ℚ)
183+
( cut-lower-ℝ x)
184+
( cut-lower-ℝ y))
185+
```
186+
187+
### Addition of lower Dedekind real numbers is associative
188+
189+
```agda
190+
module _
191+
{l1 l2 l3 : Level} (x : lower-ℝ l1) (y : lower-ℝ l2) (z : lower-ℝ l3)
192+
where
193+
194+
abstract
195+
associative-add-lower-ℝ :
196+
add-lower-ℝ (add-lower-ℝ x y) z ＝ add-lower-ℝ x (add-lower-ℝ y z)
197+
associative-add-lower-ℝ =
198+
eq-eq-cut-lower-ℝ
199+
( add-lower-ℝ (add-lower-ℝ x y) z)
200+
( add-lower-ℝ x (add-lower-ℝ y z))
201+
( associative-minkowski-mul-Commutative-Monoid
202+
( commutative-monoid-add-ℚ)
203+
( cut-lower-ℝ x)
204+
( cut-lower-ℝ y)
205+
( cut-lower-ℝ z))
206+
```
207+
208+
### Unit laws for the addition of lower Dedekind real numbers
209+
210+
```agda
211+
module _
212+
{l : Level} (x : lower-ℝ l)
213+
where
214+
215+
abstract
216+
right-unit-law-add-lower-ℝ : add-lower-ℝ x (lower-real-ℚ zero-ℚ) ＝ x
217+
right-unit-law-add-lower-ℝ =
218+
eq-sim-cut-lower-ℝ
219+
( add-lower-ℝ x (lower-real-ℚ zero-ℚ))
220+
( x)
221+
( (λ r →
222+
elim-exists
223+
( cut-lower-ℝ x r)
224+
( λ (p , q) (p<x , q<0 , r=p+q) →
225+
tr
226+
( is-in-cut-lower-ℝ x)
227+
( ap (p +ℚ_) (neg-neg-ℚ q) ∙ inv r=p+q)
228+
( is-in-cut-diff-rational-ℚ⁺-lower-ℝ
229+
( x)
230+
( p)
231+
( neg-ℚ q ,
232+
is-positive-le-zero-ℚ (neg-ℚ q) (neg-le-ℚ q zero-ℚ q<0))
233+
( p<x)))) ,
234+
(λ p p<x →
235+
elim-exists
236+
( cut-add-lower-ℝ x (lower-real-ℚ zero-ℚ) p)
237+
( λ q (p<q , q<x) →
238+
intro-exists
239+
( q , p -ℚ q)
240+
( q<x ,
241+
tr
242+
( λ r → le-ℚ r zero-ℚ)
243+
( distributive-neg-diff-ℚ q p)
244+
( neg-le-ℚ
245+
( zero-ℚ)
246+
( q -ℚ p)
247+
( backward-implication
248+
( iff-translate-diff-le-zero-ℚ p q)
249+
( p<q))) ,
250+
inv (is-identity-right-conjugation-add-ℚ q p)))
251+
( forward-implication (is-rounded-cut-lower-ℝ x p) p<x)))
252+
253+
left-unit-law-add-lower-ℝ : add-lower-ℝ (lower-real-ℚ zero-ℚ) x ＝ x
254+
left-unit-law-add-lower-ℝ =
255+
commutative-add-lower-ℝ (lower-real-ℚ zero-ℚ) x ∙ right-unit-law-add-lower-ℝ
256+
```
257+
258+
### The commutative monoid of lower Dedekind real numbers
259+
260+
```agda
261+
semigroup-add-lower-ℝ-lzero : Semigroup (lsuc lzero)
262+
semigroup-add-lower-ℝ-lzero =
263+
(lower-ℝ lzero , is-set-lower-ℝ lzero) ,
264+
add-lower-ℝ ,
265+
associative-add-lower-ℝ
266+
267+
monoid-lower-ℝ-lzero : Monoid (lsuc lzero)
268+
monoid-lower-ℝ-lzero =
269+
semigroup-add-lower-ℝ-lzero ,
270+
lower-real-ℚ zero-ℚ ,
271+
left-unit-law-add-lower-ℝ ,
272+
right-unit-law-add-lower-ℝ
273+
274+
commutative-monoid-add-lower-ℝ-lzero :
275+
Commutative-Monoid (lsuc lzero)
276+
commutative-monoid-add-lower-ℝ-lzero =
277+
monoid-lower-ℝ-lzero ,
278+
commutative-add-lower-ℝ
279+
```

0 commit comments

Comments
 (0)