The multiplicative group of positive rational numbers
Content created by Louis Wasserman, malarbol, Fredrik Bakke and Garrett Figueroa.
Created on 2024-04-25.
Last modified on 2025-10-15.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.multiplicative-group-of-positive-rational-numbers where
Imports
open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-positive-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.multiplication-integers 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.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-integers 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.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import group-theory.abelian-groups open import group-theory.groups open import group-theory.monoids open import group-theory.submonoids
Idea
The submonoid of positive rational numbers in the multiplicative monoid of rational numbers is a commutative group.
Definitions
The positive inverse of a positive rational number
opaque unfolding inv-is-positive-ℚ inv-ℚ⁺ : ℚ⁺ → ℚ⁺ pr1 (inv-ℚ⁺ (x , P)) = inv-is-positive-ℚ x P pr2 (inv-ℚ⁺ (x , P)) = is-positive-denominator-ℚ x rational-inv-ℚ⁺ : ℚ⁺ → ℚ rational-inv-ℚ⁺ q = rational-ℚ⁺ (inv-ℚ⁺ q) is-positive-rational-inv-ℚ⁺ : (q : ℚ⁺) → is-positive-ℚ (rational-inv-ℚ⁺ q) is-positive-rational-inv-ℚ⁺ q = is-positive-rational-ℚ⁺ (inv-ℚ⁺ q)
Inverse laws in the multiplicative group of positive rational numbers
opaque unfolding inv-ℚ⁺ left-inverse-law-mul-ℚ⁺ : (x : ℚ⁺) → (inv-ℚ⁺ x) *ℚ⁺ x = one-ℚ⁺ left-inverse-law-mul-ℚ⁺ x = eq-ℚ⁺ ( left-inverse-law-mul-is-positive-ℚ ( rational-ℚ⁺ x) ( is-positive-rational-ℚ⁺ x)) right-inverse-law-mul-ℚ⁺ : (x : ℚ⁺) → x *ℚ⁺ (inv-ℚ⁺ x) = one-ℚ⁺ right-inverse-law-mul-ℚ⁺ x = eq-ℚ⁺ ( right-inverse-law-mul-is-positive-ℚ ( rational-ℚ⁺ x) ( is-positive-rational-ℚ⁺ x))
The multiplicative group of positive rational numbers
group-mul-ℚ⁺ : Group lzero pr1 group-mul-ℚ⁺ = semigroup-mul-ℚ⁺ pr1 (pr2 group-mul-ℚ⁺) = is-unital-Monoid monoid-mul-ℚ⁺ pr1 (pr2 (pr2 group-mul-ℚ⁺)) = inv-ℚ⁺ pr1 (pr2 (pr2 (pr2 group-mul-ℚ⁺))) = left-inverse-law-mul-ℚ⁺ pr2 (pr2 (pr2 (pr2 group-mul-ℚ⁺))) = right-inverse-law-mul-ℚ⁺
Properties
The multiplicative group of positive rational numbers is commutative
abelian-group-mul-ℚ⁺ : Ab lzero pr1 abelian-group-mul-ℚ⁺ = group-mul-ℚ⁺ pr2 abelian-group-mul-ℚ⁺ = commutative-mul-ℚ⁺
Inversion reverses inequality on the positive rational numbers
opaque unfolding inv-ℚ⁺ unfolding leq-ℚ-Prop inv-leq-ℚ⁺ : (x y : ℚ⁺) → leq-ℚ⁺ x y → leq-ℚ⁺ (inv-ℚ⁺ y) (inv-ℚ⁺ x) inv-leq-ℚ⁺ x y = binary-tr ( leq-ℤ) ( commutative-mul-ℤ _ _) ( commutative-mul-ℤ _ _)
Inversion is an involution
abstract inv-inv-ℚ⁺ : (q : ℚ⁺) → inv-ℚ⁺ (inv-ℚ⁺ q) = q inv-inv-ℚ⁺ = inv-inv-Group group-mul-ℚ⁺ rational-inv-inv-ℚ⁺ : (q : ℚ⁺) → rational-inv-ℚ⁺ (inv-ℚ⁺ q) = rational-ℚ⁺ q rational-inv-inv-ℚ⁺ q = ap rational-ℚ⁺ (inv-inv-ℚ⁺ q)
Inversion reverses strict inequality on the positive rational numbers
opaque unfolding inv-ℚ⁺ unfolding le-ℚ-Prop inv-le-ℚ⁺ : (x y : ℚ⁺) → le-ℚ⁺ x y → le-ℚ⁺ (inv-ℚ⁺ y) (inv-ℚ⁺ x) inv-le-ℚ⁺ x y = binary-tr ( le-ℤ) ( commutative-mul-ℤ _ _) ( commutative-mul-ℤ _ _) inv-le-ℚ⁺' : (x y : ℚ⁺) → le-ℚ⁺ (inv-ℚ⁺ x) (inv-ℚ⁺ y) → le-ℚ⁺ y x inv-le-ℚ⁺' x y = binary-tr ( le-ℤ) ( commutative-mul-ℤ _ _) ( commutative-mul-ℤ _ _)
Inversion of positive rational numbers distributes over multiplication
abstract distributive-inv-mul-ℚ⁺ : (x y : ℚ⁺) → inv-ℚ⁺ (x *ℚ⁺ y) = inv-ℚ⁺ x *ℚ⁺ inv-ℚ⁺ y distributive-inv-mul-ℚ⁺ x y = distributive-inv-mul-Group' ( group-mul-ℚ⁺) ( x) ( y) ( commutative-mul-ℚ⁺ x y)
Inversion on the positive rational numbers interchanges numerator and denominator
module _ (x : ℚ⁺) where opaque unfolding inv-ℚ⁺ eq-numerator-inv-denominator-ℚ⁺ : numerator-ℚ⁺ (inv-ℚ⁺ x) = denominator-ℚ⁺ x eq-numerator-inv-denominator-ℚ⁺ = ind-Σ eq-numerator-inv-denominator-is-positive-ℚ x eq-denominator-inv-numerator-ℚ⁺ : denominator-ℚ⁺ (inv-ℚ⁺ x) = numerator-ℚ⁺ x eq-denominator-inv-numerator-ℚ⁺ = ind-Σ eq-denominator-inv-numerator-is-positive-ℚ x
Group laws on the positive rational numbers
abstract is-section-right-div-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → (q *ℚ rational-inv-ℚ⁺ p) *ℚ rational-ℚ⁺ p = q is-section-right-div-ℚ⁺ p⁺@(p , _) q = equational-reasoning (q *ℚ rational-inv-ℚ⁺ p⁺) *ℚ p = q *ℚ rational-ℚ⁺ (inv-ℚ⁺ p⁺ *ℚ⁺ p⁺) by associative-mul-ℚ _ _ _ = q *ℚ one-ℚ by ap-mul-ℚ refl (ap rational-ℚ⁺ (left-inverse-law-mul-ℚ⁺ p⁺)) = q by right-unit-law-mul-ℚ q is-retraction-left-div-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → rational-ℚ⁺ (inv-ℚ⁺ p) *ℚ (rational-ℚ⁺ p *ℚ q) = q is-retraction-left-div-ℚ⁺ p⁺@(p , _) q = equational-reasoning rational-ℚ⁺ (inv-ℚ⁺ p⁺) *ℚ (p *ℚ q) = rational-ℚ⁺ (inv-ℚ⁺ p⁺ *ℚ⁺ p⁺) *ℚ q by inv (associative-mul-ℚ _ _ _) = rational-ℚ⁺ one-ℚ⁺ *ℚ q by ap (λ r → rational-ℚ⁺ r *ℚ q) (left-inverse-law-mul-ℚ⁺ p⁺) = q by left-unit-law-mul-ℚ q is-retraction-right-div-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → (q *ℚ rational-ℚ⁺ p) *ℚ rational-ℚ⁺ (inv-ℚ⁺ p) = q is-retraction-right-div-ℚ⁺ p⁺@(p , _) q = equational-reasoning (q *ℚ p) *ℚ rational-ℚ⁺ (inv-ℚ⁺ p⁺) = q *ℚ rational-ℚ⁺ (p⁺ *ℚ⁺ inv-ℚ⁺ p⁺) by associative-mul-ℚ _ _ _ = q *ℚ rational-ℚ⁺ one-ℚ⁺ by ap (λ r → q *ℚ rational-ℚ⁺ r) (right-inverse-law-mul-ℚ⁺ p⁺) = q by right-unit-law-mul-ℚ q
Multiplication by a positive rational number reflects strict inequality
abstract reflects-le-left-mul-ℚ⁺ : (p : ℚ⁺) (q r : ℚ) → le-ℚ (rational-ℚ⁺ p *ℚ q) (rational-ℚ⁺ p *ℚ r) → le-ℚ q r reflects-le-left-mul-ℚ⁺ p⁺@(p , _) q r pq<pr = binary-tr ( le-ℚ) ( is-retraction-left-div-ℚ⁺ p⁺ q) ( is-retraction-left-div-ℚ⁺ p⁺ r) ( preserves-le-left-mul-ℚ⁺ (inv-ℚ⁺ p⁺) _ _ pq<pr)
Recent changes
- 2025-10-15. Louis Wasserman. Inequalities from multiplication of signed real numbers (#1584).
- 2025-10-14. Louis Wasserman. Multiplicative inverses of positive real numbers (#1569).
- 2025-10-11. Louis Wasserman. Square roots of nonnegative real numbers (#1570).
- 2025-10-09. Louis Wasserman. Multiplication of real numbers (#1384).
- 2025-10-04. Louis Wasserman. Split out operations on positive rational numbers (#1562).