Integer fractions
module elementary-number-theory.integer-fractions where
Imports
open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalence-relations open import foundation.identity-types open import foundation.negation open import foundation.propositions open import foundation.sets open import foundation.universe-levels
Idea
The type of integer fractions is the type of pairs n/m consisting of an
integer n and a positive integer m. The type of rational numbers is a
retract of the type of fractions.
Definitions
The type of fractions
fraction-ℤ : UU lzero fraction-ℤ = ℤ × positive-ℤ
The numerator of a fraction
numerator-fraction-ℤ : fraction-ℤ → ℤ numerator-fraction-ℤ x = pr1 x
The denominator of a fraction
positive-denominator-fraction-ℤ : fraction-ℤ → positive-ℤ positive-denominator-fraction-ℤ x = pr2 x denominator-fraction-ℤ : fraction-ℤ → ℤ denominator-fraction-ℤ x = pr1 (positive-denominator-fraction-ℤ x) is-positive-denominator-fraction-ℤ : (x : fraction-ℤ) → is-positive-ℤ (denominator-fraction-ℤ x) is-positive-denominator-fraction-ℤ x = pr2 (positive-denominator-fraction-ℤ x)
Inclusion of the integers
in-fraction-ℤ-ℤ : ℤ → fraction-ℤ pr1 (in-fraction-ℤ-ℤ x) = x pr2 (in-fraction-ℤ-ℤ x) = one-positive-ℤ
Negative one, zero and one
neg-one-fraction-ℤ : fraction-ℤ neg-one-fraction-ℤ = in-fraction-ℤ-ℤ neg-one-ℤ is-neg-one-fraction-ℤ : fraction-ℤ → UU lzero is-neg-one-fraction-ℤ x = (x ＝ neg-one-fraction-ℤ) zero-fraction-ℤ : fraction-ℤ zero-fraction-ℤ = in-fraction-ℤ-ℤ zero-ℤ is-zero-fraction-ℤ : fraction-ℤ → UU lzero is-zero-fraction-ℤ x = (x ＝ zero-fraction-ℤ) is-nonzero-fraction-ℤ : fraction-ℤ → UU lzero is-nonzero-fraction-ℤ k = ¬ (is-zero-fraction-ℤ k) one-fraction-ℤ : fraction-ℤ one-fraction-ℤ = in-fraction-ℤ-ℤ one-ℤ is-one-fraction-ℤ : fraction-ℤ → UU lzero is-one-fraction-ℤ x = (x ＝ one-fraction-ℤ)
Properties
Denominators are nonzero
is-nonzero-denominator-fraction-ℤ : (x : fraction-ℤ) → is-nonzero-ℤ (denominator-fraction-ℤ x) is-nonzero-denominator-fraction-ℤ x = is-nonzero-is-positive-ℤ ( denominator-fraction-ℤ x) ( is-positive-denominator-fraction-ℤ x)
The type of fractions is a set
is-set-fraction-ℤ : is-set fraction-ℤ is-set-fraction-ℤ = is-set-Σ is-set-ℤ λ _ → is-set-positive-ℤ
sim-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero sim-fraction-ℤ-Prop x y = Id-Prop ℤ-Set ((numerator-fraction-ℤ x) *ℤ (denominator-fraction-ℤ y)) ((numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x)) sim-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero sim-fraction-ℤ x y = type-Prop (sim-fraction-ℤ-Prop x y) is-prop-sim-fraction-ℤ : (x y : fraction-ℤ) → is-prop (sim-fraction-ℤ x y) is-prop-sim-fraction-ℤ x y = is-prop-type-Prop (sim-fraction-ℤ-Prop x y) refl-sim-fraction-ℤ : (x : fraction-ℤ) → sim-fraction-ℤ x x refl-sim-fraction-ℤ x = refl symm-sim-fraction-ℤ : (x y : fraction-ℤ) → sim-fraction-ℤ x y → sim-fraction-ℤ y x symm-sim-fraction-ℤ x y r = inv r trans-sim-fraction-ℤ : (x y z : fraction-ℤ) → sim-fraction-ℤ x y → sim-fraction-ℤ y z → sim-fraction-ℤ x z trans-sim-fraction-ℤ x y z r s = is-injective-right-mul-ℤ ( denominator-fraction-ℤ y) ( is-nonzero-denominator-fraction-ℤ y) ( ( associative-mul-ℤ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ z) ( denominator-fraction-ℤ y)) ∙ ( ( ap ( (numerator-fraction-ℤ x) *ℤ_) ( commutative-mul-ℤ ( denominator-fraction-ℤ z) ( denominator-fraction-ℤ y))) ∙ ( ( inv ( associative-mul-ℤ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ y) ( denominator-fraction-ℤ z))) ∙ ( ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙ ( ( associative-mul-ℤ ( numerator-fraction-ℤ y) ( denominator-fraction-ℤ x) ( denominator-fraction-ℤ z)) ∙ ( ( ap ( (numerator-fraction-ℤ y) *ℤ_) ( commutative-mul-ℤ ( denominator-fraction-ℤ x) ( denominator-fraction-ℤ z))) ∙ ( ( inv ( associative-mul-ℤ ( numerator-fraction-ℤ y) ( denominator-fraction-ℤ z) ( denominator-fraction-ℤ x))) ∙ ( ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙ ( ( associative-mul-ℤ ( numerator-fraction-ℤ z) ( denominator-fraction-ℤ y) ( denominator-fraction-ℤ x)) ∙ ( ( ap ( (numerator-fraction-ℤ z) *ℤ_) ( commutative-mul-ℤ ( denominator-fraction-ℤ y) ( denominator-fraction-ℤ x))) ∙ ( inv ( associative-mul-ℤ ( numerator-fraction-ℤ z) ( denominator-fraction-ℤ x) ( denominator-fraction-ℤ y))))))))))))) eq-rel-sim-fraction-ℤ : Eq-Rel lzero fraction-ℤ eq-rel-sim-fraction-ℤ = pair (sim-fraction-ℤ-Prop) ( pair' (λ {x} → refl-sim-fraction-ℤ x) ( pair' (λ {x y} → symm-sim-fraction-ℤ x y) (λ {x y z} → trans-sim-fraction-ℤ x y z)))
The greatest common divisor of the numerator and a denominator of a fraction is always a positive integer
is-positive-gcd-numerator-denominator-fraction-ℤ : (x : fraction-ℤ) → is-positive-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) is-positive-gcd-numerator-denominator-fraction-ℤ x = is-positive-gcd-is-positive-right-ℤ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ x) ( is-positive-denominator-fraction-ℤ x) is-nonzero-gcd-numerator-denominator-fraction-ℤ : (x : fraction-ℤ) → is-nonzero-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) is-nonzero-gcd-numerator-denominator-fraction-ℤ x = is-nonzero-is-positive-ℤ ( gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) ( is-positive-gcd-numerator-denominator-fraction-ℤ x)