-
Notifications
You must be signed in to change notification settings - Fork 72
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This PR introduces the cannonical map from `ℚ` to `ℝ` as well as a characterisation of its image in terms of Dedekind cuts. To do so, I had to introduce a few properties on (strict) inequalities on the rational numbers, integer fractions and integers. - modified: elementary-number-theory/addition-integers.lagda.md - the sum of a nonnegative and a positive integer is positive - new file: elementary-number-theory/cross-mul-diff-integer-fractions.lagda.md - define the cross-multiplication difference of two integer fractions - computing properties (useful to work with comparison of integer fractions) - modified: elementary-number-theory/inequality-integer-fractions.lagda.md - generic properties of the (strict) order on integer fractions (asymmetricity, transitivity, etc.) - helper functions to construct inequal fractions - modified: elementary-number-theory/inequality-integers.lagda.md - fix the definition of `le-ℤ` - generic properties of `le-ℤ` - preservation/reflection properties of `le-ℤ` w.r.t `add-ℤ` - modified: elementary-number-theory/inequality-rational-numbers.lagda.md - generic properties of the (strict) order on rational numbers - compatibility between the orderings on integer fractions and rational numbers - no lower/upper bounds, decidability, trichotomy principle - density and of strict inequality on rational numbers - modified: elementary-number-theory/integers.lagda.md - decide positivity of integers - new file: elementary-number-theory/mediant-integer-fractions.lagda.md - define the mediant of two integer fractions - the mediant preserves cross-multiplication difference - modified: elementary-number-theory/multiplication-integers.lagda.md - multiplication by a positive integer preserves strict ordering - modified: elementary-number-theory/rational-numbers.lagda.md - accessor functions for rational numbers - define the mediant of two rational numbers - modified: real-numbers/dedekind-real-numbers.lagda.md - contructor and accessor functions for real numbers - properties of Dedekind cuts - real numbers are determined by their lower/upper cuts - new file: real-numbers/rational-real-numbers.lagda.md - define the Dedekind cut given by a rational number - define the subtype of rational real numbers - `ℚ` embeds in `ℝ` as the subtype of rational real numbers
- Loading branch information
Showing
13 changed files
with
1,610 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
219 changes: 219 additions & 0 deletions
219
...entary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,219 @@ | ||
| # The cross-multiplication difference of two integer fractions | ||
|
|
||
| ```agda | ||
| module elementary-number-theory.cross-multiplication-difference-integer-fractions where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import elementary-number-theory.addition-integers | ||
| open import elementary-number-theory.difference-integers | ||
| open import elementary-number-theory.integer-fractions | ||
| open import elementary-number-theory.integers | ||
| open import elementary-number-theory.multiplication-integers | ||
|
|
||
| open import foundation.action-on-identifications-functions | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.identity-types | ||
| open import foundation.negation | ||
| open import foundation.propositions | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| The | ||
| {{#concept "cross-multiplication difference" Agda=cross-mul-diff-fraction-ℤ}} of | ||
| two [integer fractions](elementary-number-theory.integer-fractions.md) `a/b` and | ||
| `c/d` is the [difference](elementary-number-theory.difference-integers.md) of | ||
| the [products](elementary-number-theory.multiplication-integers.md) of the | ||
| numerator of each fraction with the denominator of the other: `c * b - a * d`. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### The cross-multiplication difference of two fractions | ||
|
|
||
| ```agda | ||
| cross-mul-diff-fraction-ℤ : fraction-ℤ → fraction-ℤ → ℤ | ||
| cross-mul-diff-fraction-ℤ x y = | ||
| diff-ℤ | ||
| ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) | ||
| ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### Swapping the fractions changes the sign of the cross-multiplication difference | ||
|
|
||
| ```agda | ||
| skew-commutative-cross-mul-diff-fraction-ℤ : | ||
| (x y : fraction-ℤ) → | ||
| Id | ||
| ( neg-ℤ (cross-mul-diff-fraction-ℤ x y)) | ||
| ( cross-mul-diff-fraction-ℤ y x) | ||
| skew-commutative-cross-mul-diff-fraction-ℤ x y = | ||
| distributive-neg-diff-ℤ | ||
| ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) | ||
| ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) | ||
| ``` | ||
|
|
||
| ### Two fractions are similar when their cross-multiplication difference is zero | ||
|
|
||
| ```agda | ||
| module _ | ||
| (x y : fraction-ℤ) | ||
| where | ||
|
|
||
| is-zero-cross-mul-diff-sim-fraction-ℤ : | ||
| sim-fraction-ℤ x y → | ||
| is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) | ||
| is-zero-cross-mul-diff-sim-fraction-ℤ H = | ||
| is-zero-diff-ℤ (inv H) | ||
|
|
||
| sim-is-zero-coss-mul-diff-fraction-ℤ : | ||
| is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) → | ||
| sim-fraction-ℤ x y | ||
| sim-is-zero-coss-mul-diff-fraction-ℤ H = inv (eq-diff-ℤ H) | ||
| ``` | ||
|
|
||
| ## The transitive-additive property for the cross-multiplication difference | ||
|
|
||
| Given three fractions `a/b`, `x/y` and `m/n`, the pairwise cross-multiplication | ||
| differences satisfy a transitive-additive property: | ||
|
|
||
| ```text | ||
| y * (m * b - a * n) = b * (m * y - x * n) + n * (x * b - a * y) | ||
| ``` | ||
|
|
||
| ```agda | ||
| lemma-add-cross-mul-diff-fraction-ℤ : | ||
| (p q r : fraction-ℤ) → | ||
| Id | ||
| ( add-ℤ | ||
| ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r) | ||
| ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q)) | ||
| ( denominator-fraction-ℤ q *ℤ cross-mul-diff-fraction-ℤ p r) | ||
| lemma-add-cross-mul-diff-fraction-ℤ | ||
| (np , dp , hp) | ||
| (nq , dq , hq) | ||
| (nr , dr , hr) = | ||
| equational-reasoning | ||
| add-ℤ | ||
| (dp *ℤ (nr *ℤ dq -ℤ nq *ℤ dr)) | ||
| (dr *ℤ (nq *ℤ dp -ℤ np *ℤ dq)) | ||
| ＝ add-ℤ | ||
| (dp *ℤ (nr *ℤ dq) -ℤ dp *ℤ (nq *ℤ dr)) | ||
| (dr *ℤ (nq *ℤ dp) -ℤ dr *ℤ (np *ℤ dq)) | ||
| by | ||
| ap-add-ℤ | ||
| ( inv (linear-diff-left-mul-ℤ dp (nr *ℤ dq) (nq *ℤ dr))) | ||
| ( inv (linear-diff-left-mul-ℤ dr (nq *ℤ dp) (np *ℤ dq))) | ||
| ＝ diff-ℤ | ||
| (dp *ℤ (nr *ℤ dq) +ℤ dr *ℤ (nq *ℤ dp)) | ||
| (dp *ℤ (nq *ℤ dr) +ℤ dr *ℤ (np *ℤ dq)) | ||
| by | ||
| interchange-law-add-diff-ℤ | ||
| ( mul-ℤ dp ( mul-ℤ nr dq)) | ||
| ( mul-ℤ dp ( mul-ℤ nq dr)) | ||
| ( mul-ℤ dr ( mul-ℤ nq dp)) | ||
| ( mul-ℤ dr ( mul-ℤ np dq)) | ||
| ＝ diff-ℤ | ||
| (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)) | ||
| (dr *ℤ (nq *ℤ dp) +ℤ dq *ℤ (np *ℤ dr)) | ||
| by | ||
| ap-diff-ℤ | ||
| ( ap-add-ℤ | ||
| ( lemma-interchange-mul-ℤ dp nr dq) | ||
| ( refl)) | ||
| ( ap-add-ℤ | ||
| ( lemma-interchange-mul-ℤ dp nq dr) | ||
| ( lemma-interchange-mul-ℤ dr np dq)) | ||
| ＝ diff-ℤ | ||
| (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)) | ||
| ((dq *ℤ (np *ℤ dr)) +ℤ (dr *ℤ (nq *ℤ dp))) | ||
| by | ||
| ap | ||
| ( diff-ℤ (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))) | ||
| ( commutative-add-ℤ (dr *ℤ (nq *ℤ dp)) (dq *ℤ (np *ℤ dr))) | ||
| ＝ (dq *ℤ (nr *ℤ dp)) -ℤ (dq *ℤ (np *ℤ dr)) | ||
| by | ||
| right-translation-diff-ℤ | ||
| (dq *ℤ (nr *ℤ dp)) | ||
| (dq *ℤ (np *ℤ dr)) | ||
| (dr *ℤ (nq *ℤ dp)) | ||
| ＝ dq *ℤ (nr *ℤ dp -ℤ np *ℤ dr) | ||
| by linear-diff-left-mul-ℤ dq (nr *ℤ dp) (np *ℤ dr) | ||
| where | ||
| lemma-interchange-mul-ℤ : (a b c : ℤ) → (a *ℤ (b *ℤ c)) ＝ (c *ℤ (b *ℤ a)) | ||
| lemma-interchange-mul-ℤ a b c = | ||
| inv (associative-mul-ℤ a b c) ∙ | ||
| ap (mul-ℤ' c) (commutative-mul-ℤ a b) ∙ | ||
| commutative-mul-ℤ (b *ℤ a) c | ||
|
|
||
| lemma-left-sim-cross-mul-diff-fraction-ℤ : | ||
| (a a' b : fraction-ℤ) → | ||
| sim-fraction-ℤ a a' → | ||
| Id | ||
| ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b) | ||
| ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| lemma-left-sim-cross-mul-diff-fraction-ℤ a a' b H = | ||
| equational-reasoning | ||
| ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b) | ||
| ＝ ( add-ℤ | ||
| ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a' a)) | ||
| by inv (lemma-add-cross-mul-diff-fraction-ℤ a' a b) | ||
| ＝ ( add-ℤ | ||
| ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| ( zero-ℤ)) | ||
| by | ||
| ap | ||
| ( add-ℤ | ||
| ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)) | ||
| ( ( ap | ||
| ( mul-ℤ (denominator-fraction-ℤ b)) | ||
| ( is-zero-cross-mul-diff-sim-fraction-ℤ a' a H')) ∙ | ||
| ( right-zero-law-mul-ℤ (denominator-fraction-ℤ b))) | ||
| ＝ denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b | ||
| by | ||
| right-unit-law-add-ℤ | ||
| ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| where | ||
| H' : sim-fraction-ℤ a' a | ||
| H' = symmetric-sim-fraction-ℤ a a' H | ||
|
|
||
| lemma-right-sim-cross-mul-diff-fraction-ℤ : | ||
| (a b b' : fraction-ℤ) → | ||
| sim-fraction-ℤ b b' → | ||
| Id | ||
| ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b') | ||
| ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| lemma-right-sim-cross-mul-diff-fraction-ℤ a b b' H = | ||
| equational-reasoning | ||
| ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b') | ||
| ＝ ( add-ℤ | ||
| ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ b b') | ||
| ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) | ||
| by inv (lemma-add-cross-mul-diff-fraction-ℤ a b b') | ||
| ＝ ( add-ℤ | ||
| ( zero-ℤ) | ||
| ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) | ||
| by | ||
| ap | ||
| ( add-ℤ' (denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) | ||
| ( ( ap | ||
| ( mul-ℤ (denominator-fraction-ℤ a)) | ||
| ( is-zero-cross-mul-diff-sim-fraction-ℤ b b' H)) ∙ | ||
| ( right-zero-law-mul-ℤ (denominator-fraction-ℤ a))) | ||
| ＝ denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b | ||
| by | ||
| left-unit-law-add-ℤ | ||
| ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b) | ||
| ``` | ||
|
|
||
| ## External links | ||
|
|
||
| - [Cross-multiplication](https://en.wikipedia.org/wiki/Cross-multiplication) at | ||
| Wikipedia |
Oops, something went wrong.