Rational powers of positive real numbers

.vscode/agda.code-snippets

@@ -35,5 +35,10 @@
     "body": ["retract-reasoning ? retract-of ? by ?"],
     "description": "Retract reasoning",
     "prefix": ["retract-reasoning"]
+  },
+  "Inequality reasoning": {
+    "body": ["chain-of-inequalities ? ≤ ? by ?"],
+    "description": "Inequality reasoning",
+    "prefix": ["chain-of-inequalities"]
   }
 }

src/commutative-algebra/powers-of-elements-large-commutative-rings.lagda.md

@@ -12,6 +12,7 @@ open import commutative-algebra.large-commutative-rings
 open import elementary-number-theory.addition-natural-numbers
 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.identity-types
 open import foundation.universe-levels
@@ -97,6 +98,25 @@ module _
       power-one-Large-Ring (large-ring-Large-Commutative-Ring R)
 ```
 
+### `0ⁿ = 0` for nonzero `n`
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (R : Large-Commutative-Ring α β)
+  where
+
+  nonzero-power-zero-Large-Commutative-Ring :
+    (n : ℕ⁺) →
+    ( power-Large-Commutative-Ring
+        ( R)
+        ( nat-nonzero-ℕ n)
+        ( zero-Large-Commutative-Ring R) ＝
+      zero-Large-Commutative-Ring R)
+  nonzero-power-zero-Large-Commutative-Ring =
+    nonzero-power-zero-Large-Ring (large-ring-Large-Commutative-Ring R)
+```
+
 ### `xⁿ⁺¹ = xⁿx`
 
 ```agda
@@ -188,3 +208,20 @@ module _
       distributive-power-mul-Large-Commutative-Monoid
         ( multiplicative-large-commutative-monoid-Large-Commutative-Ring R)
 ```
+
+### Iterated powers commute
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (R : Large-Commutative-Ring α β)
+  where
+
+  abstract
+    commute-power-Large-Commutative-Ring :
+      {l : Level} (m n : ℕ) (x : type-Large-Commutative-Ring R l) →
+      power-Large-Commutative-Ring R m (power-Large-Commutative-Ring R n x) ＝
+      power-Large-Commutative-Ring R n (power-Large-Commutative-Ring R m x)
+    commute-power-Large-Commutative-Ring =
+      commute-power-Large-Ring (large-ring-Large-Commutative-Ring R)
+```

src/elementary-number-theory.lagda.md

@@ -58,6 +58,7 @@ open import elementary-number-theory.decidable-total-order-natural-numbers publi
 open import elementary-number-theory.decidable-total-order-rational-numbers public
 open import elementary-number-theory.decidable-total-order-standard-finite-types public
 open import elementary-number-theory.decidable-types public
+open import elementary-number-theory.diagonal-integer-fractions public
 open import elementary-number-theory.difference-integers public
 open import elementary-number-theory.difference-rational-numbers public
 open import elementary-number-theory.dirichlet-convolution public

src/elementary-number-theory/addition-positive-rational-numbers.lagda.md

@@ -12,6 +12,7 @@ module elementary-number-theory.addition-positive-rational-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.inequality-positive-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.minimum-positive-rational-numbers
 open import elementary-number-theory.positive-integer-fractions
@@ -131,34 +132,51 @@ interchange-law-add-add-ℚ⁺ x y u v =
       ( rational-ℚ⁺ v))
 ```
 
+### Addition with a positive rational number is a strictly increasing map
+
+```agda
+abstract
+  le-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x ((rational-ℚ⁺ d) +ℚ x)
+  le-left-add-rational-ℚ⁺ x d =
+    concatenate-leq-le-ℚ
+      ( x)
+      ( zero-ℚ +ℚ x)
+      ( (rational-ℚ⁺ d) +ℚ x)
+      ( inv-tr (leq-ℚ x) (left-unit-law-add-ℚ x) (refl-leq-ℚ x))
+      ( preserves-le-left-add-ℚ
+        ( x)
+        ( zero-ℚ)
+        ( 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 =
+    inv-tr
+      ( le-ℚ x)
+      ( commutative-add-ℚ x (rational-ℚ⁺ d))
+      ( le-left-add-rational-ℚ⁺ x d)
+
+  leq-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (rational-ℚ⁺ d +ℚ x)
+  leq-left-add-rational-ℚ⁺ x d = leq-le-ℚ (le-left-add-rational-ℚ⁺ x d)
+
+  leq-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (x +ℚ rational-ℚ⁺ d)
+  leq-right-add-rational-ℚ⁺ x d = leq-le-ℚ (le-right-add-rational-ℚ⁺ x d)
+```
+
 ### The sum of two positive rational numbers is greater than each of them
 
 ```agda
 module _
   (x y : ℚ⁺)
   where
 
-  le-left-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y)
-  le-left-add-ℚ⁺ =
-    tr
-      ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y)))
-      ( right-unit-law-add-ℚ (rational-ℚ⁺ x))
-      ( preserves-le-right-add-ℚ
-        ( rational-ℚ⁺ x)
-        ( zero-ℚ)
-        ( rational-ℚ⁺ y)
-        ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ y)))
-
-  le-right-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y)
+  le-right-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y)
   le-right-add-ℚ⁺ =
-    tr
-      ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y)))
-      ( left-unit-law-add-ℚ (rational-ℚ⁺ y))
-      ( preserves-le-left-add-ℚ
-        ( rational-ℚ⁺ y)
-        ( zero-ℚ)
-        ( rational-ℚ⁺ x)
-        ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ x)))
+    le-right-add-rational-ℚ⁺ (rational-ℚ⁺ x) y
+
+  le-left-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y)
+  le-left-add-ℚ⁺ =
+    le-left-add-rational-ℚ⁺ (rational-ℚ⁺ y) x
 ```
 
 ### The positive difference of strictly inequal positive rational numbers
@@ -196,7 +214,7 @@ module _
     tr
       ( le-ℚ⁺ le-diff-ℚ⁺)
       ( left-diff-law-add-ℚ⁺)
-      ( le-left-add-ℚ⁺ le-diff-ℚ⁺ x)
+      ( le-right-add-ℚ⁺ le-diff-ℚ⁺ x)
 ```
 
 ### Any positive rational number can be expressed as the sum of two positive rational numbers
@@ -229,12 +247,18 @@ module _
     le-left-summand-split-ℚ⁺ : le-ℚ⁺ left-summand-split-ℚ⁺ x
     le-left-summand-split-ℚ⁺ = le-mediant-zero-ℚ⁺ x
 
+    leq-left-summand-split-ℚ⁺ : leq-ℚ⁺ left-summand-split-ℚ⁺ x
+    leq-left-summand-split-ℚ⁺ = leq-le-ℚ le-left-summand-split-ℚ⁺
+
     le-right-summand-split-ℚ⁺ : le-ℚ⁺ right-summand-split-ℚ⁺ x
     le-right-summand-split-ℚ⁺ =
       tr
         ( le-ℚ⁺ right-summand-split-ℚ⁺)
         ( eq-add-split-ℚ⁺)
-        ( le-right-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺)
+        ( le-left-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺)
+
+    leq-right-summand-split-ℚ⁺ : leq-ℚ⁺ right-summand-split-ℚ⁺ x
+    leq-right-summand-split-ℚ⁺ = leq-le-ℚ le-right-summand-split-ℚ⁺
 
     le-add-split-ℚ⁺ :
       (p q r s : ℚ) →
@@ -259,37 +283,6 @@ module _
           ( r<s+right))
 ```
 
-### Addition with a positive rational number is an increasing map
-
-```agda
-abstract
-  le-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x ((rational-ℚ⁺ d) +ℚ x)
-  le-left-add-rational-ℚ⁺ x d =
-    concatenate-leq-le-ℚ
-      ( x)
-      ( zero-ℚ +ℚ x)
-      ( (rational-ℚ⁺ d) +ℚ x)
-      ( inv-tr (leq-ℚ x) (left-unit-law-add-ℚ x) (refl-leq-ℚ x))
-      ( preserves-le-left-add-ℚ
-        ( x)
-        ( zero-ℚ)
-        ( 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 =
-    inv-tr
-      ( le-ℚ x)
-      ( commutative-add-ℚ x (rational-ℚ⁺ d))
-      ( le-left-add-rational-ℚ⁺ x d)
-
-  leq-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (rational-ℚ⁺ d +ℚ x)
-  leq-left-add-rational-ℚ⁺ x d = leq-le-ℚ (le-left-add-rational-ℚ⁺ x d)
-
-  leq-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (x +ℚ rational-ℚ⁺ d)
-  leq-right-add-rational-ℚ⁺ x d = leq-le-ℚ (le-right-add-rational-ℚ⁺ x d)
-```
-
 ### Subtraction by a positive rational number is a strictly deflationary map
 
 ```agda

src/elementary-number-theory/diagonal-integer-fractions.lagda.md

@@ -0,0 +1,105 @@
+# Diagonal integer fractions
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.diagonal-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.positive-integers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+{{#concept "Diagonal integer fractions" Agda=diagonal-fraction-ℤ}} are
+[integer fractions](elementary-number-theory.integer-fractions.md) of the form
+`k/k`.
+
+## Definition
+
+```agda
+is-diagonal-prop-fraction-ℤ : fraction-ℤ → Prop lzero
+is-diagonal-prop-fraction-ℤ (p , q , _) = Id-Prop ℤ-Set p q
+
+is-diagonal-fraction-ℤ : fraction-ℤ → UU lzero
+is-diagonal-fraction-ℤ (p , q , _) = p ＝ q
+
+in-diagonal-fraction-ℤ : ℤ⁺ → fraction-ℤ
+in-diagonal-fraction-ℤ k⁺@(k , _) = (k , k⁺)
+
+is-diagonal-in-diagonal-fraction-ℤ :
+  (k : ℤ⁺) → is-diagonal-fraction-ℤ (in-diagonal-fraction-ℤ k)
+is-diagonal-in-diagonal-fraction-ℤ _ = refl
+```
+
+## Properties
+
+### A fraction is diagonal if and only if it is similar to 1
+
+```agda
+abstract
+  sim-one-is-diagonal-fraction-ℤ :
+    (p : fraction-ℤ) →
+    is-diagonal-fraction-ℤ p → sim-fraction-ℤ p one-fraction-ℤ
+  sim-one-is-diagonal-fraction-ℤ (p , _ , _) refl =
+    commutative-mul-ℤ p one-ℤ
+
+  is-diagonal-sim-one-fraction-ℤ :
+    (p : fraction-ℤ) →
+    sim-fraction-ℤ p one-fraction-ℤ →
+    is-diagonal-fraction-ℤ p
+  is-diagonal-sim-one-fraction-ℤ (p , q , _) p~q =
+    equational-reasoning
+      p
+      ＝ p *ℤ one-ℤ
+        by inv (right-unit-law-mul-ℤ p)
+      ＝ one-ℤ *ℤ q
+        by p~q
+      ＝ q
+        by left-unit-law-mul-ℤ q
+```
+
+### Multiplying a fraction by a diagonal fraction results in a similar fraction
+
+```agda
+abstract
+  sim-right-mul-diagonal-fraction-ℤ :
+    (p q : fraction-ℤ) → is-diagonal-fraction-ℤ q →
+    sim-fraction-ℤ (p *fraction-ℤ q) p
+  sim-right-mul-diagonal-fraction-ℤ p (q , .q , pos-q) refl =
+    transitive-sim-fraction-ℤ
+      ( p *fraction-ℤ (q , q , pos-q))
+      ( p *fraction-ℤ one-fraction-ℤ)
+      ( p)
+      ( right-unit-law-mul-fraction-ℤ p)
+      ( sim-fraction-mul-fraction-ℤ
+        ( refl)
+        ( sim-one-is-diagonal-fraction-ℤ _ refl))
+
+  sim-left-mul-diagonal-fraction-ℤ :
+    (p q : fraction-ℤ) → is-diagonal-fraction-ℤ p →
+    sim-fraction-ℤ (p *fraction-ℤ q) q
+  sim-left-mul-diagonal-fraction-ℤ p q H =
+    transitive-sim-fraction-ℤ
+      ( p *fraction-ℤ q)
+      ( q *fraction-ℤ p)
+      ( q)
+      ( sim-right-mul-diagonal-fraction-ℤ q p H)
+      ( commutative-mul-fraction-ℤ p q)
+```