From 54da0617a511aab4529a12bee360d8df696172bc Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 10 Oct 2025 15:54:25 -0700 Subject: [PATCH 01/22] Reorganize signed arithmetic on rational numbers --- src/elementary-number-theory.lagda.md | 2 + ...closed-intervals-rational-numbers.lagda.md | 2 +- .../absolute-value-rational-numbers.lagda.md | 255 ++++++++---------- ...tion-nonnegative-rational-numbers.lagda.md | 10 +- ...ddition-positive-rational-numbers.lagda.md | 14 +- .../addition-rational-numbers.lagda.md | 5 +- ...roperty-positive-rational-numbers.lagda.md | 4 +- ...imedean-property-rational-numbers.lagda.md | 8 +- .../difference-rational-numbers.lagda.md | 2 +- .../distance-rational-numbers.lagda.md | 2 +- ...ive-and-negative-rational-numbers.lagda.md | 106 ++++++++ .../inequality-rational-numbers.lagda.md | 11 +- ...imum-nonnegative-rational-numbers.lagda.md | 4 +- ...inima-and-maxima-rational-numbers.lagda.md | 8 +- ...closed-intervals-rational-numbers.lagda.md | 1 + ...closed-intervals-rational-numbers.lagda.md | 6 +- ...ication-negative-rational-numbers.lagda.md | 159 +++++++++++ ...tion-nonnegative-rational-numbers.lagda.md | 48 +++- ...tion-nonpositive-rational-numbers.lagda.md | 14 +- ...ive-and-negative-rational-numbers.lagda.md | 9 +- ...ication-positive-rational-numbers.lagda.md | 12 +- ...icative-group-of-rational-numbers.lagda.md | 4 +- ...closed-intervals-rational-numbers.lagda.md | 6 +- .../negative-rational-numbers.lagda.md | 227 ++++------------ .../nonnegative-rational-numbers.lagda.md | 98 +++---- .../nonpositive-rational-numbers.lagda.md | 55 ++-- ...ive-and-negative-rational-numbers.lagda.md | 195 ++++++++++---- .../positive-rational-numbers.lagda.md | 104 +++---- .../rational-numbers.lagda.md | 21 +- .../squares-rational-numbers.lagda.md | 19 +- ...lity-nonnegative-rational-numbers.lagda.md | 10 - ...quality-positive-rational-numbers.lagda.md | 5 +- ...trict-inequality-rational-numbers.lagda.md | 7 +- ...at-bounded-distance-metric-spaces.lagda.md | 8 +- .../located-metric-spaces.lagda.md | 4 +- .../metric-space-of-rational-numbers.lagda.md | 8 +- ...onal-sequences-approximating-zero.lagda.md | 1 + src/order-theory.lagda.md | 1 + .../order-preserving-maps-posets.lagda.md | 6 +- ...rder-preserving-maps-total-orders.lagda.md | 193 +++++++++++++ ...ition-lower-dedekind-real-numbers.lagda.md | 16 +- ...ition-upper-dedekind-real-numbers.lagda.md | 4 +- ...thmetically-located-dedekind-cuts.lagda.md | 6 +- .../multiplication-real-numbers.lagda.md | 1 + ...lower-upper-dedekind-real-numbers.lagda.md | 16 +- .../negation-real-numbers.lagda.md | 2 +- .../nonnegative-real-numbers.lagda.md | 5 +- .../positive-real-numbers.lagda.md | 16 +- .../strict-inequality-real-numbers.lagda.md | 2 +- 49 files changed, 1052 insertions(+), 670 deletions(-) create mode 100644 src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/multiplication-negative-rational-numbers.lagda.md create mode 100644 src/order-theory/order-preserving-maps-total-orders.lagda.md diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 662f2615dc5..d6d8fc4df2d 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -93,6 +93,7 @@ open import elementary-number-theory.group-of-integers public open import elementary-number-theory.half-integers public open import elementary-number-theory.hardy-ramanujan-number public open import elementary-number-theory.inclusion-natural-numbers-conatural-numbers public +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers public open import elementary-number-theory.inequality-arithmetic-geometric-means-integers public open import elementary-number-theory.inequality-arithmetic-geometric-means-rational-numbers public open import elementary-number-theory.inequality-conatural-numbers public @@ -137,6 +138,7 @@ open import elementary-number-theory.multiplication-integers public open import elementary-number-theory.multiplication-interior-closed-intervals-rational-numbers public open import elementary-number-theory.multiplication-lists-of-natural-numbers public open import elementary-number-theory.multiplication-natural-numbers public +open import elementary-number-theory.multiplication-negative-rational-numbers public open import elementary-number-theory.multiplication-nonnegative-rational-numbers public open import elementary-number-theory.multiplication-nonpositive-rational-numbers public open import elementary-number-theory.multiplication-positive-and-negative-integers public diff --git a/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md index 21651d39f03..c0568e3e299 100644 --- a/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md @@ -69,7 +69,7 @@ abstract ( r≤0)) ( transitive-leq-ℚ (neg-ℚ r) (neg-ℚ p) (rational-abs-ℚ p) ( neg-leq-abs-ℚ p) - ( neg-leq-ℚ _ _ p≤r)))) + ( neg-leq-ℚ p≤r)))) ( λ 0≤r → transitive-leq-ℚ ( rational-abs-ℚ r) diff --git a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md index 93b5e7586ee..fa1c1a6995c 100644 --- a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md +++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md @@ -12,12 +12,15 @@ module elementary-number-theory.absolute-value-rational-numbers where open import elementary-number-theory.addition-nonnegative-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.multiplication-nonnegative-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.nonpositive-rational-numbers +open import elementary-number-theory.positive-and-negative-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 @@ -48,29 +51,27 @@ its negation. rational-abs-ℚ : ℚ → ℚ rational-abs-ℚ q = max-ℚ q (neg-ℚ q) -opaque - unfolding neg-ℚ - +abstract is-nonnegative-rational-abs-ℚ : (q : ℚ) → is-nonnegative-ℚ (rational-abs-ℚ q) is-nonnegative-rational-abs-ℚ q = rec-coproduct - ( λ 0≤q → + ( λ is-nonpos-q → inv-tr ( is-nonnegative-ℚ) - ( right-leq-left-max-ℚ - ( q) - ( neg-ℚ q) - ( transitive-leq-ℚ (neg-ℚ q) zero-ℚ q 0≤q (neg-leq-ℚ zero-ℚ q 0≤q))) - ( is-nonnegative-leq-zero-ℚ q 0≤q)) - ( λ q≤0 → + ( left-leq-right-max-ℚ _ _ + ( leq-nonpositive-nonnegative-ℚ + ( q , is-nonpos-q) + ( neg-ℚ⁰⁻ (q , is-nonpos-q)))) + ( is-nonnegative-neg-is-nonpositive-ℚ is-nonpos-q)) + ( λ is-nonneg-q → inv-tr ( is-nonnegative-ℚ) - ( left-leq-right-max-ℚ - ( q) - ( neg-ℚ q) - ( transitive-leq-ℚ q zero-ℚ (neg-ℚ q) (neg-leq-ℚ q zero-ℚ q≤0) q≤0)) - ( is-nonnegative-leq-zero-ℚ (neg-ℚ q) (neg-leq-ℚ q zero-ℚ q≤0))) - ( linear-leq-ℚ zero-ℚ q) + ( right-leq-left-max-ℚ _ _ + ( leq-nonpositive-nonnegative-ℚ + ( neg-ℚ⁰⁺ (q , is-nonneg-q)) + ( q , is-nonneg-q))) + ( is-nonneg-q)) + ( is-nonpositive-or-nonnegative-ℚ q) abs-ℚ : ℚ → ℚ⁰⁺ pr1 (abs-ℚ q) = rational-abs-ℚ q @@ -92,41 +93,43 @@ abstract le-abs-le-le-neg-ℚ p q = le-max-le-both-ℚ q p (neg-ℚ p) ``` -### The absolute value of a nonnegative rational number is the number itself +### The absolute value of the negation of `q` is the absolute value of `q` ```agda -opaque - unfolding neg-ℚ +abstract + abs-neg-ℚ : (q : ℚ) → abs-ℚ (neg-ℚ q) = abs-ℚ q + abs-neg-ℚ q = + eq-ℚ⁰⁺ + ( ap (max-ℚ (neg-ℚ q)) (neg-neg-ℚ q) ∙ commutative-max-ℚ _ _) + + rational-abs-neg-ℚ : (q : ℚ) → rational-abs-ℚ (neg-ℚ q) = rational-abs-ℚ q + rational-abs-neg-ℚ q = ap rational-ℚ⁰⁺ (abs-neg-ℚ q) +``` + +### The absolute value of a nonnegative rational number is the number itself +```agda +abstract abs-rational-ℚ⁰⁺ : (q : ℚ⁰⁺) → abs-ℚ (rational-ℚ⁰⁺ q) = q - abs-rational-ℚ⁰⁺ (q , nonneg-q) = + abs-rational-ℚ⁰⁺ q = eq-ℚ⁰⁺ - ( right-leq-left-max-ℚ - ( q) - ( neg-ℚ q) - ( transitive-leq-ℚ - ( neg-ℚ q) - ( zero-ℚ) - ( q) - ( leq-zero-is-nonnegative-ℚ q nonneg-q) - ( neg-leq-ℚ zero-ℚ q (leq-zero-is-nonnegative-ℚ q nonneg-q)))) + ( right-leq-left-max-ℚ _ _ (leq-nonpositive-nonnegative-ℚ (neg-ℚ⁰⁺ q) q)) rational-abs-zero-leq-ℚ : (q : ℚ) → leq-ℚ zero-ℚ q → rational-abs-ℚ q = q rational-abs-zero-leq-ℚ q 0≤q = - ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (q , is-nonnegative-leq-zero-ℚ q 0≤q)) + ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (q , is-nonnegative-leq-zero-ℚ 0≤q)) rational-abs-leq-zero-ℚ : (q : ℚ) → leq-ℚ q zero-ℚ → rational-abs-ℚ q = neg-ℚ q rational-abs-leq-zero-ℚ q q≤0 = - left-leq-right-max-ℚ - ( q) - ( neg-ℚ q) - ( transitive-leq-ℚ - ( q) - ( zero-ℚ) - ( neg-ℚ q) - ( neg-leq-ℚ q zero-ℚ q≤0) - ( q≤0)) + equational-reasoning + rational-abs-ℚ q + = rational-abs-ℚ (neg-ℚ q) + by inv (rational-abs-neg-ℚ q) + = neg-ℚ q + by + ap rational-ℚ⁰⁺ + ( abs-rational-ℚ⁰⁺ (neg-ℚ⁰⁻ (q , is-nonpositive-leq-zero-ℚ q≤0))) ``` ### The absolute value of a positive rational number is the number itself @@ -139,16 +142,6 @@ abstract ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (nonnegative-ℚ⁺ q)) ``` -### The absolute value of the negation of `q` is the absolute value of `q` - -```agda -abstract - abs-neg-ℚ : (q : ℚ) → abs-ℚ (neg-ℚ q) = abs-ℚ q - abs-neg-ℚ q = - eq-ℚ⁰⁺ - ( ap (max-ℚ (neg-ℚ q)) (neg-neg-ℚ q) ∙ commutative-max-ℚ _ _) -``` - ### `q` is less than or equal to `abs-ℚ q` ```agda @@ -163,36 +156,31 @@ abstract ### The absolute value of `q` is zero iff `q` is zero ```agda -opaque - unfolding neg-ℚ - - eq-zero-eq-abs-zero-ℚ : (q : ℚ) → abs-ℚ q = zero-ℚ⁰⁺ → q = zero-ℚ - eq-zero-eq-abs-zero-ℚ q abs=0 = - rec-coproduct - ( λ 0≤q → - antisymmetric-leq-ℚ - ( q) - ( zero-ℚ) - ( tr (leq-ℚ q) (ap rational-ℚ⁰⁺ abs=0) (leq-abs-ℚ q)) 0≤q) - ( λ q≤0 → - antisymmetric-leq-ℚ - ( q) - ( zero-ℚ) - ( q≤0) - ( tr - ( leq-ℚ zero-ℚ) - ( neg-neg-ℚ q) - ( neg-leq-ℚ - ( neg-ℚ q) - ( zero-ℚ) - ( tr - ( leq-ℚ (neg-ℚ q)) - ( ap rational-ℚ⁰⁺ abs=0) - ( neg-leq-abs-ℚ q))))) - ( linear-leq-ℚ zero-ℚ q) +abstract + eq-zero-eq-abs-zero-ℚ : {q : ℚ} → abs-ℚ q = zero-ℚ⁰⁺ → q = zero-ℚ + eq-zero-eq-abs-zero-ℚ {q} abs=0 = + antisymmetric-leq-ℚ + ( q) + ( zero-ℚ) + ( transitive-leq-ℚ + ( q) + ( rational-abs-ℚ q) + ( zero-ℚ) + ( leq-eq-ℚ _ _ (ap rational-ℚ⁰⁺ abs=0)) + ( leq-abs-ℚ q)) + ( binary-tr + ( leq-ℚ) + ( ap (neg-ℚ ∘ rational-ℚ⁰⁺) abs=0 ∙ neg-zero-ℚ) + ( neg-neg-ℚ q) + ( neg-leq-ℚ (neg-leq-abs-ℚ q))) abs-zero-ℚ : abs-ℚ zero-ℚ = zero-ℚ⁰⁺ - abs-zero-ℚ = eq-ℚ⁰⁺ (left-leq-right-max-ℚ _ _ (refl-leq-ℚ zero-ℚ)) + abs-zero-ℚ = + eq-ℚ⁰⁺ + ( equational-reasoning + max-ℚ zero-ℚ (neg-ℚ zero-ℚ) + = max-ℚ zero-ℚ zero-ℚ by ap-max-ℚ refl neg-zero-ℚ + = zero-ℚ by idempotent-max-ℚ zero-ℚ) ``` ### The triangle inequality @@ -236,78 +224,53 @@ abstract ### `|ab| = |a||b|` ```agda -opaque - unfolding neg-ℚ - - abs-left-mul-nonnegative-ℚ : - (q : ℚ) (p : ℚ⁰⁺) → abs-ℚ (rational-ℚ⁰⁺ p *ℚ q) = p *ℚ⁰⁺ abs-ℚ q - abs-left-mul-nonnegative-ℚ q p⁰⁺@(p , nonneg-p) with linear-leq-ℚ zero-ℚ q - ... | inl 0≤q = - eq-ℚ⁰⁺ - ( equational-reasoning - rational-abs-ℚ (p *ℚ q) - = p *ℚ q - by - ap - ( rational-ℚ⁰⁺) - ( abs-rational-ℚ⁰⁺ - ( p⁰⁺ *ℚ⁰⁺ (q , is-nonnegative-leq-zero-ℚ q 0≤q))) - = p *ℚ rational-abs-ℚ q - by ap (p *ℚ_) (inv (rational-abs-zero-leq-ℚ q 0≤q))) - ... | inr q≤0 = - eq-ℚ⁰⁺ - ( equational-reasoning - rational-abs-ℚ (p *ℚ q) - = rational-abs-ℚ (neg-ℚ (p *ℚ q)) - by ap rational-ℚ⁰⁺ (inv (abs-neg-ℚ (p *ℚ q))) - = rational-abs-ℚ (p *ℚ neg-ℚ q) - by ap rational-abs-ℚ (inv (right-negative-law-mul-ℚ p q)) - = p *ℚ neg-ℚ q - by - ap - ( rational-ℚ⁰⁺) - ( abs-rational-ℚ⁰⁺ - ( p⁰⁺ *ℚ⁰⁺ - ( neg-ℚ q , - is-nonnegative-leq-zero-ℚ - ( neg-ℚ q) - ( neg-leq-ℚ q zero-ℚ q≤0)))) - = p *ℚ rational-abs-ℚ q - by ap (p *ℚ_) (inv (rational-abs-leq-zero-ℚ q q≤0))) +abstract + rational-abs-left-mul-nonnegative-ℚ : + (q : ℚ) (p : ℚ⁰⁺) → + rational-abs-ℚ (rational-ℚ⁰⁺ p *ℚ q) = rational-ℚ⁰⁺ p *ℚ rational-abs-ℚ q + rational-abs-left-mul-nonnegative-ℚ q p⁰⁺@(p , _) = + equational-reasoning + rational-abs-ℚ (p *ℚ q) + = max-ℚ (p *ℚ q) (p *ℚ neg-ℚ q) + by ap-max-ℚ refl (inv (right-negative-law-mul-ℚ p q)) + = p *ℚ rational-abs-ℚ q + by inv (left-distributive-mul-max-ℚ⁰⁺ p⁰⁺ _ _) abs-mul-ℚ : (p q : ℚ) → abs-ℚ (p *ℚ q) = abs-ℚ p *ℚ⁰⁺ abs-ℚ q - abs-mul-ℚ p q with linear-leq-ℚ zero-ℚ p - ... | inl 0≤p = + abs-mul-ℚ p q = eq-ℚ⁰⁺ - ( equational-reasoning - rational-abs-ℚ (p *ℚ q) - = p *ℚ rational-abs-ℚ q - by - ap - ( rational-ℚ⁰⁺) - ( abs-left-mul-nonnegative-ℚ - ( q) - ( p , is-nonnegative-leq-zero-ℚ p 0≤p)) - = rational-abs-ℚ p *ℚ rational-abs-ℚ q - by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-zero-leq-ℚ p 0≤p))) - ... | inr p≤0 = - eq-ℚ⁰⁺ - ( equational-reasoning - rational-abs-ℚ (p *ℚ q) - = rational-abs-ℚ (neg-ℚ (p *ℚ q)) - by ap rational-ℚ⁰⁺ (inv (abs-neg-ℚ (p *ℚ q))) - = rational-abs-ℚ (neg-ℚ p *ℚ q) - by ap rational-abs-ℚ (inv (left-negative-law-mul-ℚ p q)) - = neg-ℚ p *ℚ rational-abs-ℚ q - by - ap - ( rational-ℚ⁰⁺) - ( abs-left-mul-nonnegative-ℚ - ( q) - ( neg-ℚ p , - is-nonnegative-leq-zero-ℚ (neg-ℚ p) (neg-leq-ℚ p zero-ℚ p≤0))) - = rational-abs-ℚ p *ℚ rational-abs-ℚ q - by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-leq-zero-ℚ p p≤0))) + ( rec-coproduct + ( λ is-nonpos-p → + equational-reasoning + rational-abs-ℚ (p *ℚ q) + = rational-abs-ℚ (neg-ℚ (p *ℚ q)) + by inv (rational-abs-neg-ℚ _) + = rational-abs-ℚ (neg-ℚ p *ℚ q) + by ap rational-abs-ℚ (inv (left-negative-law-mul-ℚ p q)) + = neg-ℚ p *ℚ rational-abs-ℚ q + by + rational-abs-left-mul-nonnegative-ℚ + ( q) + ( neg-ℚ⁰⁻ (p , is-nonpos-p)) + = rational-abs-ℚ p *ℚ rational-abs-ℚ q + by + ap-mul-ℚ + ( inv + ( rational-abs-leq-zero-ℚ + ( p) + ( leq-zero-is-nonpositive-ℚ is-nonpos-p))) + ( refl)) + ( λ is-nonneg-p → + equational-reasoning + rational-abs-ℚ (p *ℚ q) + = p *ℚ rational-abs-ℚ q + by rational-abs-left-mul-nonnegative-ℚ q (p , is-nonneg-p) + = rational-abs-ℚ p *ℚ rational-abs-ℚ q + by + ap-mul-ℚ + ( inv (ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (p , is-nonneg-p)))) + ( refl)) + ( is-nonpositive-or-nonnegative-ℚ p)) abstract rational-abs-mul-ℚ : diff --git a/src/elementary-number-theory/addition-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/addition-nonnegative-rational-numbers.lagda.md index cf3e298f8bb..fa24223764b 100644 --- a/src/elementary-number-theory/addition-nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-nonnegative-rational-numbers.lagda.md @@ -35,12 +35,12 @@ nonnegative. ```agda opaque - unfolding add-ℚ + unfolding add-ℚ is-nonnegative-ℚ is-nonnegative-add-ℚ : - (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q → + {p q : ℚ} → is-nonnegative-ℚ p → is-nonnegative-ℚ q → is-nonnegative-ℚ (p +ℚ q) - is-nonnegative-add-ℚ p q nonneg-p nonneg-q = + is-nonnegative-add-ℚ {p} {q} nonneg-p nonneg-q = is-nonnegative-rational-fraction-ℤ ( is-nonnegative-add-fraction-ℤ { fraction-ℚ p} @@ -50,7 +50,7 @@ opaque add-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ add-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) = - ( p +ℚ q , is-nonnegative-add-ℚ p q nonneg-p nonneg-q) + ( p +ℚ q , is-nonnegative-add-ℚ nonneg-p nonneg-q) infixl 35 _+ℚ⁰⁺_ _+ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ @@ -73,7 +73,7 @@ abstract ( q) ( zero-ℚ) ( p) - ( leq-zero-is-nonnegative-ℚ p nonneg-p)) + ( leq-zero-is-nonnegative-ℚ nonneg-p)) is-inflationary-map-right-add-rational-ℚ⁰⁺ : (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (_+ℚ rational-ℚ⁰⁺ p) diff --git a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md index 5b5cc12dc1b..85668704afe 100644 --- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md @@ -57,7 +57,7 @@ positive. ```agda opaque - unfolding add-ℚ + unfolding add-ℚ is-positive-ℚ is-positive-add-ℚ : {x y : ℚ} → is-positive-ℚ x → is-positive-ℚ y → is-positive-ℚ (x +ℚ y) @@ -147,9 +147,7 @@ module _ ( rational-ℚ⁺ x) ( zero-ℚ) ( rational-ℚ⁺ y) - ( le-zero-is-positive-ℚ - ( rational-ℚ⁺ y) - ( is-positive-rational-ℚ⁺ y))) + ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ y))) le-right-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y) le-right-add-ℚ⁺ = @@ -160,9 +158,7 @@ module _ ( rational-ℚ⁺ y) ( zero-ℚ) ( rational-ℚ⁺ x) - ( le-zero-is-positive-ℚ - ( rational-ℚ⁺ x) - ( is-positive-rational-ℚ⁺ x))) + ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ x))) ``` ### The positive difference of strictly inequal positive rational numbers @@ -268,9 +264,7 @@ abstract ( x) ( zero-ℚ) ( rational-ℚ⁺ d) - ( le-zero-is-positive-ℚ - ( rational-ℚ⁺ d) - ( is-positive-rational-ℚ⁺ d))) + ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ d))) le-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x (x +ℚ (rational-ℚ⁺ d)) le-right-add-rational-ℚ⁺ x d = diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md index 8d887c25a69..0603a977979 100644 --- a/src/elementary-number-theory/addition-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md @@ -154,8 +154,7 @@ abstract ```agda opaque - unfolding add-ℚ - unfolding neg-ℚ + unfolding add-ℚ neg-ℚ left-inverse-law-add-ℚ : (x : ℚ) → (neg-ℚ x) +ℚ x = zero-ℚ left-inverse-law-add-ℚ x = @@ -199,7 +198,7 @@ opaque distributive-neg-add-ℚ : (x y : ℚ) → neg-ℚ (x +ℚ y) = neg-ℚ x +ℚ neg-ℚ y distributive-neg-add-ℚ (x , dxp) (y , dyp) = - ( inv (preserves-neg-rational-fraction-ℤ (x +fraction-ℤ y))) ∙ + ( inv (neg-rational-fraction-ℤ (x +fraction-ℤ y))) ∙ ( eq-ℚ-sim-fraction-ℤ ( neg-fraction-ℤ (x +fraction-ℤ y)) ( add-fraction-ℤ (neg-fraction-ℤ x) (neg-fraction-ℤ y)) diff --git a/src/elementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md index 3affd486cfb..458395e0a84 100644 --- a/src/elementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md @@ -13,7 +13,6 @@ open import elementary-number-theory.archimedean-property-rational-numbers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers -open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-rational-numbers @@ -22,7 +21,6 @@ open import elementary-number-theory.strict-inequality-positive-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.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types @@ -57,7 +55,7 @@ abstract asymmetric-le-ℚ ( zero-ℚ) ( y) - ( le-zero-is-positive-ℚ y pos-y) + ( le-zero-is-positive-ℚ pos-y) ( tr ( le-ℚ y) ( equational-reasoning diff --git a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md index 59ab9240074..f2fdcf6a303 100644 --- a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md +++ b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md @@ -15,7 +15,7 @@ open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integer-fractions open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.natural-numbers -open import elementary-number-theory.positive-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 @@ -42,7 +42,9 @@ of `ℚ` is that for any two an `n : ℕ` such that `y` is less than `n` as a rational number times `x`. ```agda -abstract +opaque + unfolding is-positive-ℚ + bound-archimedean-property-ℚ : (x y : ℚ) → is-positive-ℚ x → @@ -90,5 +92,5 @@ abstract exists-greater-natural-ℚ q = map-tot-exists ( λ _ → tr (le-ℚ q) (right-unit-law-mul-ℚ _)) - ( archimedean-property-ℚ one-ℚ q _) + ( archimedean-property-ℚ one-ℚ q (is-positive-rational-ℚ⁺ one-ℚ⁺)) ``` diff --git a/src/elementary-number-theory/difference-rational-numbers.lagda.md b/src/elementary-number-theory/difference-rational-numbers.lagda.md index 45b52b7ba80..21f068f27b5 100644 --- a/src/elementary-number-theory/difference-rational-numbers.lagda.md +++ b/src/elementary-number-theory/difference-rational-numbers.lagda.md @@ -183,7 +183,7 @@ abstract equational-reasoning rational-ℤ x -ℚ rational-ℤ y = rational-ℤ x +ℚ rational-ℤ (neg-ℤ y) - by ap (rational-ℤ x +ℚ_) (inv (preserves-neg-rational-ℤ y)) + by ap (rational-ℤ x +ℚ_) (inv (neg-rational-ℤ y)) = rational-ℤ (x -ℤ y) by add-rational-ℤ x (neg-ℤ y) ``` diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md index 8576576ca69..066898a463e 100644 --- a/src/elementary-number-theory/distance-rational-numbers.lagda.md +++ b/src/elementary-number-theory/distance-rational-numbers.lagda.md @@ -141,7 +141,7 @@ abstract ( equational-reasoning p *ℚ rational-dist-ℚ q r = rational-abs-ℚ (p *ℚ (q -ℚ r)) - by ap rational-ℚ⁰⁺ (inv (abs-left-mul-nonnegative-ℚ _ p⁰⁺)) + by inv (rational-abs-left-mul-nonnegative-ℚ _ p⁰⁺) = rational-abs-ℚ (p *ℚ q +ℚ p *ℚ (neg-ℚ r)) by ap rational-abs-ℚ (left-distributive-mul-add-ℚ p q (neg-ℚ r)) = rational-abs-ℚ (p *ℚ q -ℚ p *ℚ r) diff --git a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md new file mode 100644 index 00000000000..3c35c0ff087 --- /dev/null +++ b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md @@ -0,0 +1,106 @@ +# Inequalities between positive, negative, nonnegative, and nonpositive rational numbers + +```agda +module elementary-number-theory.inequalities-positive-and-negative-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.negative-rational-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.nonpositive-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.dependent-pair-types +``` + +
+ +## Idea + +This page describes +[inequalities](elementary-number-theory.inequalities-rational-numbers.md) and +[strict inequalities](elementary-number-theory.strict-inequality-rational-numbers.md) +between [positive](elementary-number-theory.positive-rational-numbers.md), +[negative](elementary-number-theory.negative-rational-numbers.md), +[nonnegative](elementary-number-theory.nonnegative-rational-numbers.md), and +[nonpositive](elementary-number-theory.nonpositive-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md). + +## Properties + +### Inequalities between rational numbers with different signs + +Some inequalities can be deduced directly from the sign of a rational number: +for example, every negative rational number is less than every nonnegative +rational number. + +#### Any negative rational number is less than any nonnegative rational number + +```agda +abstract + le-negative-nonnegative-ℚ : + (p : ℚ⁻) (q : ℚ⁰⁺) → le-ℚ (rational-ℚ⁻ p) (rational-ℚ⁰⁺ q) + le-negative-nonnegative-ℚ (p , neg-p) (q , nonneg-q) = + concatenate-le-leq-ℚ p zero-ℚ q + ( le-zero-is-negative-ℚ neg-p) + ( leq-zero-is-nonnegative-ℚ nonneg-q) + + leq-negative-nonnegative-ℚ : + (p : ℚ⁻) (q : ℚ⁰⁺) → leq-ℚ (rational-ℚ⁻ p) (rational-ℚ⁰⁺ q) + leq-negative-nonnegative-ℚ p q = leq-le-ℚ (le-negative-nonnegative-ℚ p q) +``` + +#### A nonpositive rational number is less than a positive rational number + +```agda +abstract + le-nonpositive-positive-ℚ : + (p : ℚ⁰⁻) (q : ℚ⁺) → le-ℚ (rational-ℚ⁰⁻ p) (rational-ℚ⁺ q) + le-nonpositive-positive-ℚ (p , nonpos-p) (q , pos-q) = + concatenate-leq-le-ℚ p zero-ℚ q + ( leq-zero-is-nonpositive-ℚ nonpos-p) + ( le-zero-is-positive-ℚ pos-q) +``` + +#### A nonpositive rational number is less than or equal to a nonnegative rational number + +```agda +abstract + leq-nonpositive-nonnegative-ℚ : + (p : ℚ⁰⁻) (q : ℚ⁰⁺) → leq-ℚ (rational-ℚ⁰⁻ p) (rational-ℚ⁰⁺ q) + leq-nonpositive-nonnegative-ℚ (p , nonpos-p) (q , nonneg-q) = + transitive-leq-ℚ p zero-ℚ q + ( leq-zero-is-nonnegative-ℚ nonneg-q) + ( leq-zero-is-nonpositive-ℚ nonpos-p) +``` + +### Inequalities showing the sign of a rational number + +#### If `p < q` and `p` is nonnegative, then `q` is positive + +```agda +abstract + is-positive-le-ℚ⁰⁺ : + (p : ℚ⁰⁺) (q : ℚ) → le-ℚ (rational-ℚ⁰⁺ p) q → is-positive-ℚ q + is-positive-le-ℚ⁰⁺ (p , nonneg-p) q pImports + +```agda +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.negative-rational-numbers +open import elementary-number-theory.positive-and-negative-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.identity-types +open import foundation.transport-along-identifications +``` + + + +## Idea + +The product of two +[negative rational numbers](elementary-number-theory.negative-rational-numbers.md) +is their [product](elementary-number-theory.multiplication-rational-numbers.md) +as [rational numbers](elementary-number-theory.rational-numbers.md), and is +[positive](elementary-number-theory.positive-rational-numbers.md). + +## Properties + +### The product of two negative rational numbers is positive + +```agda +opaque + unfolding is-negative-ℚ + + is-positive-mul-negative-ℚ : + {x y : ℚ} → is-negative-ℚ x → is-negative-ℚ y → is-positive-ℚ (x *ℚ y) + is-positive-mul-negative-ℚ {x} {y} P Q = + tr + ( is-positive-ℚ) + ( negative-law-mul-ℚ x y) + ( is-positive-mul-ℚ P Q) +``` + +### Multiplication by a negative rational number reverses inequality + +```agda +module _ + (p : ℚ⁻) + (q r : ℚ) + (H : leq-ℚ q r) + where + + abstract + reverses-leq-right-mul-ℚ⁻ : leq-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p) + reverses-leq-right-mul-ℚ⁻ = + binary-tr + ( leq-ℚ) + ( negative-law-mul-ℚ r (rational-ℚ⁻ p)) + ( negative-law-mul-ℚ q (rational-ℚ⁻ p)) + ( preserves-leq-right-mul-ℚ⁺ + ( neg-ℚ⁻ p) + ( neg-ℚ r) + ( neg-ℚ q) + ( neg-leq-ℚ H)) +``` + +### Multiplication by a negative rational number reverses strict inequality + +```agda +module _ + (p : ℚ⁻) + (q r : ℚ) + (H : le-ℚ q r) + where + + abstract + reverses-le-right-mul-ℚ⁻ : le-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p) + reverses-le-right-mul-ℚ⁻ = + binary-tr + ( le-ℚ) + ( negative-law-mul-ℚ r (rational-ℚ⁻ p)) + ( negative-law-mul-ℚ q (rational-ℚ⁻ p)) + ( preserves-le-right-mul-ℚ⁺ + ( neg-ℚ⁻ p) + ( neg-ℚ r) + ( neg-ℚ q) + ( neg-le-ℚ H)) + + reverses-le-left-mul-ℚ⁻ : le-ℚ (rational-ℚ⁻ p *ℚ r) (rational-ℚ⁻ p *ℚ q) + reverses-le-left-mul-ℚ⁻ = + binary-tr + ( le-ℚ) + ( commutative-mul-ℚ _ _) + ( commutative-mul-ℚ _ _) + ( reverses-le-right-mul-ℚ⁻) +``` + +### The negative rational numbers are invertible elements of the multiplicative monoid of rational numbers + +```agda +opaque + inv-ℚ⁻ : ℚ⁻ → ℚ⁻ + inv-ℚ⁻ q = neg-ℚ⁺ (inv-ℚ⁺ (neg-ℚ⁻ q)) + + left-inverse-law-mul-ℚ⁻ : + (q : ℚ⁻) → rational-ℚ⁻ (inv-ℚ⁻ q) *ℚ rational-ℚ⁻ q = one-ℚ + left-inverse-law-mul-ℚ⁻ q = + inv (swap-neg-mul-ℚ _ _) ∙ + ap rational-ℚ⁺ (left-inverse-law-mul-ℚ⁺ (neg-ℚ⁻ q)) + + right-inverse-law-mul-ℚ⁻ : + (q : ℚ⁻) → rational-ℚ⁻ q *ℚ rational-ℚ⁻ (inv-ℚ⁻ q) = one-ℚ + right-inverse-law-mul-ℚ⁻ q = + swap-neg-mul-ℚ _ _ ∙ + ap rational-ℚ⁺ (right-inverse-law-mul-ℚ⁺ (neg-ℚ⁻ q)) +``` + +### Inversion reverses inequality on negative rational numbers + +```agda +opaque + unfolding inv-ℚ⁻ + + reverses-leq-inv-ℚ⁻ : + (p q : ℚ⁻) → leq-ℚ⁻ p q → leq-ℚ⁻ (inv-ℚ⁻ q) (inv-ℚ⁻ p) + reverses-leq-inv-ℚ⁻ p q p≤q = + neg-leq-ℚ + ( inv-leq-ℚ⁺ + ( neg-ℚ⁻ q) + ( neg-ℚ⁻ p) + ( neg-leq-ℚ p≤q)) +``` + +### Inversion reverses strict inequality on negative rational numbers + +```agda +opaque + unfolding inv-ℚ⁻ + + reverses-le-inv-ℚ⁻ : + (p q : ℚ⁻) → le-ℚ⁻ p q → le-ℚ⁻ (inv-ℚ⁻ q) (inv-ℚ⁻ p) + reverses-le-inv-ℚ⁻ p q pImports ```agda +open import elementary-number-theory.decidable-total-order-rational-numbers open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.maximum-rational-numbers +open import elementary-number-theory.minimum-rational-numbers open import elementary-number-theory.multiplication-integer-fractions open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-positive-and-negative-integers @@ -23,6 +26,8 @@ open import elementary-number-theory.rational-numbers open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.identity-types + +open import order-theory.order-preserving-maps-total-orders ``` @@ -41,12 +46,12 @@ itself nonnegative. ```agda opaque - unfolding mul-ℚ + unfolding is-nonnegative-ℚ mul-ℚ is-nonnegative-mul-ℚ : - (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q → + {p q : ℚ} → is-nonnegative-ℚ p → is-nonnegative-ℚ q → is-nonnegative-ℚ (p *ℚ q) - is-nonnegative-mul-ℚ p q nonneg-p nonneg-q = + is-nonnegative-mul-ℚ {p} {q} nonneg-p nonneg-q = is-nonnegative-rational-fraction-ℤ ( is-nonnegative-mul-nonnegative-fraction-ℤ { fraction-ℚ p} @@ -56,7 +61,7 @@ opaque mul-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ mul-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) = - ( p *ℚ q , is-nonnegative-mul-ℚ p q nonneg-p nonneg-q) + ( p *ℚ q , is-nonnegative-mul-ℚ nonneg-p nonneg-q) infixl 35 _*ℚ⁰⁺_ _*ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ @@ -77,8 +82,7 @@ abstract ```agda opaque - unfolding leq-ℚ-Prop - unfolding mul-ℚ + unfolding is-nonnegative-ℚ leq-ℚ-Prop mul-ℚ preserves-leq-right-mul-ℚ⁰⁺ : (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r → @@ -123,3 +127,33 @@ abstract ( preserves-leq-right-mul-ℚ⁰⁺ s _ _ p≤q) ( preserves-leq-left-mul-ℚ⁰⁺ p _ _ r≤s) ``` + +### Multiplication by a nonnegative rational number distributes over the minimum operation + +```agda +abstract + left-distributive-mul-min-ℚ⁰⁺ : + (p : ℚ⁰⁺) (q r : ℚ) → + rational-ℚ⁰⁺ p *ℚ min-ℚ q r = + min-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) + left-distributive-mul-min-ℚ⁰⁺ p⁰⁺@(p , _) = + distributive-map-hom-min-Total-Order + ( ℚ-Total-Order) + ( ℚ-Total-Order) + ( p *ℚ_ , preserves-leq-left-mul-ℚ⁰⁺ p⁰⁺) +``` + +### Multiplication by a nonnegative rational number distributes over the maximum operation + +```agda +abstract + left-distributive-mul-max-ℚ⁰⁺ : + (p : ℚ⁰⁺) (q r : ℚ) → + rational-ℚ⁰⁺ p *ℚ max-ℚ q r = + max-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) + left-distributive-mul-max-ℚ⁰⁺ p⁰⁺@(p , _) = + distributive-map-hom-max-Total-Order + ( ℚ-Total-Order) + ( ℚ-Total-Order) + ( p *ℚ_ , preserves-leq-left-mul-ℚ⁰⁺ p⁰⁺) +``` diff --git a/src/elementary-number-theory/multiplication-nonpositive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-nonpositive-rational-numbers.lagda.md index 42b601b5891..f5bb0a14227 100644 --- a/src/elementary-number-theory/multiplication-nonpositive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-nonpositive-rational-numbers.lagda.md @@ -1,4 +1,4 @@ -# Multiplication of nonpositive rational numbers +# Multiplication by nonpositive rational numbers ```agda {-# OPTIONS --lossy-unification #-} @@ -36,7 +36,9 @@ as [rational numbers](elementary-number-theory.rational-numbers.md), and is ## Definition ```agda -abstract +opaque + unfolding is-nonpositive-ℚ + is-nonnegative-mul-nonpositive-ℚ : {x y : ℚ} → is-nonpositive-ℚ x → is-nonpositive-ℚ y → is-nonnegative-ℚ (x *ℚ y) @@ -44,7 +46,7 @@ abstract tr ( is-nonnegative-ℚ) ( negative-law-mul-ℚ x y) - ( is-nonnegative-mul-ℚ _ _ nonpos-x nonpos-y) + ( is-nonnegative-mul-ℚ nonpos-x nonpos-y) mul-nonpositive-ℚ : ℚ⁰⁻ → ℚ⁰⁻ → ℚ⁰⁺ mul-nonpositive-ℚ (p , nonpos-p) (q , nonpos-q) = @@ -56,7 +58,9 @@ mul-nonpositive-ℚ (p , nonpos-p) (q , nonpos-q) = ### Multiplication by a nonpositive rational number reverses inequality ```agda -abstract +opaque + unfolding is-nonpositive-ℚ + reverses-leq-right-mul-ℚ⁰⁻ : (p : ℚ⁰⁻) (q r : ℚ) → leq-ℚ q r → leq-ℚ (r *ℚ rational-ℚ⁰⁻ p) (q *ℚ rational-ℚ⁰⁻ p) @@ -65,6 +69,6 @@ abstract ( leq-ℚ) ( ap neg-ℚ (right-negative-law-mul-ℚ r p) ∙ neg-neg-ℚ _) ( ap neg-ℚ (right-negative-law-mul-ℚ q p) ∙ neg-neg-ℚ _) - ( neg-leq-ℚ _ _ + ( neg-leq-ℚ ( preserves-leq-right-mul-ℚ⁰⁺ (neg-ℚ p , nonpos-p) q r q≤r)) ``` diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md index bf55c8c8e74..63a7876bb54 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md @@ -1,4 +1,4 @@ -# Multiplication of positive, negative, and nonnegative rational numbers +# Multiplication by positive, negative, and nonnegative rational numbers ```agda module elementary-number-theory.multiplication-positive-and-negative-rational-numbers where @@ -25,8 +25,9 @@ open import foundation.transport-along-identifications ## Idea When we have information about the sign of the factors of a -[rational product](elementary-number-theory.multiplication-rational-numbers.md), -we can deduce the sign of their product too. +[rational](elementary-number-theory.rational-numbers.md) +[product](elementary-number-theory.multiplication-rational-numbers.md), we can +deduce the sign of their product too. ## Lemmas @@ -34,7 +35,7 @@ we can deduce the sign of their product too. ```agda opaque - unfolding mul-ℚ + unfolding is-positive-ℚ mul-ℚ is-negative-mul-positive-negative-ℚ : {x y : ℚ} → is-positive-ℚ x → is-negative-ℚ y → is-negative-ℚ (x *ℚ y) diff --git a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md index fd4ad86379d..1c43c7546b9 100644 --- a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md @@ -1,4 +1,4 @@ -# Multiplication of positive rational numbers +# Multiplication by positive rational numbers ```agda {-# OPTIONS --lossy-unification #-} @@ -59,7 +59,7 @@ itself positive. ```agda opaque - unfolding mul-ℚ + unfolding is-positive-ℚ mul-ℚ is-positive-mul-ℚ : {x y : ℚ} → is-positive-ℚ x → is-positive-ℚ y → is-positive-ℚ (x *ℚ y) @@ -147,7 +147,7 @@ module _ where opaque - unfolding mul-ℚ + unfolding is-positive-ℚ mul-ℚ inv-is-positive-ℚ : ℚ pr1 inv-is-positive-ℚ = inv-is-positive-fraction-ℤ (fraction-ℚ x) P @@ -215,8 +215,7 @@ module _ ```agda opaque - unfolding le-ℚ-Prop - unfolding mul-ℚ + unfolding is-positive-ℚ le-ℚ-Prop mul-ℚ preserves-le-left-mul-ℚ⁺ : (p : ℚ⁺) (q r : ℚ) → @@ -256,8 +255,7 @@ opaque ```agda opaque - unfolding leq-ℚ-Prop - unfolding mul-ℚ + unfolding is-positive-ℚ leq-ℚ-Prop mul-ℚ preserves-leq-left-mul-ℚ⁺ : (p : ℚ⁺) (q r : ℚ) → leq-ℚ q r → diff --git a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md index 37fa4dc41d4..4db36a011c9 100644 --- a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md @@ -138,7 +138,9 @@ module _ ( H) ( inv K) - abstract + opaque + unfolding is-negative-ℚ + is-invertible-element-ring-is-nonzero-ℚ : is-nonzero-ℚ x → is-invertible-element-Ring ring-ℚ x is-invertible-element-ring-is-nonzero-ℚ H = diff --git a/src/elementary-number-theory/negation-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/negation-closed-intervals-rational-numbers.lagda.md index 27b21b5e0b1..36d0cbef5f4 100644 --- a/src/elementary-number-theory/negation-closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/negation-closed-intervals-rational-numbers.lagda.md @@ -32,7 +32,7 @@ of a ```agda neg-closed-interval-ℚ : closed-interval-ℚ → closed-interval-ℚ neg-closed-interval-ℚ ((a , b) , a≤b) = - ((neg-ℚ b , neg-ℚ a) , neg-leq-ℚ a b a≤b) + ((neg-ℚ b , neg-ℚ a) , neg-leq-ℚ a≤b) ``` ## Properties @@ -48,7 +48,7 @@ abstract ( neg-closed-interval-ℚ [a,b]) ( neg-closed-interval-ℚ [c,d]) is-interior-neg-closed-interval-ℚ ((a , b) , _) ((c , d) , _) (aImports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.disjunction +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.order-preserving-maps-posets +open import order-theory.total-orders +``` + + + +## Idea + +A map `f : P → Q` between the underlying types of two +[total orders](order-theory.total-orders.md) is said to be +{{#concept "order preserving" Agda=hom-Total-Order Disambiguation="map between total orders"}} +if `x ≤ y` in `P` implies `f x ≤ f y` in `Q`. + +## Definition + +### Order preserving maps + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Total-Order l1 l2) (Q : Total-Order l3 l4) + where + + preserves-order-prop-Total-Order : + (type-Total-Order P → type-Total-Order Q) → Prop (l1 ⊔ l2 ⊔ l4) + preserves-order-prop-Total-Order = + preserves-order-prop-Poset (poset-Total-Order P) (poset-Total-Order Q) + + preserves-order-Total-Order : + (type-Total-Order P → type-Total-Order Q) → UU (l1 ⊔ l2 ⊔ l4) + preserves-order-Total-Order = + preserves-order-Poset (poset-Total-Order P) (poset-Total-Order Q) + + is-prop-preserves-order-Total-Order : + (f : type-Total-Order P → type-Total-Order Q) → + is-prop (preserves-order-Total-Order f) + is-prop-preserves-order-Total-Order = + is-prop-preserves-order-Poset (poset-Total-Order P) (poset-Total-Order Q) + + hom-set-Total-Order : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4) + hom-set-Total-Order = + set-subset + ( function-Set (type-Total-Order P) (set-Total-Order Q)) + ( preserves-order-prop-Total-Order) + + hom-Total-Order : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + hom-Total-Order = type-Set hom-set-Total-Order + + map-hom-Total-Order : + hom-Total-Order → type-Total-Order P → type-Total-Order Q + map-hom-Total-Order = + map-hom-Poset (poset-Total-Order P) (poset-Total-Order Q) + + preserves-order-hom-Total-Order : + (f : hom-Total-Order) → preserves-order-Total-Order (map-hom-Total-Order f) + preserves-order-hom-Total-Order = + preserves-order-hom-Poset (poset-Total-Order P) (poset-Total-Order Q) +``` + +## Properties + +### Order-preserving maps distribute over the minimum operation + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Total-Order l1 l2) (Q : Total-Order l3 l4) + (f : hom-Total-Order P Q) + where + + abstract + distributive-map-hom-min-Total-Order : + (x y : type-Total-Order P) → + map-hom-Total-Order P Q f (min-Total-Order P x y) = + min-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + distributive-map-hom-min-Total-Order x y = + elim-disjunction + ( Id-Prop + ( set-Total-Order Q) + ( map-hom-Total-Order P Q f (min-Total-Order P x y)) + ( min-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y))) + ( λ x≤y → + equational-reasoning + map-hom-Total-Order P Q f (min-Total-Order P x y) + = map-hom-Total-Order P Q f x + by + ap + ( map-hom-Total-Order P Q f) + ( left-leq-right-min-Total-Order P x y x≤y) + = + min-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + by + inv + ( left-leq-right-min-Total-Order Q _ _ + ( preserves-order-hom-Total-Order P Q f x y x≤y))) + ( λ y≤x → + equational-reasoning + map-hom-Total-Order P Q f (min-Total-Order P x y) + = map-hom-Total-Order P Q f y + by + ap + ( map-hom-Total-Order P Q f) + ( right-leq-left-min-Total-Order P x y y≤x) + = + min-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + by + inv + ( right-leq-left-min-Total-Order Q _ _ + ( preserves-order-hom-Total-Order P Q f y x y≤x))) + ( is-total-Total-Order P x y) +``` + +### Order-preserving maps distribute over the maximum operation + +```agda +module _ + {l1 l2 l3 l4 : Level} (P : Total-Order l1 l2) (Q : Total-Order l3 l4) + (f : hom-Total-Order P Q) + where + + abstract + distributive-map-hom-max-Total-Order : + (x y : type-Total-Order P) → + map-hom-Total-Order P Q f (max-Total-Order P x y) = + max-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + distributive-map-hom-max-Total-Order x y = + elim-disjunction + ( Id-Prop + ( set-Total-Order Q) + ( map-hom-Total-Order P Q f (max-Total-Order P x y)) + ( max-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y))) + ( λ x≤y → + equational-reasoning + map-hom-Total-Order P Q f (max-Total-Order P x y) + = map-hom-Total-Order P Q f y + by + ap + ( map-hom-Total-Order P Q f) + ( left-leq-right-max-Total-Order P x y x≤y) + = + max-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + by + inv + ( left-leq-right-max-Total-Order Q _ _ + ( preserves-order-hom-Total-Order P Q f x y x≤y))) + ( λ y≤x → + equational-reasoning + map-hom-Total-Order P Q f (max-Total-Order P x y) + = map-hom-Total-Order P Q f x + by + ap + ( map-hom-Total-Order P Q f) + ( right-leq-left-max-Total-Order P x y y≤x) + = + max-Total-Order Q + ( map-hom-Total-Order P Q f x) + ( map-hom-Total-Order P Q f y) + by + inv + ( right-leq-left-max-Total-Order Q _ _ + ( preserves-order-hom-Total-Order P Q f y x y≤x))) + ( is-total-Total-Order P x y) +``` 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 6d2c68d957e..d970a20b789 100644 --- a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md @@ -12,6 +12,8 @@ module real-numbers.addition-lower-dedekind-real-numbers where 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.negative-rational-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-positive-rational-numbers @@ -213,9 +215,7 @@ module _ {l : Level} (x : lower-ℝ l) where - opaque - unfolding neg-ℚ - + abstract right-unit-law-add-lower-ℝ : add-lower-ℝ x (lower-real-ℚ zero-ℚ) = x right-unit-law-add-lower-ℝ = eq-sim-cut-lower-ℝ @@ -231,8 +231,7 @@ module _ ( is-in-cut-diff-rational-ℚ⁺-lower-ℝ ( x) ( p) - ( neg-ℚ q , - is-positive-le-zero-ℚ (neg-ℚ q) (neg-le-ℚ q zero-ℚ q<0)) + ( neg-ℚ⁻ (q , is-negative-le-zero-ℚ q<0)) ( p Date: Fri, 10 Oct 2025 16:00:52 -0700 Subject: [PATCH 02/22] make pre-commit --- .../archimedean-property-rational-numbers.lagda.md | 2 +- ...inequalities-positive-and-negative-rational-numbers.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md index f2fdcf6a303..f9f12927fbf 100644 --- a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md +++ b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md @@ -15,7 +15,7 @@ open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integer-fractions open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.natural-numbers --- open import elementary-number-theory.positive-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 diff --git a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md index 3c35c0ff087..ac81b04c088 100644 --- a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md @@ -23,7 +23,7 @@ open import foundation.dependent-pair-types ## Idea This page describes -[inequalities](elementary-number-theory.inequalities-rational-numbers.md) and +[inequalities](elementary-number-theory.inequality-rational-numbers.md) and [strict inequalities](elementary-number-theory.strict-inequality-rational-numbers.md) between [positive](elementary-number-theory.positive-rational-numbers.md), [negative](elementary-number-theory.negative-rational-numbers.md), From 9dc460aca8f3d50aede96fcb7222cc61ea54219b Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 11 Oct 2025 21:23:22 -0700 Subject: [PATCH 03/22] Update --- ...ive-and-negative-rational-numbers.lagda.md | 15 ++++++++ .../negative-rational-numbers.lagda.md | 6 ++-- .../nonnegative-rational-numbers.lagda.md | 25 ++++++++++++++ .../nonpositive-rational-numbers.lagda.md | 13 +++++++ ...ive-and-negative-rational-numbers.lagda.md | 20 +++++------ .../rational-numbers.lagda.md | 3 +- ...e-roots-positive-rational-numbers.lagda.md | 2 +- .../squares-rational-numbers.lagda.md | 6 ++-- .../nonnegative-real-numbers.lagda.md | 7 ++-- ...re-roots-nonnegative-real-numbers.lagda.md | 34 ++++++++++--------- 10 files changed, 93 insertions(+), 38 deletions(-) diff --git a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md index ac81b04c088..414fa5ecdc3 100644 --- a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md @@ -11,6 +11,7 @@ open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.nonpositive-rational-numbers +open import elementary-number-theory.positive-and-negative-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 @@ -55,6 +56,20 @@ abstract leq-negative-nonnegative-ℚ p q = leq-le-ℚ (le-negative-nonnegative-ℚ p q) ``` +#### Any negative rational number is less than any positive rational number + +```agda +abstract + le-negative-positive-ℚ : + (p : ℚ⁻) (q : ℚ⁺) → le-ℚ (rational-ℚ⁻ p) (rational-ℚ⁺ q) + le-negative-positive-ℚ p q = + le-negative-nonnegative-ℚ p (nonnegative-ℚ⁺ q) + + leq-negative-positive-ℚ : + (p : ℚ⁻) (q : ℚ⁺) → leq-ℚ (rational-ℚ⁻ p) (rational-ℚ⁺ q) + leq-negative-positive-ℚ p q = leq-le-ℚ (le-negative-positive-ℚ p q) +``` + #### A nonpositive rational number is less than a positive rational number ```agda diff --git a/src/elementary-number-theory/negative-rational-numbers.lagda.md b/src/elementary-number-theory/negative-rational-numbers.lagda.md index 2dc1da8460c..20a8ca5963f 100644 --- a/src/elementary-number-theory/negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/negative-rational-numbers.lagda.md @@ -264,13 +264,13 @@ opaque mediant-zero-ℚ⁻ : ℚ⁻ → ℚ⁻ mediant-zero-ℚ⁻ (q , is-neg-q) = ( mediant-ℚ q zero-ℚ , - is-negative-le-zero-ℚ _ - ( le-right-mediant-ℚ _ _ (le-zero-is-negative-ℚ q is-neg-q))) + is-negative-le-zero-ℚ + ( le-right-mediant-ℚ _ _ (le-zero-is-negative-ℚ is-neg-q))) le-mediant-zero-ℚ⁻ : (q : ℚ⁻) → le-ℚ (rational-ℚ⁻ q) (rational-ℚ⁻ (mediant-zero-ℚ⁻ q)) le-mediant-zero-ℚ⁻ (q , is-neg-q) = - le-left-mediant-ℚ _ _ (le-zero-is-negative-ℚ q is-neg-q) + le-left-mediant-ℚ _ _ (le-zero-is-negative-ℚ is-neg-q) rational-mediant-zero-ℚ⁻ : ℚ⁻ → ℚ rational-mediant-zero-ℚ⁻ q = rational-ℚ⁻ (mediant-zero-ℚ⁻ q) diff --git a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md index 621a2787146..b7d23dc65ad 100644 --- a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md @@ -249,3 +249,28 @@ abstract nonnegative-diff-leq-ℚ : (x y : ℚ) → leq-ℚ x y → ℚ⁰⁺ nonnegative-diff-leq-ℚ x y x≤y = (y -ℚ x , is-nonnegative-diff-leq-ℚ x y x≤y) ``` + +### If `x ≤ y` and `x` is nonnegative, then `y` is nonnegative + +```agda +abstract + is-nonnegative-leq-ℚ⁰⁺ : + (x : ℚ⁰⁺) (y : ℚ) → leq-ℚ (rational-ℚ⁰⁺ x) y → + is-nonnegative-ℚ y + is-nonnegative-leq-ℚ⁰⁺ (x , is-nonneg-x) y x≤y = + is-nonnegative-leq-zero-ℚ + ( transitive-leq-ℚ zero-ℚ x y + ( x≤y) + ( leq-zero-is-nonnegative-ℚ is-nonneg-x)) +``` + +### If `x < y` and `x` is nonnegative, then `y` is nonnegative + +```agda +abstract + is-nonnegative-le-ℚ⁰⁺ : + (x : ℚ⁰⁺) (y : ℚ) → le-ℚ (rational-ℚ⁰⁺ x) y → + is-nonnegative-ℚ y + is-nonnegative-le-ℚ⁰⁺ x y xImports ```agda +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.minimum-rational-numbers @@ -88,8 +89,7 @@ module _ ( λ is-nonneg-neg-one-ℚ → ex-falso ( not-is-negative-is-nonnegative-ℚ - ( is-nonneg-neg-one-ℚ) - ( is-negative-rational-ℚ⁻ neg-one-ℚ⁻))) + ( is-negative-rational-ℚ⁻ neg-one-ℚ⁻ , is-nonneg-neg-one-ℚ))) is-inhabited-upper-cut-sqrt-ℝ⁰⁺ : is-inhabited-subtype upper-cut-sqrt-ℝ⁰⁺ is-inhabited-upper-cut-sqrt-ℝ⁰⁺ = @@ -122,8 +122,8 @@ module _ λ is-nonneg-q' → ex-falso ( not-is-negative-is-nonnegative-ℚ - ( is-nonneg-q') - ( is-negative-rational-ℚ⁻ (mediant-zero-ℚ⁻ q⁻))))) + ( is-negative-rational-ℚ⁻ (mediant-zero-ℚ⁻ q⁻) , + is-nonneg-q')))) ( λ q=0 → do ( q' , 0 Date: Tue, 14 Oct 2025 14:29:14 -0700 Subject: [PATCH 04/22] Progress --- ...wers-of-positive-rational-numbers.lagda.md | 0 ...wers-of-positive-rational-numbers.lagda.md | 49 +++++++++++++++++++ 2 files changed, 49 insertions(+) create mode 100644 src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/powers-of-positive-rational-numbers.lagda.md diff --git a/src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md b/src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md new file mode 100644 index 00000000000..e69de29bb2d diff --git a/src/elementary-number-theory/powers-of-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-of-positive-rational-numbers.lagda.md new file mode 100644 index 00000000000..33cb3b88f16 --- /dev/null +++ b/src/elementary-number-theory/powers-of-positive-rational-numbers.lagda.md @@ -0,0 +1,49 @@ +# Powers of positive rational numbers + +```agda +module elementary-number-theory.powers-of-positive-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.bernoullis-inequality-positive-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import group-theory.powers-of-elements-groups +``` + +
+ +## Idea + +The +{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ}} +on the [positive](elementary-number-theory.positive-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, +which is defined by [iteratively](foundation.iterating-functions.md) multiplying +`x` with itself `n` times. + +## Definition + +```agda +power-ℚ⁺ : ℕ → ℚ⁺ → ℚ⁺ +power-ℚ⁺ = power-Group group-mul-ℚ⁺ +``` + +## Properties + +### For any positive rational `ε`, `(1 + ε)ⁿ` grows without bound + +```agda + +``` + +## See also + +- [Powers of elements of a group](group-theory.powers-of-elements-groups.md) From 9963c472ee1f912b12ac290301d97d71fb48dd33 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 14 Oct 2025 14:49:48 -0700 Subject: [PATCH 05/22] Updates --- .../maximum-nonnegative-rational-numbers.lagda.md | 2 +- .../minimum-positive-rational-numbers.lagda.md | 6 +++--- ...positive-and-negative-rational-numbers.lagda.md | 6 ++++-- ...positive-and-negative-rational-numbers.lagda.md | 14 ++++++++++++++ ...icative-inverses-positive-real-numbers.lagda.md | 5 ++++- src/real-numbers/positive-real-numbers.lagda.md | 1 - 6 files changed, 26 insertions(+), 8 deletions(-) diff --git a/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md index e58e1036a68..2160af8be1b 100644 --- a/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md @@ -37,7 +37,7 @@ abstract {p q : ℚ} → is-nonnegative-ℚ p → is-nonnegative-ℚ q → is-nonnegative-ℚ (max-ℚ p q) is-nonnegative-max-ℚ {p} {q} is-nonneg-p _ = - is-nonnegative-leq-zero-ℚ _ + is-nonnegative-leq-zero-ℚ ( transitive-leq-ℚ ( zero-ℚ) ( p) diff --git a/src/elementary-number-theory/minimum-positive-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-positive-rational-numbers.lagda.md index 47c9745f5f1..b5ccc9867d9 100644 --- a/src/elementary-number-theory/minimum-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/minimum-positive-rational-numbers.lagda.md @@ -39,10 +39,10 @@ abstract is-positive-min-ℚ : {p q : ℚ} → is-positive-ℚ p → is-positive-ℚ q → is-positive-ℚ (min-ℚ p q) is-positive-min-ℚ {p} {q} is-pos-p is-pos-q = - is-positive-le-zero-ℚ _ + is-positive-le-zero-ℚ ( le-min-le-both-ℚ zero-ℚ p q - ( le-zero-is-positive-ℚ p is-pos-p) - ( le-zero-is-positive-ℚ q is-pos-q)) + ( le-zero-is-positive-ℚ is-pos-p) + ( le-zero-is-positive-ℚ is-pos-q)) min-ℚ⁺ : ℚ⁺ → ℚ⁺ → ℚ⁺ min-ℚ⁺ (p , is-pos-p) (q , is-pos-q) = diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md index 72a497095a0..8cbfc9610b2 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md @@ -71,7 +71,7 @@ mul-negative-positive-ℚ (p , neg-p) (q , pos-q) = ```agda opaque - unfolding mul-ℚ + unfolding is-nonnegative-ℚ is-positive-ℚ mul-ℚ is-nonnegative-mul-nonnegative-positive-ℚ : {x y : ℚ} → is-nonnegative-ℚ x → is-positive-ℚ y → is-nonnegative-ℚ (x *ℚ y) @@ -83,7 +83,9 @@ opaque ### The product of a nonpositive and a positive rational number is nonpositive ```agda -abstract +opaque + unfolding is-nonpositive-ℚ + is-nonpositive-mul-nonpositive-positive-ℚ : {x y : ℚ} → is-nonpositive-ℚ x → is-positive-ℚ y → is-nonpositive-ℚ (x *ℚ y) is-nonpositive-mul-nonpositive-positive-ℚ is-nonneg-neg-x is-pos-y = diff --git a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md index a2f18c7d166..af6fead7f8f 100644 --- a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md @@ -238,3 +238,17 @@ abstract ( le-zero-is-negative-ℚ N) ( leq-zero-is-nonnegative-ℚ NN) ``` + +### A rational number is not both positive and nonpositive + +```agda +abstract + not-is-positive-is-nonpositive-ℚ : + {x : ℚ} → ¬ (is-positive-ℚ x × is-nonpositive-ℚ x) + not-is-positive-is-nonpositive-ℚ {x} (P , NP) = + not-leq-le-ℚ + ( zero-ℚ) + ( x) + ( le-zero-is-positive-ℚ P) + ( leq-zero-is-nonpositive-ℚ NP) +``` diff --git a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md index b8a957c53fe..384e7af4c8a 100644 --- a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md @@ -19,6 +19,7 @@ open import elementary-number-theory.multiplication-closed-intervals-rational-nu open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers open import elementary-number-theory.nonpositive-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers @@ -443,7 +444,9 @@ module _ ( inv-le-ℚ⁺ p⁺ q⁺ p Date: Tue, 14 Oct 2025 16:39:53 -0700 Subject: [PATCH 06/22] More properties --- src/elementary-number-theory.lagda.md | 2 + ...roup-of-positive-rational-numbers.lagda.md | 8 + ...wers-of-positive-rational-numbers.lagda.md | 49 ---- .../powers-positive-rational-numbers.lagda.md | 256 ++++++++++++++++++ .../powers-of-elements-groups.lagda.md | 25 ++ ...ve-inverses-positive-real-numbers.lagda.md | 2 +- 6 files changed, 292 insertions(+), 50 deletions(-) delete mode 100644 src/elementary-number-theory/powers-of-positive-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/powers-positive-rational-numbers.lagda.md diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 542cd4fce73..f53d1f7c1a8 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -108,6 +108,7 @@ open import elementary-number-theory.infinitude-of-primes public open import elementary-number-theory.initial-segments-natural-numbers public open import elementary-number-theory.integer-fractions public open import elementary-number-theory.integer-partitions public +open import elementary-number-theory.integer-powers-of-positive-rational-numbers public open import elementary-number-theory.integers public open import elementary-number-theory.interior-closed-intervals-rational-numbers public open import elementary-number-theory.intersections-closed-intervals-rational-numbers public @@ -179,6 +180,7 @@ open import elementary-number-theory.positive-integers public open import elementary-number-theory.positive-rational-numbers public open import elementary-number-theory.powers-integers public open import elementary-number-theory.powers-of-two public +open import elementary-number-theory.powers-positive-rational-numbers public open import elementary-number-theory.prime-numbers public open import elementary-number-theory.products-of-natural-numbers public open import elementary-number-theory.proper-closed-intervals-rational-numbers public diff --git a/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md index 9ccaea277e7..3b2ca16a732 100644 --- a/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md @@ -236,3 +236,11 @@ abstract ( is-retraction-left-div-ℚ⁺ p⁺ r) ( preserves-le-left-mul-ℚ⁺ (inv-ℚ⁺ p⁺) _ _ pqImports - -```agda -open import elementary-number-theory.multiplication-positive-rational-numbers -open import elementary-number-theory.rational-numbers -open import elementary-number-theory.positive-rational-numbers -open import elementary-number-theory.bernoullis-inequality-positive-rational-numbers -open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers -open import elementary-number-theory.natural-numbers -open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.multiplication-natural-numbers -open import group-theory.powers-of-elements-groups -``` - - - -## Idea - -The -{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ}} -on the [positive](elementary-number-theory.positive-rational-numbers.md) -[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, -which is defined by [iteratively](foundation.iterating-functions.md) multiplying -`x` with itself `n` times. - -## Definition - -```agda -power-ℚ⁺ : ℕ → ℚ⁺ → ℚ⁺ -power-ℚ⁺ = power-Group group-mul-ℚ⁺ -``` - -## Properties - -### For any positive rational `ε`, `(1 + ε)ⁿ` grows without bound - -```agda - -``` - -## See also - -- [Powers of elements of a group](group-theory.powers-of-elements-groups.md) diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md new file mode 100644 index 00000000000..7815783fb91 --- /dev/null +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -0,0 +1,256 @@ +# Powers of positive rational numbers + +```agda +module elementary-number-theory.powers-positive-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.archimedean-property-rational-numbers +open import elementary-number-theory.arithmetic-sequences-positive-rational-numbers +open import elementary-number-theory.bernoullis-inequality-positive-rational-numbers +open import elementary-number-theory.geometric-sequences-positive-rational-numbers +open import elementary-number-theory.inequality-positive-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-positive-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.dependent-pair-types +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.transport-along-identifications + +open import group-theory.multiples-of-elements-abelian-groups +open import group-theory.powers-of-elements-groups +``` + +
+ +## Idea + +The +{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ}} +on the [positive](elementary-number-theory.positive-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, +which is defined by [iteratively](foundation.iterating-functions.md) multiplying +`x` with itself `n` times. + +## Definition + +```agda +power-ℚ⁺ : ℕ → ℚ⁺ → ℚ⁺ +power-ℚ⁺ = power-Group group-mul-ℚ⁺ +``` + +## Properties + +### `1ⁿ = 1` + +```agda +power-one-ℚ⁺ : (n : ℕ) → power-ℚ⁺ n one-ℚ⁺ = one-ℚ⁺ +power-one-ℚ⁺ = power-unit-Group group-mul-ℚ⁺ +``` + +### `qⁿ⁺¹ = qⁿq` + +```agda +power-succ-ℚ⁺ : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = power-ℚ⁺ n q *ℚ⁺ q +power-succ-ℚ⁺ = power-succ-Group group-mul-ℚ⁺ +``` + +### `qⁿ = qqⁿ` + +```agda +power-succ-ℚ⁺' : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = q *ℚ⁺ power-ℚ⁺ n q +power-succ-ℚ⁺' = power-succ-Group' group-mul-ℚ⁺ +``` + +### `qᵐ⁺ⁿ = qᵐqⁿ` + +```agda +distributive-power-add-ℚ⁺ : + (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m +ℕ n) q = power-ℚ⁺ m q *ℚ⁺ power-ℚ⁺ n q +distributive-power-add-ℚ⁺ m n _ = distributive-power-add-Group group-mul-ℚ⁺ m n +``` + +### `(pq)ⁿ=pⁿqⁿ` + +```agda +left-distributive-power-mul-ℚ⁺ : + (n : ℕ) (p q : ℚ⁺) → power-ℚ⁺ n (p *ℚ⁺ q) = power-ℚ⁺ n p *ℚ⁺ power-ℚ⁺ n q +left-distributive-power-mul-ℚ⁺ n p q = + left-distributive-multiple-add-Ab abelian-group-mul-ℚ⁺ n +``` + +### `pᵐⁿ = (pᵐ)ⁿ` + +```agda +power-mul-ℚ⁺ : + (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m *ℕ n) q = power-ℚ⁺ n (power-ℚ⁺ m q) +power-mul-ℚ⁺ m n q = power-mul-Group group-mul-ℚ⁺ m n +``` + +### If `p` and `q` are positive rational numbers with `p < q` and `n` is nonzero, `pⁿ < qⁿ` + +```agda +abstract + preserves-le-power-ℚ⁺ : + (n : ℕ) (p q : ℚ⁺) → le-ℚ⁺ p q → is-nonzero-ℕ n → + le-ℚ⁺ (power-ℚ⁺ n p) (power-ℚ⁺ n q) + preserves-le-power-ℚ⁺ 0 p q p Date: Tue, 14 Oct 2025 16:43:12 -0700 Subject: [PATCH 07/22] Back out integer powers --- .../integer-powers-of-positive-rational-numbers.lagda.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md diff --git a/src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md b/src/elementary-number-theory/integer-powers-of-positive-rational-numbers.lagda.md deleted file mode 100644 index e69de29bb2d..00000000000 From a69f76695b653a7178ad6277aa99b9713adfd65f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 14 Oct 2025 20:45:33 -0700 Subject: [PATCH 08/22] Fixes --- src/elementary-number-theory.lagda.md | 1 - .../powers-positive-rational-numbers.lagda.md | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index f53d1f7c1a8..be3b1e0ad01 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -108,7 +108,6 @@ open import elementary-number-theory.infinitude-of-primes public open import elementary-number-theory.initial-segments-natural-numbers public open import elementary-number-theory.integer-fractions public open import elementary-number-theory.integer-partitions public -open import elementary-number-theory.integer-powers-of-positive-rational-numbers public open import elementary-number-theory.integers public open import elementary-number-theory.interior-closed-intervals-rational-numbers public open import elementary-number-theory.intersections-closed-intervals-rational-numbers public diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 7815783fb91..811235c5420 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -45,7 +45,7 @@ open import group-theory.powers-of-elements-groups ## Idea The -{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ}} +{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ⁺}} on the [positive](elementary-number-theory.positive-rational-numbers.md) [rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md) multiplying From ea3fa12c81c28d11c10da66a04d9e42d6a7baf98 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 15 Oct 2025 09:15:11 -0700 Subject: [PATCH 09/22] Fix merge --- ...ion-positive-and-negative-rational-numbers.lagda.md | 6 ++---- .../positive-and-negative-rational-numbers.lagda.md | 10 ---------- ...ltiplicative-inverses-nonzero-real-numbers.lagda.md | 4 +--- src/real-numbers/negative-real-numbers.lagda.md | 4 ++-- .../square-roots-nonnegative-real-numbers.lagda.md | 10 ++-------- 5 files changed, 7 insertions(+), 27 deletions(-) diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md index e8b894794eb..eda0123b5e7 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md @@ -148,8 +148,7 @@ abstract ( y≠0) ( λ is-pos-y → ex-falso - ( is-not-negative-and-positive-ℚ - ( x *ℚ y) + ( not-is-negative-is-positive-ℚ ( is-negative-mul-negative-positive-ℚ is-neg-x is-pos-y , is-pos-xy)))) ( λ x=0 → @@ -164,8 +163,7 @@ abstract ( y) ( λ is-neg-y → ex-falso - ( is-not-negative-and-positive-ℚ - ( x *ℚ y) + ( not-is-negative-is-positive-ℚ ( is-negative-mul-positive-negative-ℚ is-pos-x is-neg-y , is-pos-xy))) ( y≠0) diff --git a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md index ed64fcf3fdf..00e1063ad38 100644 --- a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md @@ -239,16 +239,6 @@ abstract ( leq-zero-is-nonnegative-ℚ NN) ``` -### A positive rational number is not negative - -```agda -abstract - not-is-negative-is-positive-ℚ : - {q : ℚ} → is-positive-ℚ q → ¬ (is-negative-ℚ q) - not-is-negative-is-positive-ℚ {q} is-pos-q = - not-is-negative-is-nonnegative-ℚ (is-nonnegative-is-positive-ℚ q is-pos-q) -``` - ### If `p < q` and `q` is nonpositive, then `p` is negative ```agda diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index 79a1985bb71..43c55227e30 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -151,7 +151,6 @@ opaque let is-positive-mul p q {r} lb1 lb2 = is-positive-le-zero-ℚ - ( p *ℚ q) ( concatenate-le-leq-ℚ ( zero-ℚ) ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d]) @@ -173,8 +172,7 @@ opaque ( intro-exists (b , is-neg-b) x Date: Wed, 15 Oct 2025 09:29:06 -0700 Subject: [PATCH 10/22] make pre-commit --- .../multiplicative-inverses-positive-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md index 384e7af4c8a..06b96659065 100644 --- a/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-positive-real-numbers.lagda.md @@ -10,6 +10,7 @@ module real-numbers.multiplicative-inverses-positive-real-numbers where ```agda open import elementary-number-theory.closed-intervals-rational-numbers +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.maximum-positive-rational-numbers open import elementary-number-theory.maximum-rational-numbers @@ -19,7 +20,6 @@ open import elementary-number-theory.multiplication-closed-intervals-rational-nu open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers -open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers open import elementary-number-theory.nonpositive-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers From df308e2425fb8b1863565200a6a735d7e5afc7cd Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 15 Oct 2025 13:58:21 -0700 Subject: [PATCH 11/22] Fix merge --- ...ication-negative-rational-numbers.lagda.md | 19 +++++++++---------- .../squares-real-numbers.lagda.md | 4 ++-- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/elementary-number-theory/multiplication-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-negative-rational-numbers.lagda.md index 5a41de6f305..bd53f0e9c03 100644 --- a/src/elementary-number-theory/multiplication-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-negative-rational-numbers.lagda.md @@ -21,18 +21,9 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-transport +open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.transport-along-identifications -open import elementary-number-theory.multiplication-positive-rational-numbers -open import elementary-number-theory.multiplication-rational-numbers -open import elementary-number-theory.negative-integer-fractions -open import elementary-number-theory.negative-rational-numbers -open import elementary-number-theory.positive-and-negative-rational-numbers -open import elementary-number-theory.positive-integer-fractions -open import elementary-number-theory.positive-rational-numbers -open import elementary-number-theory.rational-numbers - -open import foundation.dependent-pair-types ``` @@ -60,6 +51,14 @@ opaque ( is-positive-ℚ) ( negative-law-mul-ℚ x y) ( is-positive-mul-ℚ P Q) + +mul-ℚ⁻ : ℚ⁻ → ℚ⁻ → ℚ⁺ +mul-ℚ⁻ (p , is-neg-p) (q , is-neg-q) = + (p *ℚ q , is-positive-mul-negative-ℚ is-neg-p is-neg-q) + +infixl 40 _*ℚ⁻_ +_*ℚ⁻_ : ℚ⁻ → ℚ⁻ → ℚ⁺ +_*ℚ⁻_ = mul-ℚ⁻ ``` ### Multiplication by a negative rational number reverses inequality diff --git a/src/real-numbers/squares-real-numbers.lagda.md b/src/real-numbers/squares-real-numbers.lagda.md index 9420a081e95..c6fedb34990 100644 --- a/src/real-numbers/squares-real-numbers.lagda.md +++ b/src/real-numbers/squares-real-numbers.lagda.md @@ -98,7 +98,7 @@ opaque ( is-positive-prop-ℚ q) ( λ a'<0 → let - a'⁻ = (a' , is-negative-le-zero-ℚ a' a'<0) + a'⁻ = (a' , is-negative-le-zero-ℚ a'<0) in is-positive-le-ℚ⁺ ( a'⁻ *ℚ⁻ a'⁻) @@ -113,7 +113,7 @@ opaque ( [a',b'][a',b'] Date: Fri, 17 Oct 2025 09:39:18 -0700 Subject: [PATCH 12/22] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- ...lities-positive-and-negative-rational-numbers.lagda.md | 8 ++++---- ...cation-positive-and-negative-rational-numbers.lagda.md | 3 +-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md index 414fa5ecdc3..88ac145a32a 100644 --- a/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md @@ -36,8 +36,8 @@ between [positive](elementary-number-theory.positive-rational-numbers.md), ### Inequalities between rational numbers with different signs -Some inequalities can be deduced directly from the sign of a rational number: -for example, every negative rational number is less than every nonnegative +Some inequalities can be deduced directly from the sign of a rational number. +For example, every negative rational number is less than every nonnegative rational number. #### Any negative rational number is less than any nonnegative rational number @@ -70,7 +70,7 @@ abstract leq-negative-positive-ℚ p q = leq-le-ℚ (le-negative-positive-ℚ p q) ``` -#### A nonpositive rational number is less than a positive rational number +#### A nonpositive rational number is less than any positive rational number ```agda abstract @@ -82,7 +82,7 @@ abstract ( le-zero-is-positive-ℚ pos-q) ``` -#### A nonpositive rational number is less than or equal to a nonnegative rational number +#### A nonpositive rational number is less than or equal to any nonnegative rational number ```agda abstract diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md index eda0123b5e7..39db46c6512 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md @@ -30,8 +30,7 @@ open import foundation.transport-along-identifications ## Idea When we have information about the sign of the factors of a -[rational](elementary-number-theory.rational-numbers.md) -[product](elementary-number-theory.multiplication-rational-numbers.md), we can +[product](elementary-number-theory.multiplication-rational-numbers.md) of [rational numbers](elementary-number-theory.rational-numbers.md), we can deduce the sign of their product too. ## Lemmas From daa9fc084e696aa8775564973cdcc2804bd7e3aa Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 09:43:42 -0700 Subject: [PATCH 13/22] Respond to review comments --- ...positive-and-negative-rational-numbers.lagda.md | 9 +++++---- ...positive-and-negative-rational-numbers.lagda.md | 14 +++++++------- .../order-preserving-maps-posets.lagda.md | 2 +- .../order-preserving-maps-total-orders.lagda.md | 2 +- ...licative-inverses-nonzero-real-numbers.lagda.md | 2 +- ...icative-inverses-positive-real-numbers.lagda.md | 2 +- .../square-roots-nonnegative-real-numbers.lagda.md | 10 +++++----- 7 files changed, 21 insertions(+), 20 deletions(-) diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md index 39db46c6512..4cbe0a91112 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-rational-numbers.lagda.md @@ -30,8 +30,9 @@ open import foundation.transport-along-identifications ## Idea When we have information about the sign of the factors of a -[product](elementary-number-theory.multiplication-rational-numbers.md) of [rational numbers](elementary-number-theory.rational-numbers.md), we can -deduce the sign of their product too. +[product](elementary-number-theory.multiplication-rational-numbers.md) of +[rational numbers](elementary-number-theory.rational-numbers.md), we can deduce +the sign of their product too. ## Lemmas @@ -147,7 +148,7 @@ abstract ( y≠0) ( λ is-pos-y → ex-falso - ( not-is-negative-is-positive-ℚ + ( is-not-negative-and-positive-ℚ ( is-negative-mul-negative-positive-ℚ is-neg-x is-pos-y , is-pos-xy)))) ( λ x=0 → @@ -162,7 +163,7 @@ abstract ( y) ( λ is-neg-y → ex-falso - ( not-is-negative-is-positive-ℚ + ( is-not-negative-and-positive-ℚ ( is-negative-mul-positive-negative-ℚ is-pos-x is-neg-y , is-pos-xy))) ( y≠0) diff --git a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md index 00e1063ad38..e0447a64bbc 100644 --- a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md @@ -215,9 +215,9 @@ neg-ℚ⁰⁻ (q , is-nonpos-q) = ```agda abstract - not-is-negative-is-positive-ℚ : + is-not-negative-and-positive-ℚ : {x : ℚ} → ¬ (is-negative-ℚ x × is-positive-ℚ x) - not-is-negative-is-positive-ℚ {x} (N , P) = + is-not-negative-and-positive-ℚ {x} (N , P) = not-leq-le-ℚ ( zero-ℚ) ( x) @@ -229,9 +229,9 @@ abstract ```agda abstract - not-is-negative-is-nonnegative-ℚ : + is-not-negative-and-nonnegativeℚ : {x : ℚ} → ¬ (is-negative-ℚ x × is-nonnegative-ℚ x) - not-is-negative-is-nonnegative-ℚ {x} (N , NN) = + is-not-negative-and-nonnegativeℚ {x} (N , NN) = not-leq-le-ℚ ( x) ( zero-ℚ) @@ -239,13 +239,13 @@ abstract ( leq-zero-is-nonnegative-ℚ NN) ``` -### If `p < q` and `q` is nonpositive, then `p` is negative +### A rational number is not both positive and nonpositive ```agda abstract - not-is-positive-is-nonpositive-ℚ : + is-not-positive-and-nonpositive-ℚ : {x : ℚ} → ¬ (is-positive-ℚ x × is-nonpositive-ℚ x) - not-is-positive-is-nonpositive-ℚ {x} (P , NP) = + is-not-positive-and-nonpositive-ℚ {x} (P , NP) = not-leq-le-ℚ ( zero-ℚ) ( x) diff --git a/src/order-theory/order-preserving-maps-posets.lagda.md b/src/order-theory/order-preserving-maps-posets.lagda.md index 4d127ed3ff8..bcd5ba75286 100644 --- a/src/order-theory/order-preserving-maps-posets.lagda.md +++ b/src/order-theory/order-preserving-maps-posets.lagda.md @@ -27,7 +27,7 @@ open import order-theory.posets A map `f : P → Q` between the underlying types of two [posets](order-theory.posets.md) is said to be -{{#concept "order preserving" Agda=hom-Poset Disambiguation="map between posets"}} +{{#concept "order preserving" WD="increasing function" WDID=Q3075182 Agda=hom-Poset Disambiguation="map between posets"}} if `x ≤ y` in `P` implies `f x ≤ f y` in `Q`. ## Definition diff --git a/src/order-theory/order-preserving-maps-total-orders.lagda.md b/src/order-theory/order-preserving-maps-total-orders.lagda.md index f3ae69baab9..161a0dafd86 100644 --- a/src/order-theory/order-preserving-maps-total-orders.lagda.md +++ b/src/order-theory/order-preserving-maps-total-orders.lagda.md @@ -26,7 +26,7 @@ open import order-theory.total-orders A map `f : P → Q` between the underlying types of two [total orders](order-theory.total-orders.md) is said to be -{{#concept "order preserving" Agda=hom-Total-Order Disambiguation="map between total orders"}} +{{#concept "order preserving" WD="increasing function" WDID=Q3075182 Agda=hom-Total-Order Disambiguation="map between total orders"}} if `x ≤ y` in `P` implies `f x ≤ f y` in `Q`. ## Definition diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index 43c55227e30..f91c1d2bfcf 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -172,7 +172,7 @@ opaque ( intro-exists (b , is-neg-b) x Date: Fri, 17 Oct 2025 10:07:16 -0700 Subject: [PATCH 14/22] Progress --- .../powers-rational-numbers.lagda.md | 228 ++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 src/elementary-number-theory/powers-rational-numbers.lagda.md diff --git a/src/elementary-number-theory/powers-rational-numbers.lagda.md b/src/elementary-number-theory/powers-rational-numbers.lagda.md new file mode 100644 index 00000000000..ee922d0fad0 --- /dev/null +++ b/src/elementary-number-theory/powers-rational-numbers.lagda.md @@ -0,0 +1,228 @@ +# Powers of rational numbers + +```agda +module elementary-number-theory.powers-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.multiplicative-monoid-of-rational-numbers +open import group-theory.powers-of-elements-monoids +open import foundation.identity-types +``` + +
+ +## Idea + +The +{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ⁺}} +on the [positive](elementary-number-theory.positive-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, +which is defined by [iteratively](foundation.iterating-functions.md) multiplying +`x` with itself `n` times. + +## Definition + +```agda +power-ℚ⁺ : ℕ → ℚ⁺ → ℚ⁺ +power-ℚ⁺ = power-Group group-mul-ℚ⁺ +``` + +## Properties + +### `1ⁿ = 1` + +```agda +power-one-ℚ⁺ : (n : ℕ) → power-ℚ⁺ n one-ℚ⁺ = one-ℚ⁺ +power-one-ℚ⁺ = power-unit-Group group-mul-ℚ⁺ +``` + +### `qⁿ⁺¹ = qⁿq` + +```agda +power-succ-ℚ⁺ : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = power-ℚ⁺ n q *ℚ⁺ q +power-succ-ℚ⁺ = power-succ-Group group-mul-ℚ⁺ +``` + +### `qⁿ = qqⁿ` + +```agda +power-succ-ℚ⁺' : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = q *ℚ⁺ power-ℚ⁺ n q +power-succ-ℚ⁺' = power-succ-Group' group-mul-ℚ⁺ +``` + +### `qᵐ⁺ⁿ = qᵐqⁿ` + +```agda +distributive-power-add-ℚ⁺ : + (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m +ℕ n) q = power-ℚ⁺ m q *ℚ⁺ power-ℚ⁺ n q +distributive-power-add-ℚ⁺ m n _ = distributive-power-add-Group group-mul-ℚ⁺ m n +``` + +### `(pq)ⁿ=pⁿqⁿ` + +```agda +left-distributive-power-mul-ℚ⁺ : + (n : ℕ) (p q : ℚ⁺) → power-ℚ⁺ n (p *ℚ⁺ q) = power-ℚ⁺ n p *ℚ⁺ power-ℚ⁺ n q +left-distributive-power-mul-ℚ⁺ n p q = + left-distributive-multiple-add-Ab abelian-group-mul-ℚ⁺ n +``` + +### `pᵐⁿ = (pᵐ)ⁿ` + +```agda +power-mul-ℚ⁺ : + (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m *ℕ n) q = power-ℚ⁺ n (power-ℚ⁺ m q) +power-mul-ℚ⁺ m n q = power-mul-Group group-mul-ℚ⁺ m n +``` + +### If `p` and `q` are positive rational numbers with `p < q` and `n` is nonzero, `pⁿ < qⁿ` + +```agda +abstract + preserves-le-power-ℚ⁺ : + (n : ℕ) (p q : ℚ⁺) → le-ℚ⁺ p q → is-nonzero-ℕ n → + le-ℚ⁺ (power-ℚ⁺ n p) (power-ℚ⁺ n q) + preserves-le-power-ℚ⁺ 0 p q p Date: Fri, 17 Oct 2025 10:07:41 -0700 Subject: [PATCH 15/22] Clarify concept disambiguation --- .../powers-positive-rational-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 811235c5420..789446dfa67 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -45,7 +45,7 @@ open import group-theory.powers-of-elements-groups ## Idea The -{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ⁺}} +{{#concept "power operation" Disambiguation="a positive rational number to a natural number power" Agda=power-ℚ⁺}} on the [positive](elementary-number-theory.positive-rational-numbers.md) [rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md) multiplying From e0a24b825f0e63177d5c9fe62c33c3a092b47e2d Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 10:08:06 -0700 Subject: [PATCH 16/22] Progress --- .../powers-rational-numbers.lagda.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/elementary-number-theory/powers-rational-numbers.lagda.md b/src/elementary-number-theory/powers-rational-numbers.lagda.md index ee922d0fad0..2f5c88228e5 100644 --- a/src/elementary-number-theory/powers-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-rational-numbers.lagda.md @@ -17,11 +17,10 @@ open import foundation.identity-types ## Idea The -{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ⁺}} -on the [positive](elementary-number-theory.positive-rational-numbers.md) -[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, -which is defined by [iteratively](foundation.iterating-functions.md) multiplying -`x` with itself `n` times. +{{#concept "power operation" Disambiguation="raising a rational number to a natural number power" Agda=power-ℚ}} +on the [rational numbers](elementary-number-theory.rational-numbers.md) +`n x ↦ xⁿ`, is defined by [iteratively](foundation.iterating-functions.md) +multiplying `x` with itself `n` times. ## Definition From c5b3be8a204d11ef7e5b5439126af5ecc24b5cd4 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 10:08:45 -0700 Subject: [PATCH 17/22] Further clarify doc --- .../powers-positive-rational-numbers.lagda.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md index 789446dfa67..61a906395d3 100644 --- a/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-positive-rational-numbers.lagda.md @@ -47,9 +47,11 @@ open import group-theory.powers-of-elements-groups The {{#concept "power operation" Disambiguation="a positive rational number to a natural number power" Agda=power-ℚ⁺}} on the [positive](elementary-number-theory.positive-rational-numbers.md) -[rational numbers](elementary-number-theory.rational-numbers.md) `n x ↦ xⁿ`, -which is defined by [iteratively](foundation.iterating-functions.md) multiplying -`x` with itself `n` times. +[rational numbers](elementary-number-theory.rational-numbers.md) is the +operation `n x ↦ xⁿ`, which is defined by +[iteratively](foundation.iterating-functions.md) multiplying `x` with itself `n` +times. This file covers the case where `n` is a +[natural number](elementary-number-theory.natural-numbers.md). ## Definition From a8c35cd424f51abc92b27cfe1e0f2330b3df1025 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 10:55:55 -0700 Subject: [PATCH 18/22] Progress --- src/elementary-number-theory.lagda.md | 1 + .../parity-natural-numbers.lagda.md | 10 +- .../powers-rational-numbers.lagda.md | 271 +++++++++--------- .../squares-rational-numbers.lagda.md | 24 ++ ...s-of-elements-commutative-monoids.lagda.md | 8 +- 5 files changed, 168 insertions(+), 146 deletions(-) diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index be3b1e0ad01..0e518ce0112 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -180,6 +180,7 @@ open import elementary-number-theory.positive-rational-numbers public open import elementary-number-theory.powers-integers public open import elementary-number-theory.powers-of-two public open import elementary-number-theory.powers-positive-rational-numbers public +open import elementary-number-theory.powers-rational-numbers public open import elementary-number-theory.prime-numbers public open import elementary-number-theory.products-of-natural-numbers public open import elementary-number-theory.proper-closed-intervals-rational-numbers public diff --git a/src/elementary-number-theory/parity-natural-numbers.lagda.md b/src/elementary-number-theory/parity-natural-numbers.lagda.md index 503b5245425..9fa410e7f87 100644 --- a/src/elementary-number-theory/parity-natural-numbers.lagda.md +++ b/src/elementary-number-theory/parity-natural-numbers.lagda.md @@ -29,9 +29,13 @@ open import foundation.universe-levels ## Idea -Parity partitions the natural numbers into two classes: the even and the odd -natural numbers. Even natural numbers are those that are divisible by two, and -odd natural numbers are those that aren't. +{{#concept "Parity" WDID=Q230967 WD="parity"}} partitions the +[natural numbers](elementary-number-theory.natural-numbers.md) into two classes: +the {{#concept "even" WDID=Q13366104 WD="even number" Agda=is-even-ℕ}} and the +{{#concept "odd" WDID=Q13366129 WD="odd number" Agda=is-odd-ℕ}} natural numbers. +Even natural numbers are those that are +[divisible](elementary-number-theory.divisibility-natural-numbers.md) by two, +and odd natural numbers are those that [aren't](foundation.negation.md). ## Definition diff --git a/src/elementary-number-theory/powers-rational-numbers.lagda.md b/src/elementary-number-theory/powers-rational-numbers.lagda.md index 2f5c88228e5..83f95cea235 100644 --- a/src/elementary-number-theory/powers-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-rational-numbers.lagda.md @@ -7,9 +7,32 @@ module elementary-number-theory.powers-rational-numbers where
Imports ```agda +open import elementary-number-theory.absolute-value-rational-numbers +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.inequality-nonnegative-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-nonnegative-rational-numbers +open import elementary-number-theory.multiplication-positive-and-negative-rational-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-rational-numbers -open import group-theory.powers-of-elements-monoids +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-rational-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.parity-natural-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.squares-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.transport-along-identifications + +open import group-theory.powers-of-elements-commutative-monoids +open import group-theory.powers-of-elements-monoids ```
@@ -25,8 +48,8 @@ multiplying `x` with itself `n` times. ## Definition ```agda -power-ℚ⁺ : ℕ → ℚ⁺ → ℚ⁺ -power-ℚ⁺ = power-Group group-mul-ℚ⁺ +power-ℚ : ℕ → ℚ → ℚ +power-ℚ = power-Monoid monoid-mul-ℚ ``` ## Properties @@ -34,194 +57,162 @@ power-ℚ⁺ = power-Group group-mul-ℚ⁺ ### `1ⁿ = 1` ```agda -power-one-ℚ⁺ : (n : ℕ) → power-ℚ⁺ n one-ℚ⁺ = one-ℚ⁺ -power-one-ℚ⁺ = power-unit-Group group-mul-ℚ⁺ +abstract + power-one-ℚ : (n : ℕ) → power-ℚ n one-ℚ = one-ℚ + power-one-ℚ = power-unit-Monoid monoid-mul-ℚ ``` -### `qⁿ⁺¹ = qⁿq` +### `qⁿ¹ = qⁿq` ```agda -power-succ-ℚ⁺ : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = power-ℚ⁺ n q *ℚ⁺ q -power-succ-ℚ⁺ = power-succ-Group group-mul-ℚ⁺ +abstract + power-succ-ℚ : (n : ℕ) (q : ℚ) → power-ℚ (succ-ℕ n) q = power-ℚ n q *ℚ q + power-succ-ℚ = power-succ-Monoid monoid-mul-ℚ ``` ### `qⁿ = qqⁿ` ```agda -power-succ-ℚ⁺' : (n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (succ-ℕ n) q = q *ℚ⁺ power-ℚ⁺ n q -power-succ-ℚ⁺' = power-succ-Group' group-mul-ℚ⁺ +abstract + power-succ-ℚ' : (n : ℕ) (q : ℚ) → power-ℚ (succ-ℕ n) q = q *ℚ power-ℚ n q + power-succ-ℚ' = power-succ-Monoid' monoid-mul-ℚ ``` -### `qᵐ⁺ⁿ = qᵐqⁿ` +### `qᵐⁿ = qᵐqⁿ` ```agda -distributive-power-add-ℚ⁺ : - (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m +ℕ n) q = power-ℚ⁺ m q *ℚ⁺ power-ℚ⁺ n q -distributive-power-add-ℚ⁺ m n _ = distributive-power-add-Group group-mul-ℚ⁺ m n +abstract + distributive-power-add-ℚ : + (m n : ℕ) (q : ℚ) → power-ℚ (m +ℕ n) q = power-ℚ m q *ℚ power-ℚ n q + distributive-power-add-ℚ m n _ = + distributive-power-add-Monoid monoid-mul-ℚ m n ``` ### `(pq)ⁿ=pⁿqⁿ` ```agda -left-distributive-power-mul-ℚ⁺ : - (n : ℕ) (p q : ℚ⁺) → power-ℚ⁺ n (p *ℚ⁺ q) = power-ℚ⁺ n p *ℚ⁺ power-ℚ⁺ n q -left-distributive-power-mul-ℚ⁺ n p q = - left-distributive-multiple-add-Ab abelian-group-mul-ℚ⁺ n +abstract + left-distributive-power-mul-ℚ : + (n : ℕ) (p q : ℚ) → power-ℚ n (p *ℚ q) = power-ℚ n p *ℚ power-ℚ n q + left-distributive-power-mul-ℚ n p q = + distributive-power-mul-Commutative-Monoid commutative-monoid-mul-ℚ n ``` ### `pᵐⁿ = (pᵐ)ⁿ` ```agda -power-mul-ℚ⁺ : - (m n : ℕ) (q : ℚ⁺) → power-ℚ⁺ (m *ℕ n) q = power-ℚ⁺ n (power-ℚ⁺ m q) -power-mul-ℚ⁺ m n q = power-mul-Group group-mul-ℚ⁺ m n +abstract + power-mul-ℚ : + (m n : ℕ) (q : ℚ) → power-ℚ (m *ℕ n) q = power-ℚ n (power-ℚ m q) + power-mul-ℚ m n q = power-mul-Monoid monoid-mul-ℚ m n ``` -### If `p` and `q` are positive rational numbers with `p < q` and `n` is nonzero, `pⁿ < qⁿ` +### Even powers of rational numbers are nonnegative ```agda abstract - preserves-le-power-ℚ⁺ : - (n : ℕ) (p q : ℚ⁺) → le-ℚ⁺ p q → is-nonzero-ℕ n → - le-ℚ⁺ (power-ℚ⁺ n p) (power-ℚ⁺ n q) - preserves-le-power-ℚ⁺ 0 p q pImports ```agda +open import elementary-number-theory.absolute-value-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.maximum-rational-numbers open import elementary-number-theory.multiplication-negative-rational-numbers open import elementary-number-theory.multiplication-nonnegative-rational-numbers open import elementary-number-theory.multiplication-nonpositive-rational-numbers @@ -171,6 +173,10 @@ abstract (x : ℚ) → is-negative-ℚ x → is-positive-ℚ (square-ℚ x) is-positive-square-negative-ℚ x neg-x = is-positive-mul-negative-ℚ {x} {x} neg-x neg-x + +square-ℚ⁻ : ℚ⁻ → ℚ⁺ +square-ℚ⁻ (q , is-neg-q) = + (square-ℚ q , is-positive-square-negative-ℚ q is-neg-q) ``` ### If the square of a rational number is 0, it is zero @@ -274,3 +280,21 @@ abstract ( preserves-leq-square-ℚ⁰⁺ q⁰⁺ p⁰⁺ q≤p))) ( decide-le-leq-ℚ p q) ``` + +### `|p|² = p²` + +```agda +abstract + square-abs-ℚ : (q : ℚ) → square-ℚ (rational-abs-ℚ q) = square-ℚ q + square-abs-ℚ q = + rec-coproduct + ( λ q≤-q → + equational-reasoning + square-ℚ (rational-abs-ℚ q) + = square-ℚ (neg-ℚ q) + by ap square-ℚ (left-leq-right-max-ℚ _ _ q≤-q) + = square-ℚ q + by square-neg-ℚ q) + ( λ -q≤q → ap square-ℚ (right-leq-left-max-ℚ _ _ -q≤q)) + ( linear-leq-ℚ q (neg-ℚ q)) +``` diff --git a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md index 344471dcb03..54c92815ab0 100644 --- a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md @@ -144,13 +144,15 @@ module _ distributive-power-mul-Commutative-Monoid : (n : ℕ) {x y : type-Commutative-Monoid M} → - (H : mul-Commutative-Monoid M x y = mul-Commutative-Monoid M y x) → power-Commutative-Monoid M n (mul-Commutative-Monoid M x y) = mul-Commutative-Monoid M ( power-Commutative-Monoid M n x) ( power-Commutative-Monoid M n y) - distributive-power-mul-Commutative-Monoid = - distributive-power-mul-Monoid (monoid-Commutative-Monoid M) + distributive-power-mul-Commutative-Monoid n = + distributive-power-mul-Monoid + ( monoid-Commutative-Monoid M) + ( n) + ( commutative-mul-Commutative-Monoid M _ _) ``` ### Powers by products of natural numbers are iterated powers From 906c3fb059f557700d7b67fb336fef916c093875 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 12:21:35 -0700 Subject: [PATCH 19/22] Progress --- src/elementary-number-theory.lagda.md | 2 + .../absolute-value-rational-numbers.lagda.md | 14 +- ...lity-nonnegative-rational-numbers.lagda.md | 8 + ...d-of-nonnegative-rational-numbers.lagda.md | 55 ++++ ...cative-monoid-of-rational-numbers.lagda.md | 4 +- .../nonnegative-rational-numbers.lagda.md | 3 + .../parity-natural-numbers.lagda.md | 9 + ...wers-nonnegative-rational-numbers.lagda.md | 146 ++++++++++ .../powers-positive-rational-numbers.lagda.md | 10 +- .../powers-rational-numbers.lagda.md | 258 +++++++++++++++--- ...lity-nonnegative-rational-numbers.lagda.md | 22 ++ .../submonoids-commutative-monoids.lagda.md | 5 +- src/group-theory/submonoids.lagda.md | 6 +- 13 files changed, 495 insertions(+), 47 deletions(-) create mode 100644 src/elementary-number-theory/multiplicative-monoid-of-nonnegative-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 0e518ce0112..6655218d7ca 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -148,6 +148,7 @@ open import elementary-number-theory.multiplicative-group-of-positive-rational-n open import elementary-number-theory.multiplicative-group-of-rational-numbers public open import elementary-number-theory.multiplicative-inverses-positive-integer-fractions public open import elementary-number-theory.multiplicative-monoid-of-natural-numbers public +open import elementary-number-theory.multiplicative-monoid-of-nonnegative-rational-numbers public open import elementary-number-theory.multiplicative-monoid-of-rational-numbers public open import elementary-number-theory.multiplicative-units-integers public open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public @@ -178,6 +179,7 @@ open import elementary-number-theory.positive-integer-fractions public open import elementary-number-theory.positive-integers public open import elementary-number-theory.positive-rational-numbers public open import elementary-number-theory.powers-integers public +open import elementary-number-theory.powers-nonnegative-rational-numbers public open import elementary-number-theory.powers-of-two public open import elementary-number-theory.powers-positive-rational-numbers public open import elementary-number-theory.powers-rational-numbers public diff --git a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md index fa1c1a6995c..4b0ad01d885 100644 --- a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md +++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md @@ -174,13 +174,15 @@ abstract ( neg-neg-ℚ q) ( neg-leq-ℚ (neg-leq-abs-ℚ q))) + rational-abs-zero-ℚ : rational-abs-ℚ zero-ℚ = zero-ℚ + rational-abs-zero-ℚ = + equational-reasoning + max-ℚ zero-ℚ (neg-ℚ zero-ℚ) + = max-ℚ zero-ℚ zero-ℚ by ap-max-ℚ refl neg-zero-ℚ + = zero-ℚ by idempotent-max-ℚ zero-ℚ + abs-zero-ℚ : abs-ℚ zero-ℚ = zero-ℚ⁰⁺ - abs-zero-ℚ = - eq-ℚ⁰⁺ - ( equational-reasoning - max-ℚ zero-ℚ (neg-ℚ zero-ℚ) - = max-ℚ zero-ℚ zero-ℚ by ap-max-ℚ refl neg-zero-ℚ - = zero-ℚ by idempotent-max-ℚ zero-ℚ) + abs-zero-ℚ = eq-ℚ⁰⁺ rational-abs-zero-ℚ ``` ### The triangle inequality diff --git a/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md index 7ec428e6cf1..a78e7658d87 100644 --- a/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md @@ -51,3 +51,11 @@ decidable-total-order-ℚ⁰⁺ = ℚ-Decidable-Total-Order is-nonnegative-prop-ℚ ``` + +### Inequality on the nonnegative rational numbers is transitive + +```agda +abstract + transitive-leq-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → leq-ℚ⁰⁺ q r → leq-ℚ⁰⁺ p q → leq-ℚ⁰⁺ p r + transitive-leq-ℚ⁰⁺ (p , _) (q , _) (r , _) = transitive-leq-ℚ p q r +``` diff --git a/src/elementary-number-theory/multiplicative-monoid-of-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-monoid-of-nonnegative-rational-numbers.lagda.md new file mode 100644 index 00000000000..da8d59e5b14 --- /dev/null +++ b/src/elementary-number-theory/multiplicative-monoid-of-nonnegative-rational-numbers.lagda.md @@ -0,0 +1,55 @@ +# The multiplicative monoid of nonnegative rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.multiplicative-monoid-of-nonnegative-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.multiplication-nonnegative-rational-numbers +open import elementary-number-theory.multiplicative-monoid-of-rational-numbers +open import elementary-number-theory.nonnegative-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import group-theory.commutative-monoids +open import group-theory.monoids +open import group-theory.submonoids-commutative-monoids +``` + +
+ +## Idea + +The type of +[nonnegative](elementary-number-theory.nonnegative-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md) equipped with +[multiplication](elementary-number-theory.multiplication-nonnegative-rational-numbers.md) +is a [commutative monoid](group-theory.commutative-monoids.md) with unit +`one-ℚ⁰⁺`. + +## Definitions + +### The multiplicative commutative monoid of nonnegative rational numbers + +```agda +nonnegative-submonoid-commutative-monoid-mul-ℚ : + Commutative-Submonoid lzero commutative-monoid-mul-ℚ +nonnegative-submonoid-commutative-monoid-mul-ℚ = + ( is-nonnegative-prop-ℚ , + is-nonnegative-one-ℚ , + λ _ _ → is-nonnegative-mul-ℚ) + +commutative-monoid-mul-ℚ⁰⁺ : Commutative-Monoid lzero +commutative-monoid-mul-ℚ⁰⁺ = + commutative-monoid-Commutative-Submonoid + ( commutative-monoid-mul-ℚ) + ( nonnegative-submonoid-commutative-monoid-mul-ℚ) + +monoid-mul-ℚ⁰⁺ : Monoid lzero +monoid-mul-ℚ⁰⁺ = monoid-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ +``` diff --git a/src/elementary-number-theory/multiplicative-monoid-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-monoid-of-rational-numbers.lagda.md index 781ac3df4c6..a3ac5b301d7 100644 --- a/src/elementary-number-theory/multiplicative-monoid-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-monoid-of-rational-numbers.lagda.md @@ -27,8 +27,8 @@ open import group-theory.semigroups The type of [rational numbers](elementary-number-theory.rational-numbers.md) equipped with -[multiplication](elementary-number-theory.addition-rational-numbers.md) is a -[commutative monoid](group-theory.commutative-monoids.md) with unit `one-ℚ`. +[multiplication](elementary-number-theory.multiplication-rational-numbers.md) is +a [commutative monoid](group-theory.commutative-monoids.md) with unit `one-ℚ`. ## Definitions diff --git a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md index b7d23dc65ad..f16ddf889fb 100644 --- a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md +++ b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md @@ -166,6 +166,9 @@ zero-ℚ⁰⁺ = nonnegative-rational-ℕ zero-ℕ one-ℚ⁰⁺ : ℚ⁰⁺ one-ℚ⁰⁺ = nonnegative-rational-ℕ 1 + +is-nonnegative-one-ℚ : is-nonnegative-ℚ one-ℚ +is-nonnegative-one-ℚ = is-nonnegative-rational-ℕ 1 ``` ### The rational image of a nonnegative integer fraction is nonnegative diff --git a/src/elementary-number-theory/parity-natural-numbers.lagda.md b/src/elementary-number-theory/parity-natural-numbers.lagda.md index 9fa410e7f87..5a7c82123c1 100644 --- a/src/elementary-number-theory/parity-natural-numbers.lagda.md +++ b/src/elementary-number-theory/parity-natural-numbers.lagda.md @@ -12,6 +12,7 @@ open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers open import foundation.action-on-identifications-functions open import foundation.decidable-types @@ -69,6 +70,14 @@ is-odd-one-ℕ : is-odd-ℕ 1 is-odd-one-ℕ H = Eq-eq-ℕ (is-one-div-one-ℕ 2 H) ``` +### An odd natural number is nonzero + +```agda +abstract + is-nonzero-is-odd-ℕ : {n : ℕ} → is-odd-ℕ n → is-nonzero-ℕ n + is-nonzero-is-odd-ℕ odd-n refl = odd-n is-even-zero-ℕ +``` + ### A natural number `x` is even if and only if `x + 2` is even ```agda diff --git a/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md new file mode 100644 index 00000000000..9ad7fa97c80 --- /dev/null +++ b/src/elementary-number-theory/powers-nonnegative-rational-numbers.lagda.md @@ -0,0 +1,146 @@ +# Powers of nonnegative rational numbers + +```agda +module elementary-number-theory.powers-nonnegative-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers +open import elementary-number-theory.inequality-nonnegative-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-nonnegative-rational-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplicative-monoid-of-nonnegative-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-nonnegative-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.identity-types + +open import group-theory.powers-of-elements-commutative-monoids +open import group-theory.powers-of-elements-monoids +``` + +
+ +## Idea + +The +{{#concept "power operation" Disambiguation="a nonnegative rational number to a natural number power" Agda=power-ℚ⁰⁺}} +on the [nonnegative](elementary-number-theory.nonnegative-rational-numbers.md) +[rational numbers](elementary-number-theory.rational-numbers.md) is the +operation `n x ↦ xⁿ`, which is defined by +[iteratively](foundation.iterating-functions.md) multiplying `x` with itself `n` +times. This file covers the case where `n` is a +[natural number](elementary-number-theory.natural-numbers.md). + +## Definition + +```agda +power-ℚ⁰⁺ : ℕ → ℚ⁰⁺ → ℚ⁰⁺ +power-ℚ⁰⁺ = power-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ +``` + +## Properties + +### `1ⁿ = 1` + +```agda +power-one-ℚ⁰⁺ : (n : ℕ) → power-ℚ⁰⁺ n one-ℚ⁰⁺ = one-ℚ⁰⁺ +power-one-ℚ⁰⁺ = power-unit-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ +``` + +### `qⁿ⁺¹ = qⁿq` + +```agda +power-succ-ℚ⁰⁺ : + (n : ℕ) (q : ℚ⁰⁺) → power-ℚ⁰⁺ (succ-ℕ n) q = power-ℚ⁰⁺ n q *ℚ⁰⁺ q +power-succ-ℚ⁰⁺ = power-succ-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ +``` + +### `qⁿ = qqⁿ` + +```agda +power-succ-ℚ⁰⁺' : + (n : ℕ) (q : ℚ⁰⁺) → power-ℚ⁰⁺ (succ-ℕ n) q = q *ℚ⁰⁺ power-ℚ⁰⁺ n q +power-succ-ℚ⁰⁺' = power-succ-Commutative-Monoid' commutative-monoid-mul-ℚ⁰⁺ +``` + +### `qᵐ⁺ⁿ = qᵐqⁿ` + +```agda +abstract + distributive-power-add-ℚ⁰⁺ : + (m n : ℕ) (q : ℚ⁰⁺) → + power-ℚ⁰⁺ (m +ℕ n) q = power-ℚ⁰⁺ m q *ℚ⁰⁺ power-ℚ⁰⁺ n q + distributive-power-add-ℚ⁰⁺ m n _ = + distributive-power-add-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ m n +``` + +### `(pq)ⁿ=pⁿqⁿ` + +```agda +abstract + left-distributive-power-mul-ℚ⁰⁺ : + (n : ℕ) (p q : ℚ⁰⁺) → + power-ℚ⁰⁺ n (p *ℚ⁰⁺ q) = power-ℚ⁰⁺ n p *ℚ⁰⁺ power-ℚ⁰⁺ n q + left-distributive-power-mul-ℚ⁰⁺ n p q = + distributive-power-mul-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ n +``` + +### `pᵐⁿ = (pᵐ)ⁿ` + +```agda +power-mul-ℚ⁰⁺ : + (m n : ℕ) (q : ℚ⁰⁺) → power-ℚ⁰⁺ (m *ℕ n) q = power-ℚ⁰⁺ n (power-ℚ⁰⁺ m q) +power-mul-ℚ⁰⁺ m n q = + power-mul-Commutative-Monoid commutative-monoid-mul-ℚ⁰⁺ m n +``` + +### If `p` and `q` are nonnegative rational numbers with `p < q` and `n` is nonzero, `pⁿ < qⁿ` + +```agda +abstract + preserves-le-power-ℚ⁰⁺ : + (n : ℕ) → is-nonzero-ℕ n → (p q : ℚ⁰⁺) → le-ℚ⁰⁺ p q → + le-ℚ⁰⁺ (power-ℚ⁰⁺ n p) (power-ℚ⁰⁺ n q) + preserves-le-power-ℚ⁰⁺ 0 H p q pImports ```agda +open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -37,3 +38,24 @@ le-prop-ℚ⁰⁺ p q = le-ℚ-Prop (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q le-ℚ⁰⁺ : (p q : ℚ⁰⁺) → UU lzero le-ℚ⁰⁺ p q = type-Prop (le-prop-ℚ⁰⁺ p q) ``` + +## Properties + +### Strict inequality on the nonnegative rational numbers is transitive + +```agda +abstract + transitive-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p q → le-ℚ⁰⁺ p r + transitive-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = transitive-le-ℚ p q r +``` + +### Concatenation laws with inequality + +```agda +abstract + concatenate-le-leq-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ p q → leq-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r + concatenate-le-leq-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-le-leq-ℚ p q r + + concatenate-leq-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → leq-ℚ⁰⁺ p q → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r + concatenate-leq-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-leq-le-ℚ p q r +``` diff --git a/src/group-theory/submonoids-commutative-monoids.lagda.md b/src/group-theory/submonoids-commutative-monoids.lagda.md index 1b93a31af20..6734dc7ba91 100644 --- a/src/group-theory/submonoids-commutative-monoids.lagda.md +++ b/src/group-theory/submonoids-commutative-monoids.lagda.md @@ -27,7 +27,10 @@ open import group-theory.subsets-commutative-monoids ## Idea -A submonoid of a commutative monoid `M` is a subset of `M` that contains the +A +{{#concept "submonoid" Disambiguation="of a commutative monoid" Agda=Commutative-Submonoid}} +of a [commutative monoid](group-theory.commutative-monoids.md) `M` is a +[subset](group-theory.subsets-commutative-monoids.md) of `M` that contains the unit of `M` and is closed under multiplication. ## Definitions diff --git a/src/group-theory/submonoids.lagda.md b/src/group-theory/submonoids.lagda.md index 4245b22e102..28dacdedee4 100644 --- a/src/group-theory/submonoids.lagda.md +++ b/src/group-theory/submonoids.lagda.md @@ -27,8 +27,10 @@ open import group-theory.subsets-monoids ## Idea -A submonoid of a monoid `M` is a subset of `M` that contains the unit of `M` and -is closed under multiplication. +A {{#concept "submonoid" WDID=Q121499459 WD="submonoid" Agda=Submonoid}} of a +[monoid](group-theory.monoids.md) `M` is a +[subset](group-theory.subsets-monoids.md) of `M` that contains the unit of `M` +and is closed under multiplication. ## Definitions From 92b42a5ad47796ab1923535a41077a5cdc97a22c Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 12:37:31 -0700 Subject: [PATCH 20/22] Correct superscripts --- src/elementary-number-theory/powers-rational-numbers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/powers-rational-numbers.lagda.md b/src/elementary-number-theory/powers-rational-numbers.lagda.md index 1374740c371..392ea1998cf 100644 --- a/src/elementary-number-theory/powers-rational-numbers.lagda.md +++ b/src/elementary-number-theory/powers-rational-numbers.lagda.md @@ -93,7 +93,7 @@ abstract power-one-ℚ = power-unit-Monoid monoid-mul-ℚ ``` -### `qⁿ¹ = qⁿq` +### `qⁿ⁺¹ = qⁿq` ```agda abstract @@ -101,7 +101,7 @@ abstract power-succ-ℚ = power-succ-Monoid monoid-mul-ℚ ``` -### `qⁿ = qqⁿ` +### `qⁿ⁺¹ = qqⁿ` ```agda abstract From 978b5045b61f96dfd1b8dc09145956ea5da15ce8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 15:47:48 -0700 Subject: [PATCH 21/22] Progress --- ...of-elements-commutative-semirings.lagda.md | 15 ++ ...icative-group-of-rational-numbers.lagda.md | 21 ++ .../arithmetic-sequences-semigroups.lagda.md | 27 +++ src/lists/sequences.lagda.md | 9 + src/ring-theory.lagda.md | 1 + .../geometric-sequences-rings.lagda.md | 216 ++++++++++++++++++ .../geometric-sequences-semirings.lagda.md | 36 ++- 7 files changed, 323 insertions(+), 2 deletions(-) create mode 100644 src/ring-theory/geometric-sequences-rings.lagda.md diff --git a/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md b/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md index 0bda772d1a1..a5727d03a8e 100644 --- a/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md +++ b/src/commutative-algebra/powers-of-elements-commutative-semirings.lagda.md @@ -51,6 +51,21 @@ module _ power-succ-Semiring (semiring-Commutative-Semiring A) ``` +### `xⁿ⁺¹ = xxⁿ` + +```agda +module _ + {l : Level} (A : Commutative-Semiring l) + where + + power-succ-Commutative-Semiring' : + (n : ℕ) (x : type-Commutative-Semiring A) → + power-Commutative-Semiring A (succ-ℕ n) x = + mul-Commutative-Semiring A x (power-Commutative-Semiring A n x) + power-succ-Commutative-Semiring' = + power-succ-Semiring' (semiring-Commutative-Semiring A) +``` + ### Powers by sums of natural numbers are products of powers ```agda diff --git a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md index 4db36a011c9..a35af131e80 100644 --- a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md @@ -10,8 +10,10 @@ module elementary-number-theory.multiplicative-group-of-rational-numbers where ```agda open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-rational-numbers +open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers @@ -25,6 +27,7 @@ open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.function-types +open import foundation.negated-equality open import foundation.identity-types open import foundation.subtypes open import foundation.transport-along-identifications @@ -86,6 +89,9 @@ _*ℚˣ_ = mul-ℚˣ inv-ℚˣ : ℚˣ → ℚˣ inv-ℚˣ = inv-group-of-units-Ring ring-ℚ + +rational-inv-ℚˣ : ℚˣ → ℚ +rational-inv-ℚˣ q = rational-ℚˣ (inv-ℚˣ q) ``` ### Inverse laws in the multiplicative group of rational numbers @@ -169,3 +175,18 @@ invertible-ℚ⁺ = invertible-nonzero-ℚ ∘ nonzero-ℚ⁺ invertible-ℚ⁻ : ℚ⁻ → ℚˣ invertible-ℚ⁻ = invertible-nonzero-ℚ ∘ nonzero-ℚ⁻ ``` + +### If `a ≠ b`, `b - a` is invertible + +```agda +abstract + is-invertible-diff-neq-ℚ : + (a b : ℚ) → a ≠ b → is-invertible-element-Ring ring-ℚ (b -ℚ a) + is-invertible-diff-neq-ℚ a b a≠b = + is-invertible-element-ring-is-nonzero-ℚ + ( b -ℚ a) + ( λ b-a=0 → a≠b (inv (eq-is-unit-right-div-Group group-add-ℚ b-a=0))) + +invertible-diff-neq-ℚ : (a b : ℚ) → a ≠ b → ℚˣ +invertible-diff-neq-ℚ a b a≠b = (b -ℚ a , is-invertible-diff-neq-ℚ a b a≠b) +``` diff --git a/src/group-theory/arithmetic-sequences-semigroups.lagda.md b/src/group-theory/arithmetic-sequences-semigroups.lagda.md index f58aa8571c4..0238c5bd311 100644 --- a/src/group-theory/arithmetic-sequences-semigroups.lagda.md +++ b/src/group-theory/arithmetic-sequences-semigroups.lagda.md @@ -13,6 +13,7 @@ open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.homotopies open import foundation.identity-types open import foundation.propositions @@ -188,6 +189,32 @@ module _ ( refl) ``` +### The tail of a standard arithmetic sequence is another standard arithmetic sequence + +```agda +module _ + {l : Level} (G : Semigroup l) (a d : type-Semigroup G) + where + + abstract + htpy-tail-standard-arithmetric-sequence-Semigroup : + tail-sequence + ( seq-standard-arithmetic-sequence-Semigroup G a d) ~ + seq-standard-arithmetic-sequence-Semigroup G (mul-Semigroup G a d) d + htpy-tail-standard-arithmetric-sequence-Semigroup 0 = refl + htpy-tail-standard-arithmetric-sequence-Semigroup (succ-ℕ n) = + ap-mul-Semigroup G + ( htpy-tail-standard-arithmetric-sequence-Semigroup n) + ( refl) + + eq-tail-standard-arithmetric-sequence-Semigroup : + tail-sequence + ( seq-standard-arithmetic-sequence-Semigroup G a d) = + seq-standard-arithmetic-sequence-Semigroup G (mul-Semigroup G a d) d + eq-tail-standard-arithmetric-sequence-Semigroup = + eq-htpy htpy-tail-standard-arithmetric-sequence-Semigroup +``` + ## External links - [Arithmetic progressions](https://en.wikipedia.org/wiki/Arithmetic_progression) diff --git a/src/lists/sequences.lagda.md b/src/lists/sequences.lagda.md index 2549a666e11..a09c39a608b 100644 --- a/src/lists/sequences.lagda.md +++ b/src/lists/sequences.lagda.md @@ -7,6 +7,8 @@ module lists.sequences where
Imports ```agda +open import elementary-number-theory.natural-numbers + open import foundation.universe-levels open import foundation-core.function-types @@ -36,6 +38,13 @@ sequence : {l : Level} → UU l → UU l sequence A = dependent-sequence (λ _ → A) ``` +### The tail of a sequence + +```agda +tail-sequence : {l : Level} {A : UU l} → sequence A → sequence A +tail-sequence u n = u (succ-ℕ n) +``` + ### Functorial action on maps of sequences ```agda diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md index a16c402dafa..7322fd40478 100644 --- a/src/ring-theory.lagda.md +++ b/src/ring-theory.lagda.md @@ -29,6 +29,7 @@ open import ring-theory.full-ideals-rings public open import ring-theory.function-rings public open import ring-theory.function-semirings public open import ring-theory.generating-elements-rings public +open import ring-theory.geometric-sequences-rings public open import ring-theory.geometric-sequences-semirings public open import ring-theory.groups-of-units-rings public open import ring-theory.homomorphisms-cyclic-rings public diff --git a/src/ring-theory/geometric-sequences-rings.lagda.md b/src/ring-theory/geometric-sequences-rings.lagda.md new file mode 100644 index 00000000000..90497c4db21 --- /dev/null +++ b/src/ring-theory/geometric-sequences-rings.lagda.md @@ -0,0 +1,216 @@ +# Geometric sequences in rings + +```agda +module ring-theory.geometric-sequences-rings where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.arithmetic-sequences-semigroups + +open import lists.sequences + +open import ring-theory.geometric-sequences-semirings +open import ring-theory.powers-of-elements-rings +open import ring-theory.rings +``` + +
+ +## Ideas + +A +{{#concept "geometric sequence" Disambiguation="in a ring" Agda=geometric-sequence-Ring}} +in a [ring](ring-theory.semirings.md) is an +[arithmetic sequence](ring-theory.geometric-sequence-semirings.md) in the +underlying [semiring](ring-theory.semirings.md). + +These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the +semiring. + +## Definitions + +### Geometric sequences in rings + +```agda +module _ + {l : Level} (R : Ring l) + where + + geometric-sequence-Ring : UU l + geometric-sequence-Ring = + geometric-sequence-Semiring (semiring-Ring R) + +module _ + {l : Level} (R : Ring l) + (u : geometric-sequence-Ring R) + where + + seq-geometric-sequence-Ring : ℕ → type-Ring R + seq-geometric-sequence-Ring = + seq-geometric-sequence-Semiring (semiring-Ring R) u + + common-ratio-geometric-sequence-Ring : type-Ring R + common-ratio-geometric-sequence-Ring = + common-ratio-geometric-sequence-Semiring (semiring-Ring R) u + + is-common-ratio-geometric-sequence-Ring : + ( n : ℕ) → + ( seq-geometric-sequence-Ring (succ-ℕ n)) = + ( mul-Ring + ( R) + ( seq-geometric-sequence-Ring n) + ( common-ratio-geometric-sequence-Ring)) + is-common-ratio-geometric-sequence-Ring = + is-common-difference-arithmetic-sequence-Semigroup + ( multiplicative-semigroup-Ring R) + ( u) + + initial-term-geometric-sequence-Ring : type-Ring R + initial-term-geometric-sequence-Ring = + initial-term-arithmetic-sequence-Semigroup + ( multiplicative-semigroup-Ring R) + ( u) +``` + +### The standard geometric sequences in a semiring + +The standard geometric sequence with initial term `a` and common factor `r` is +the sequence `u` defined by: + +- `u₀ = a` +- `uₙ₊₁ = uₙ * r` + +```agda +module _ + {l : Level} (R : Ring l) (a r : type-Ring R) + where + + standard-geometric-sequence-Ring : geometric-sequence-Ring R + standard-geometric-sequence-Ring = + standard-arithmetic-sequence-Semigroup + ( multiplicative-semigroup-Ring R) + ( a) + ( r) + + seq-standard-geometric-sequence-Ring : ℕ → type-Ring R + seq-standard-geometric-sequence-Ring = + seq-geometric-sequence-Ring R + standard-geometric-sequence-Ring +``` + +### The geometric sequences `n ↦ a * rⁿ` + +```agda +module _ + {l : Level} (R : Ring l) (a r : type-Ring R) + where + + mul-pow-nat-Ring : sequence (type-Ring R) + mul-pow-nat-Ring = mul-pow-nat-Semiring (semiring-Ring R) a r + + geometric-mul-pow-nat-Ring : geometric-sequence-Ring R + geometric-mul-pow-nat-Ring = + geometric-mul-pow-nat-Semiring (semiring-Ring R) a r + + initial-term-mul-pow-nat-Ring : type-Ring R + initial-term-mul-pow-nat-Ring = + initial-term-mul-pow-nat-Semiring (semiring-Ring R) a r + + eq-initial-term-mul-pow-nat-Ring : + initial-term-mul-pow-nat-Ring = a + eq-initial-term-mul-pow-nat-Ring = + eq-initial-term-mul-pow-nat-Semiring (semiring-Ring R) a r +``` + +## Properties + +### Any geometric sequence in a semiring is homotopic to a standard geometric sequence + +```agda +module _ + {l : Level} (R : Ring l) + (u : geometric-sequence-Ring R) + where + + htpy-seq-standard-geometric-sequence-Ring : + ( seq-geometric-sequence-Ring R + ( standard-geometric-sequence-Ring R + ( initial-term-geometric-sequence-Ring R u) + ( common-ratio-geometric-sequence-Ring R u))) ~ + ( seq-geometric-sequence-Ring R u) + htpy-seq-standard-geometric-sequence-Ring = + htpy-seq-standard-arithmetic-sequence-Semigroup + ( multiplicative-semigroup-Ring R) + ( u) +``` + +### The nth term of an geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` + +```agda +module _ + {l : Level} (R : Ring l) (a r : type-Ring R) + where + + htpy-mul-pow-standard-geometric-sequence-Ring : + mul-pow-nat-Ring R a r ~ seq-standard-geometric-sequence-Ring R a r + htpy-mul-pow-standard-geometric-sequence-Ring = + htpy-mul-pow-standard-geometric-sequence-Semiring (semiring-Ring R) a r +``` + +```agda +module _ + {l : Level} (R : Ring l) (u : geometric-sequence-Ring R) + where + + htpy-mul-pow-geometric-sequence-Ring : + mul-pow-nat-Ring + ( R) + ( initial-term-geometric-sequence-Ring R u) + ( common-ratio-geometric-sequence-Ring R u) ~ + seq-geometric-sequence-Ring R u + htpy-mul-pow-geometric-sequence-Ring = + htpy-mul-pow-geometric-sequence-Semiring (semiring-Ring R) u +``` + +### Constant sequences are geometric with common ratio one + +```agda +module _ + {l : Level} (R : Ring l) (a : type-Ring R) + where + + one-is-common-ratio-const-sequence-Ring : + is-common-difference-sequence-Semigroup + ( multiplicative-semigroup-Ring R) + ( λ _ → a) + ( one-Ring R) + one-is-common-ratio-const-sequence-Ring n = + inv (right-unit-law-mul-Ring R a) + + geometric-const-sequence-Ring : geometric-sequence-Ring R + geometric-const-sequence-Ring = + geometric-const-sequence-Semiring (semiring-Ring R) a +``` + +## See also + +- [Geometric sequences in a semiring](ring-theory.geometric-sequences-semirings.md) + +## External links + +- [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression) + at Wikipedia diff --git a/src/ring-theory/geometric-sequences-semirings.lagda.md b/src/ring-theory/geometric-sequences-semirings.lagda.md index 2b0107a2dbd..3d7dff3e3ac 100644 --- a/src/ring-theory/geometric-sequences-semirings.lagda.md +++ b/src/ring-theory/geometric-sequences-semirings.lagda.md @@ -13,6 +13,7 @@ open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.homotopies open import foundation.identity-types open import foundation.propositions @@ -54,6 +55,11 @@ module _ arithmetic-sequence-Semigroup ( multiplicative-semigroup-Semiring R) + is-geometric-sequence-Semiring : sequence (type-Semiring R) → UU l + is-geometric-sequence-Semiring = + is-arithmetic-sequence-Semigroup + ( multiplicative-semigroup-Semiring R) + module _ {l : Level} (R : Semiring l) (u : geometric-sequence-Semiring R) @@ -66,8 +72,8 @@ module _ ( u) is-geometric-seq-geometric-sequence-Semiring : - is-arithmetic-sequence-Semigroup - ( multiplicative-semigroup-Semiring R) + is-geometric-sequence-Semiring + ( R) ( seq-geometric-sequence-Semiring) is-geometric-seq-geometric-sequence-Semiring = is-arithmetic-seq-arithmetic-sequence-Semigroup @@ -267,6 +273,32 @@ module _ ( one-Semiring R , one-is-common-ratio-const-sequence-Semiring) ``` +### The tail of a standard geometric sequence is another standard geometric sequence + +```agda +module _ + {l : Level} (R : Semiring l) (a r : type-Semiring R) + where + + abstract + htpy-tail-standard-geometric-sequence-Semiring : + tail-sequence + ( seq-standard-geometric-sequence-Semiring R a r) ~ + seq-standard-geometric-sequence-Semiring R (mul-Semiring R a r) r + htpy-tail-standard-geometric-sequence-Semiring = + htpy-tail-standard-arithmetric-sequence-Semigroup + ( multiplicative-semigroup-Semiring R) + ( a) + ( r) + + eq-tail-standard-geometric-sequence-Semiring : + tail-sequence + ( seq-standard-geometric-sequence-Semiring R a r) = + seq-standard-geometric-sequence-Semiring R (mul-Semiring R a r) r + eq-tail-standard-geometric-sequence-Semiring = + eq-htpy htpy-tail-standard-geometric-sequence-Semiring +``` + ## External links - [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression) From e332e1993006ccbeed9f7b35f0e8499bc429155c Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 17 Oct 2025 16:26:05 -0700 Subject: [PATCH 22/22] Sums of geometric series for rational numbers --- src/commutative-algebra.lagda.md | 2 + ...etric-sequences-commutative-rings.lagda.md | 311 +++++++++++++ ...c-sequences-commutative-semirings.lagda.md | 439 ++++++++++++++++++ src/elementary-number-theory.lagda.md | 1 + ...metric-sequences-rational-numbers.lagda.md | 203 ++++++++ ...icative-group-of-rational-numbers.lagda.md | 23 +- .../geometric-sequences-rings.lagda.md | 2 +- .../geometric-sequences-semirings.lagda.md | 2 +- 8 files changed, 978 insertions(+), 5 deletions(-) create mode 100644 src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md create mode 100644 src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md create mode 100644 src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md index 0ca53e325c4..801d517bd88 100644 --- a/src/commutative-algebra.lagda.md +++ b/src/commutative-algebra.lagda.md @@ -22,6 +22,8 @@ open import commutative-algebra.formal-power-series-commutative-semirings public open import commutative-algebra.full-ideals-commutative-rings public open import commutative-algebra.function-commutative-rings public open import commutative-algebra.function-commutative-semirings public +open import commutative-algebra.geometric-sequences-commutative-rings public +open import commutative-algebra.geometric-sequences-commutative-semirings public open import commutative-algebra.groups-of-units-commutative-rings public open import commutative-algebra.homomorphisms-commutative-rings public open import commutative-algebra.homomorphisms-commutative-semirings public diff --git a/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md new file mode 100644 index 00000000000..ee6b868c9e9 --- /dev/null +++ b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md @@ -0,0 +1,311 @@ +# Geometric sequences in commutative rings + +```agda +module commutative-algebra.geometric-sequences-commutative-rings where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-rings +open import commutative-algebra.commutative-semirings +open import commutative-algebra.geometric-sequences-commutative-semirings +open import commutative-algebra.powers-of-elements-commutative-rings + +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.arithmetic-sequences-semigroups + +open import lists.finite-sequences +open import lists.sequences +``` + +
+ +## Ideas + +A +{{#concept "geometric sequence" Disambiguation="in a commutative semiring" Agda=geometric-sequence-Commutative-Ring}} +in a [semiring](ring-theory.semirings.md) is an +[geometric sequence](ring-theory.geometric-sequences-semirings.md) in the +semiring multiplicative [semigroup](group-theory.semigroups.md). + +These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the +semiring. + +## Definitions + +### Geometric sequences in semirings + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + geometric-sequence-Commutative-Ring : UU l + geometric-sequence-Commutative-Ring = + geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + is-geometric-sequence-Commutative-Ring : + sequence (type-Commutative-Ring R) → UU l + is-geometric-sequence-Commutative-Ring = + is-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + +module _ + {l : Level} (R : Commutative-Ring l) + (u : geometric-sequence-Commutative-Ring R) + where + + seq-geometric-sequence-Commutative-Ring : ℕ → type-Commutative-Ring R + seq-geometric-sequence-Commutative-Ring = + seq-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) + + is-geometric-seq-geometric-sequence-Commutative-Ring : + is-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( seq-geometric-sequence-Commutative-Ring) + is-geometric-seq-geometric-sequence-Commutative-Ring = + is-geometric-seq-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) + + common-ratio-geometric-sequence-Commutative-Ring : + type-Commutative-Ring R + common-ratio-geometric-sequence-Commutative-Ring = + common-ratio-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) + + is-common-ratio-geometric-sequence-Commutative-Ring : + ( n : ℕ) → + ( seq-geometric-sequence-Commutative-Ring (succ-ℕ n)) = + ( mul-Commutative-Ring + ( R) + ( seq-geometric-sequence-Commutative-Ring n) + ( common-ratio-geometric-sequence-Commutative-Ring)) + is-common-ratio-geometric-sequence-Commutative-Ring = + is-common-ratio-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) + + initial-term-geometric-sequence-Commutative-Ring : + type-Commutative-Ring R + initial-term-geometric-sequence-Commutative-Ring = + initial-term-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) +``` + +### The standard geometric sequences in a semiring + +The standard geometric sequence with initial term `a` and common factor `r` is +the sequence `u` defined by: + +- `u₀ = a` +- `uₙ₊₁ = uₙ * r` + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R) + where + + standard-geometric-sequence-Commutative-Ring : + geometric-sequence-Commutative-Ring R + standard-geometric-sequence-Commutative-Ring = + standard-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) + ( r) + + seq-standard-geometric-sequence-Commutative-Ring : + ℕ → type-Commutative-Ring R + seq-standard-geometric-sequence-Commutative-Ring = + seq-geometric-sequence-Commutative-Ring R + standard-geometric-sequence-Commutative-Ring + + is-geometric-standard-geometric-sequence-Commutative-Ring : + is-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( seq-standard-geometric-sequence-Commutative-Ring) + is-geometric-standard-geometric-sequence-Commutative-Ring = + is-geometric-seq-geometric-sequence-Commutative-Ring R + standard-geometric-sequence-Commutative-Ring +``` + +### The geometric sequences `n ↦ a * rⁿ` + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R) + where + + mul-pow-nat-Commutative-Ring : ℕ → type-Commutative-Ring R + mul-pow-nat-Commutative-Ring n = + mul-Commutative-Ring R a (power-Commutative-Ring R n r) + + geometric-mul-pow-nat-Commutative-Ring : geometric-sequence-Commutative-Ring R + geometric-mul-pow-nat-Commutative-Ring = + geometric-mul-pow-nat-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) + ( r) + + initial-term-mul-pow-nat-Commutative-Ring : type-Commutative-Ring R + initial-term-mul-pow-nat-Commutative-Ring = + initial-term-geometric-sequence-Commutative-Ring + ( R) + ( geometric-mul-pow-nat-Commutative-Ring) + + eq-initial-term-mul-pow-nat-Commutative-Ring : + initial-term-mul-pow-nat-Commutative-Ring = a + eq-initial-term-mul-pow-nat-Commutative-Ring = + right-unit-law-mul-Commutative-Ring R a +``` + +## Properties + +### Any geometric sequence in a semiring is homotopic to a standard geometric sequence + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (u : geometric-sequence-Commutative-Ring R) + where + + htpy-seq-standard-geometric-sequence-Commutative-Ring : + ( seq-geometric-sequence-Commutative-Ring R + ( standard-geometric-sequence-Commutative-Ring R + ( initial-term-geometric-sequence-Commutative-Ring R u) + ( common-ratio-geometric-sequence-Commutative-Ring R u))) ~ + ( seq-geometric-sequence-Commutative-Ring R u) + htpy-seq-standard-geometric-sequence-Commutative-Ring = + htpy-seq-standard-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) +``` + +### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R) + where + + htpy-mul-pow-standard-geometric-sequence-Commutative-Ring : + mul-pow-nat-Commutative-Ring R a r ~ + seq-standard-geometric-sequence-Commutative-Ring R a r + htpy-mul-pow-standard-geometric-sequence-Commutative-Ring = + htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) + ( r) + + initial-term-standard-geometric-sequence-Commutative-Ring : + seq-standard-geometric-sequence-Commutative-Ring R a r 0 = a + initial-term-standard-geometric-sequence-Commutative-Ring = + ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Ring 0)) ∙ + ( eq-initial-term-mul-pow-nat-Commutative-Ring R a r) +``` + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (u : geometric-sequence-Commutative-Ring R) + where + + htpy-mul-pow-geometric-sequence-Commutative-Ring : + mul-pow-nat-Commutative-Ring + ( R) + ( initial-term-geometric-sequence-Commutative-Ring R u) + ( common-ratio-geometric-sequence-Commutative-Ring R u) ~ + seq-geometric-sequence-Commutative-Ring R u + htpy-mul-pow-geometric-sequence-Commutative-Ring n = + ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring + ( R) + ( initial-term-geometric-sequence-Commutative-Ring R u) + ( common-ratio-geometric-sequence-Commutative-Ring R u) + ( n)) ∙ + ( htpy-seq-standard-geometric-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( u) + ( n)) +``` + +### Constant sequences are geometric with common ratio one + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a : type-Commutative-Ring R) + where + + geometric-const-sequence-Commutative-Ring : + geometric-sequence-Commutative-Ring R + geometric-const-sequence-Commutative-Ring = + geometric-const-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) +``` + +### Finite geometric sequences + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R) + where + + standard-geometric-fin-sequence-Commutative-Ring : + (n : ℕ) → fin-sequence (type-Commutative-Ring R) n + standard-geometric-fin-sequence-Commutative-Ring = + fin-sequence-sequence + ( seq-standard-geometric-sequence-Commutative-Ring R a r) + + sum-standard-geometric-fin-sequence-Commutative-Ring : + (n : ℕ) → type-Commutative-Ring R + sum-standard-geometric-fin-sequence-Commutative-Ring = + sum-standard-geometric-fin-sequence-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) + ( r) +``` + +### The sum of a finite geometric sequence + +```agda +module _ + {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R) + where + + abstract + compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring : + (n : ℕ) → + sum-standard-geometric-fin-sequence-Commutative-Ring R + ( a) + ( r) + ( succ-ℕ n) = + add-Commutative-Ring R + ( a) + ( mul-Commutative-Ring R + ( r) + ( sum-standard-geometric-fin-sequence-Commutative-Ring R a r n)) + compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring = + compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( a) + ( r) +``` diff --git a/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md new file mode 100644 index 00000000000..821a30d43c3 --- /dev/null +++ b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md @@ -0,0 +1,439 @@ +# Geometric sequences in commutative semirings + +```agda +module commutative-algebra.geometric-sequences-commutative-semirings where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-semirings +open import commutative-algebra.powers-of-elements-commutative-semirings +open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semirings + +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.arithmetic-sequences-semigroups + +open import lists.finite-sequences +open import lists.sequences + +open import ring-theory.geometric-sequences-semirings +open import ring-theory.powers-of-elements-semirings +open import ring-theory.semirings + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Ideas + +A +{{#concept "geometric sequence" Disambiguation="in a commutative semiring" Agda=geometric-sequence-Commutative-Semiring}} +in a [semiring](ring-theory.semirings.md) is an +[geometric sequence](ring-theory.geometric-sequences-semirings.md) in the +semiring multiplicative [semigroup](group-theory.semigroups.md). + +These are sequences of the form `n ↦ a * rⁿ`, for elements `a`, `r` in the +semiring. + +## Definitions + +### Geometric sequences in semirings + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + geometric-sequence-Commutative-Semiring : UU l + geometric-sequence-Commutative-Semiring = + geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + + is-geometric-sequence-Commutative-Semiring : + sequence (type-Commutative-Semiring R) → UU l + is-geometric-sequence-Commutative-Semiring = + is-geometric-sequence-Semiring (semiring-Commutative-Semiring R) + +module _ + {l : Level} (R : Commutative-Semiring l) + (u : geometric-sequence-Commutative-Semiring R) + where + + seq-geometric-sequence-Commutative-Semiring : ℕ → type-Commutative-Semiring R + seq-geometric-sequence-Commutative-Semiring = + seq-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) + + is-geometric-seq-geometric-sequence-Commutative-Semiring : + is-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( seq-geometric-sequence-Commutative-Semiring) + is-geometric-seq-geometric-sequence-Commutative-Semiring = + is-geometric-seq-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) + + common-ratio-geometric-sequence-Commutative-Semiring : + type-Commutative-Semiring R + common-ratio-geometric-sequence-Commutative-Semiring = + common-ratio-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) + + is-common-ratio-geometric-sequence-Commutative-Semiring : + ( n : ℕ) → + ( seq-geometric-sequence-Commutative-Semiring (succ-ℕ n)) = + ( mul-Commutative-Semiring + ( R) + ( seq-geometric-sequence-Commutative-Semiring n) + ( common-ratio-geometric-sequence-Commutative-Semiring)) + is-common-ratio-geometric-sequence-Commutative-Semiring = + is-common-ratio-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) + + initial-term-geometric-sequence-Commutative-Semiring : + type-Commutative-Semiring R + initial-term-geometric-sequence-Commutative-Semiring = + initial-term-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) +``` + +### The standard geometric sequences in a semiring + +The standard geometric sequence with initial term `a` and common factor `r` is +the sequence `u` defined by: + +- `u₀ = a` +- `uₙ₊₁ = uₙ * r` + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R) + where + + standard-geometric-sequence-Commutative-Semiring : + geometric-sequence-Commutative-Semiring R + standard-geometric-sequence-Commutative-Semiring = + standard-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( a) + ( r) + + seq-standard-geometric-sequence-Commutative-Semiring : + ℕ → type-Commutative-Semiring R + seq-standard-geometric-sequence-Commutative-Semiring = + seq-geometric-sequence-Commutative-Semiring R + standard-geometric-sequence-Commutative-Semiring + + is-geometric-standard-geometric-sequence-Commutative-Semiring : + is-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( seq-standard-geometric-sequence-Commutative-Semiring) + is-geometric-standard-geometric-sequence-Commutative-Semiring = + is-geometric-seq-geometric-sequence-Commutative-Semiring R + standard-geometric-sequence-Commutative-Semiring +``` + +### The geometric sequences `n ↦ a * rⁿ` + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R) + where + + mul-pow-nat-Commutative-Semiring : ℕ → type-Commutative-Semiring R + mul-pow-nat-Commutative-Semiring n = + mul-Commutative-Semiring R a (power-Commutative-Semiring R n r) + + geometric-mul-pow-nat-Commutative-Semiring : + geometric-sequence-Commutative-Semiring R + geometric-mul-pow-nat-Commutative-Semiring = + geometric-mul-pow-nat-Semiring (semiring-Commutative-Semiring R) a r + + initial-term-mul-pow-nat-Commutative-Semiring : type-Commutative-Semiring R + initial-term-mul-pow-nat-Commutative-Semiring = + initial-term-geometric-sequence-Commutative-Semiring + ( R) + ( geometric-mul-pow-nat-Commutative-Semiring) + + eq-initial-term-mul-pow-nat-Commutative-Semiring : + initial-term-mul-pow-nat-Commutative-Semiring = a + eq-initial-term-mul-pow-nat-Commutative-Semiring = + right-unit-law-mul-Commutative-Semiring R a +``` + +## Properties + +### Any geometric sequence in a semiring is homotopic to a standard geometric sequence + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (u : geometric-sequence-Commutative-Semiring R) + where + + htpy-seq-standard-geometric-sequence-Commutative-Semiring : + ( seq-geometric-sequence-Commutative-Semiring R + ( standard-geometric-sequence-Commutative-Semiring R + ( initial-term-geometric-sequence-Commutative-Semiring R u) + ( common-ratio-geometric-sequence-Commutative-Semiring R u))) ~ + ( seq-geometric-sequence-Commutative-Semiring R u) + htpy-seq-standard-geometric-sequence-Commutative-Semiring = + htpy-seq-standard-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) +``` + +### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R) + where + + htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring : + mul-pow-nat-Commutative-Semiring R a r ~ + seq-standard-geometric-sequence-Commutative-Semiring R a r + htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring = + htpy-mul-pow-standard-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( a) + ( r) + + initial-term-standard-geometric-sequence-Commutative-Semiring : + seq-standard-geometric-sequence-Commutative-Semiring R a r 0 = a + initial-term-standard-geometric-sequence-Commutative-Semiring = + ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring 0)) ∙ + ( eq-initial-term-mul-pow-nat-Commutative-Semiring R a r) +``` + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (u : geometric-sequence-Commutative-Semiring R) + where + + htpy-mul-pow-geometric-sequence-Commutative-Semiring : + mul-pow-nat-Commutative-Semiring + ( R) + ( initial-term-geometric-sequence-Commutative-Semiring R u) + ( common-ratio-geometric-sequence-Commutative-Semiring R u) ~ + seq-geometric-sequence-Commutative-Semiring R u + htpy-mul-pow-geometric-sequence-Commutative-Semiring n = + ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring + ( R) + ( initial-term-geometric-sequence-Commutative-Semiring R u) + ( common-ratio-geometric-sequence-Commutative-Semiring R u) + ( n)) ∙ + ( htpy-seq-standard-geometric-sequence-Semiring + ( semiring-Commutative-Semiring R) + ( u) + ( n)) +``` + +### Constant sequences are geometric with common ratio one + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a : type-Commutative-Semiring R) + where + + geometric-const-sequence-Commutative-Semiring : + geometric-sequence-Commutative-Semiring R + geometric-const-sequence-Commutative-Semiring = + geometric-const-sequence-Semiring (semiring-Commutative-Semiring R) a +``` + +### Finite geometric sequences + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R) + where + + standard-geometric-fin-sequence-Commutative-Semiring : + (n : ℕ) → fin-sequence (type-Commutative-Semiring R) n + standard-geometric-fin-sequence-Commutative-Semiring = + fin-sequence-sequence + ( seq-standard-geometric-sequence-Commutative-Semiring R a r) + + sum-standard-geometric-fin-sequence-Commutative-Semiring : + (n : ℕ) → type-Commutative-Semiring R + sum-standard-geometric-fin-sequence-Commutative-Semiring n = + sum-fin-sequence-type-Commutative-Semiring R n + ( standard-geometric-fin-sequence-Commutative-Semiring n) +``` + +### The sum of a finite geometric sequence + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) (a r : type-Commutative-Semiring R) + where + + abstract + compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring : + (n : ℕ) → + sum-standard-geometric-fin-sequence-Commutative-Semiring R + ( a) + ( r) + ( succ-ℕ n) = + add-Commutative-Semiring R + ( a) + ( mul-Commutative-Semiring R + ( r) + ( sum-standard-geometric-fin-sequence-Commutative-Semiring R a r n)) + compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring n = + equational-reasoning + sum-standard-geometric-fin-sequence-Commutative-Semiring R + ( a) + ( r) + ( succ-ℕ n) + = + add-Commutative-Semiring R + ( term-Fin a r (succ-ℕ n) (zero-Fin n)) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → term-Fin a r (succ-ℕ n) (inr-Fin n i))) + by + snoc-sum-fin-sequence-type-Commutative-Semiring R n + ( standard-geometric-fin-sequence-Commutative-Semiring R + ( a) + ( r) + ( succ-ℕ n)) + ( refl) + = + add-Commutative-Semiring R + ( term a r 0) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → term a r (succ-ℕ (nat-Fin n i)))) + by + ap-add-Commutative-Semiring R + ( ap + ( seq-standard-geometric-sequence-Commutative-Semiring R a r) + ( is-zero-nat-zero-Fin {n})) + ( htpy-sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → ap (term a r) (nat-inr-Fin n i))) + = + add-Commutative-Semiring R + ( a) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + mul-Commutative-Semiring R + ( a) + ( power-Commutative-Semiring R (succ-ℕ (nat-Fin n i)) r))) + by + ap-add-Commutative-Semiring R + ( initial-term-standard-geometric-sequence-Commutative-Semiring + ( R) + ( a) + ( r)) + ( htpy-sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + inv + ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring + ( R) + ( a) + ( r) + ( succ-ℕ (nat-Fin n i))))) + = + add-Commutative-Semiring R + ( a) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + mul-Commutative-Semiring R + ( a) + ( mul-Commutative-Semiring R + ( r) + ( power-Commutative-Semiring R (nat-Fin n i) r)))) + by + ap-add-Commutative-Semiring R + ( refl) + ( htpy-sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + ap-mul-Commutative-Semiring R + ( refl) + ( power-succ-Commutative-Semiring' R (nat-Fin n i) r))) + = + add-Commutative-Semiring R + ( a) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + mul-Commutative-Semiring R + ( r) + ( mul-Commutative-Semiring R + ( a) + ( power-Commutative-Semiring R (nat-Fin n i) r)))) + by + ap-add-Commutative-Semiring R + ( refl) + ( htpy-sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → left-swap-mul-Commutative-Semiring R _ _ _)) + = + add-Commutative-Semiring R + ( a) + ( mul-Commutative-Semiring R + ( r) + ( sum-fin-sequence-type-Commutative-Semiring R n + ( λ i → + mul-Commutative-Semiring R + ( a) + ( power-Commutative-Semiring R (nat-Fin n i) r)))) + by + ap-add-Commutative-Semiring R + ( refl) + ( inv + ( left-distributive-mul-sum-fin-sequence-type-Commutative-Semiring + ( R) + ( n) + ( r) + ( _))) + = + add-Commutative-Semiring R + ( a) + ( mul-Commutative-Semiring R + ( r) + ( sum-standard-geometric-fin-sequence-Commutative-Semiring R + ( a) + ( r) + ( n))) + by + ap-add-Commutative-Semiring R + ( refl) + ( ap-mul-Commutative-Semiring R + ( refl) + ( htpy-sum-fin-sequence-type-Commutative-Semiring R n + ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring + ( R) + ( a) + ( r) ∘ + nat-Fin n))) + where + term : + type-Commutative-Semiring R → type-Commutative-Semiring R → + sequence (type-Commutative-Semiring R) + term a' r' = + seq-standard-geometric-sequence-Commutative-Semiring R a' r' + term-Fin : + type-Commutative-Semiring R → type-Commutative-Semiring R → + (n : ℕ) → fin-sequence (type-Commutative-Semiring R) n + term-Fin a' r' = + standard-geometric-fin-sequence-Commutative-Semiring R a' r' +``` diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 6655218d7ca..51a5fb4b31e 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -85,6 +85,7 @@ open import elementary-number-theory.finitary-natural-numbers public open import elementary-number-theory.finitely-cyclic-maps public open import elementary-number-theory.fundamental-theorem-of-arithmetic public open import elementary-number-theory.geometric-sequences-positive-rational-numbers public +open import elementary-number-theory.geometric-sequences-rational-numbers public open import elementary-number-theory.goldbach-conjecture public open import elementary-number-theory.greatest-common-divisor-integers public open import elementary-number-theory.greatest-common-divisor-natural-numbers public diff --git a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md new file mode 100644 index 00000000000..747150c04bb --- /dev/null +++ b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md @@ -0,0 +1,203 @@ +# Geometric sequences of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.geometric-sequences-rational-numbers where +``` + +
Imports + +```agda +open import commutative-algebra.geometric-sequences-commutative-rings +open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings + +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.multiplication-rational-numbers +open import elementary-number-theory.multiplicative-group-of-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.powers-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.ring-of-rational-numbers + +open import foundation.identity-types +open import foundation.negated-equality +open import foundation.universe-levels + +open import group-theory.groups + +open import lists.sequences + +open import order-theory.strictly-increasing-sequences-strictly-preordered-sets +``` + +
+ +## Idea + +A +{{#concept "geometric sequence" Disambiguation="of rational numbers" Agda=geometric-sequence-ℚ}} +of [rational numbers](elementary-number-theory.positive-rational-numbers.md) is +a +[geometric sequence](commutative-algebra.geometric-sequences-commutative-rings.md) +in the +[commutative ring of rational numbers](elementary-number-theory.ring-of-rational-numbers.md). + +## Definitions + +```agda +geometric-sequence-ℚ : UU lzero +geometric-sequence-ℚ = geometric-sequence-Commutative-Ring commutative-ring-ℚ + +seq-geometric-sequence-ℚ : geometric-sequence-ℚ → sequence ℚ +seq-geometric-sequence-ℚ = + seq-geometric-sequence-Commutative-Ring commutative-ring-ℚ + +standard-geometric-sequence-ℚ : ℚ → ℚ → geometric-sequence-ℚ +standard-geometric-sequence-ℚ = + standard-geometric-sequence-Commutative-Ring commutative-ring-ℚ + +seq-standard-geometric-sequence-ℚ : ℚ → ℚ → sequence ℚ +seq-standard-geometric-sequence-ℚ = + seq-standard-geometric-sequence-Commutative-Ring commutative-ring-ℚ +``` + +## Properties + +### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` + +```agda +module _ + (a r : ℚ) + where + + compute-standard-geometric-sequence-ℚ : + (n : ℕ) → seq-standard-geometric-sequence-ℚ a r n = a *ℚ power-ℚ n r + compute-standard-geometric-sequence-ℚ n = + inv + ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring + ( commutative-ring-ℚ) + ( a) + ( r) + ( n)) +``` + +### If `r ≠ 1`, the sum of the first `n` elements of the standard geometric sequence `n ↦ arⁿ` is `a(1-rⁿ)/(1-r)` + +```agda +sum-standard-geometric-fin-sequence-ℚ : ℚ → ℚ → ℕ → ℚ +sum-standard-geometric-fin-sequence-ℚ = + sum-standard-geometric-fin-sequence-Commutative-Ring commutative-ring-ℚ + +module _ + (a r : ℚ) (r≠1 : r ≠ one-ℚ) + where + + abstract + compute-sum-standard-geometric-fin-sequence-ℚ : + (n : ℕ) → + sum-standard-geometric-fin-sequence-ℚ a r n = + ( a *ℚ + ( (one-ℚ -ℚ power-ℚ n r) *ℚ + rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1))) + compute-sum-standard-geometric-fin-sequence-ℚ 0 = + inv + ( equational-reasoning + a *ℚ ((one-ℚ -ℚ one-ℚ) *ℚ _) + = a *ℚ (zero-ℚ *ℚ _) + by + ap-mul-ℚ + ( refl) + ( ap-mul-ℚ (right-inverse-law-add-ℚ one-ℚ) refl) + = a *ℚ zero-ℚ + by ap-mul-ℚ refl (left-zero-law-mul-ℚ _) + = zero-ℚ + by right-zero-law-mul-ℚ a) + compute-sum-standard-geometric-fin-sequence-ℚ (succ-ℕ n) = + let + 1/1-r = rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1) + in + equational-reasoning + sum-standard-geometric-fin-sequence-ℚ a r (succ-ℕ n) + = + sum-standard-geometric-fin-sequence-ℚ a r n +ℚ + seq-standard-geometric-sequence-ℚ a r n + by + cons-sum-fin-sequence-type-Commutative-Ring + ( commutative-ring-ℚ) + ( n) + ( _) + ( refl) + = + ( a *ℚ + ( (one-ℚ -ℚ power-ℚ n r) *ℚ 1/1-r)) +ℚ + ( a *ℚ power-ℚ n r) + by + ap-add-ℚ + ( compute-sum-standard-geometric-fin-sequence-ℚ n) + ( compute-standard-geometric-sequence-ℚ a r n) + = + a *ℚ + (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/1-r) +ℚ power-ℚ n r) + by inv (left-distributive-mul-add-ℚ a _ _) + = + a *ℚ + ( (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/1-r) +ℚ + (power-ℚ n r *ℚ (one-ℚ -ℚ r)) *ℚ 1/1-r)) + by + ap-mul-ℚ + ( refl) + ( ap-add-ℚ + ( refl) + ( inv + ( cancel-right-mul-div-ℚˣ _ + ( invertible-diff-neq-ℚ r one-ℚ r≠1)))) + = + a *ℚ + ( ( (one-ℚ -ℚ power-ℚ n r) +ℚ (power-ℚ n r *ℚ (one-ℚ -ℚ r))) *ℚ + 1/1-r) + by + ap-mul-ℚ + ( refl) + ( inv (right-distributive-mul-add-ℚ _ _ 1/1-r)) + = + a *ℚ + ( ( one-ℚ -ℚ power-ℚ n r +ℚ + ((power-ℚ n r *ℚ one-ℚ) -ℚ (power-ℚ n r *ℚ r))) *ℚ + 1/1-r) + by + ap-mul-ℚ + ( refl) + ( ap-mul-ℚ + ( ap-add-ℚ refl (left-distributive-mul-diff-ℚ _ _ _)) + ( refl)) + = + a *ℚ + ( ( one-ℚ -ℚ power-ℚ n r +ℚ + ((power-ℚ n r -ℚ power-ℚ (succ-ℕ n) r))) *ℚ + 1/1-r) + by + ap-mul-ℚ + ( refl) + ( ap-mul-ℚ + ( ap-add-ℚ + ( refl) + ( ap-diff-ℚ + ( right-unit-law-mul-ℚ _) + ( inv (power-succ-ℚ n r)))) + ( refl)) + = a *ℚ ((one-ℚ -ℚ power-ℚ (succ-ℕ n) r) *ℚ 1/1-r) + by + ap-mul-ℚ + ( refl) + ( ap-mul-ℚ + ( mul-right-div-Group group-add-ℚ _ _ _) + ( refl)) +``` + +## External links + +- [Geometric progressions](https://en.wikipedia.org/wiki/Geometric_progression) + at Wikipedia diff --git a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md index a35af131e80..3df03c15ddf 100644 --- a/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md @@ -9,11 +9,11 @@ module elementary-number-theory.multiplicative-group-of-rational-numbers where
Imports ```agda -open import elementary-number-theory.multiplication-positive-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.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-monoid-of-rational-numbers -open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-rational-numbers @@ -27,8 +27,8 @@ open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.function-types -open import foundation.negated-equality open import foundation.identity-types +open import foundation.negated-equality open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels @@ -190,3 +190,20 @@ abstract invertible-diff-neq-ℚ : (a b : ℚ) → a ≠ b → ℚˣ invertible-diff-neq-ℚ a b a≠b = (b -ℚ a , is-invertible-diff-neq-ℚ a b a≠b) ``` + +### Cancellation laws + +```agda +abstract + cancel-right-mul-div-ℚˣ : + (p : ℚ) (q : ℚˣ) → (p *ℚ rational-ℚˣ q) *ℚ rational-inv-ℚˣ q = p + cancel-right-mul-div-ℚˣ p q = + equational-reasoning + p *ℚ rational-ℚˣ q *ℚ rational-inv-ℚˣ q + = p *ℚ (rational-ℚˣ q *ℚ rational-inv-ℚˣ q) + by associative-mul-ℚ _ _ _ + = p *ℚ rational-ℚˣ one-ℚˣ + by ap-mul-ℚ refl (ap rational-ℚˣ (right-inverse-law-mul-ℚˣ q)) + = p + by right-unit-law-mul-ℚ p +``` diff --git a/src/ring-theory/geometric-sequences-rings.lagda.md b/src/ring-theory/geometric-sequences-rings.lagda.md index 90497c4db21..9458cf5a5fa 100644 --- a/src/ring-theory/geometric-sequences-rings.lagda.md +++ b/src/ring-theory/geometric-sequences-rings.lagda.md @@ -158,7 +158,7 @@ module _ ( u) ``` -### The nth term of an geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` +### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` ```agda module _ diff --git a/src/ring-theory/geometric-sequences-semirings.lagda.md b/src/ring-theory/geometric-sequences-semirings.lagda.md index 3d7dff3e3ac..1e560ceabd0 100644 --- a/src/ring-theory/geometric-sequences-semirings.lagda.md +++ b/src/ring-theory/geometric-sequences-semirings.lagda.md @@ -211,7 +211,7 @@ module _ ( u) ``` -### The nth term of an geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` +### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ` ```agda module _