Integer fractions
Content created by Fredrik Bakke, Egbert Rijke, malarbol, Fernando Chu, Julian KG, fernabnor and louismntnu.
Created on 2023-04-08.
Last modified on 2024-04-09.
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 elementary-number-theory.nonzero-integers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.binary-relations 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-ℤ)
The negative of an integer fraction
neg-fraction-ℤ : fraction-ℤ → fraction-ℤ neg-fraction-ℤ (d , n) = (neg-ℤ d , n)
Properties
Denominators are nonzero
abstract is-nonzero-denominator-fraction-ℤ : (x : fraction-ℤ) → is-nonzero-ℤ (denominator-fraction-ℤ x) is-nonzero-denominator-fraction-ℤ x = is-nonzero-is-positive-ℤ (is-positive-denominator-fraction-ℤ x)
The type of fractions is a set
abstract 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-ℤ : is-reflexive sim-fraction-ℤ refl-sim-fraction-ℤ x = refl symmetric-sim-fraction-ℤ : is-symmetric sim-fraction-ℤ symmetric-sim-fraction-ℤ x y r = inv r abstract transitive-sim-fraction-ℤ : is-transitive sim-fraction-ℤ transitive-sim-fraction-ℤ x y z s r = 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)))) equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop pr1 (pr2 equivalence-relation-sim-fraction-ℤ) = refl-sim-fraction-ℤ pr1 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = symmetric-sim-fraction-ℤ pr2 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = transitive-sim-fraction-ℤ
The negatives of two similar integer fractions are similar
module _ (x y : fraction-ℤ) where abstract preserves-sim-neg-fraction-ℤ : sim-fraction-ℤ x y → sim-fraction-ℤ (neg-fraction-ℤ x) (neg-fraction-ℤ y) preserves-sim-neg-fraction-ℤ H = ( left-negative-law-mul-ℤ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ y)) ∙ ( ap neg-ℤ H) ∙ ( inv ( left-negative-law-mul-ℤ ( numerator-fraction-ℤ y) ( denominator-fraction-ℤ x)))
Two integer fractions with zero numerator are similar
abstract sim-is-zero-numerator-fraction-ℤ : (x y : fraction-ℤ) → is-zero-ℤ (numerator-fraction-ℤ x) → is-zero-ℤ (numerator-fraction-ℤ y) → sim-fraction-ℤ x y sim-is-zero-numerator-fraction-ℤ x y H K = eq-is-zero-ℤ ( ap (_*ℤ (denominator-fraction-ℤ y)) H ∙ left-zero-law-mul-ℤ (denominator-fraction-ℤ y)) ( ap (_*ℤ (denominator-fraction-ℤ x)) K ∙ left-zero-law-mul-ℤ (denominator-fraction-ℤ x))
The greatest common divisor of the numerator and a denominator of a fraction is always a positive integer
abstract 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) abstract 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-ℤ ( is-positive-gcd-numerator-denominator-fraction-ℤ x)
Recent changes
- 2024-04-09. malarbol and Fredrik Bakke. The additive group of rational numbers (#1100).
- 2024-03-28. malarbol and Fredrik Bakke. Refactoring positive integers (#1059).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-10-06. Egbert Rijke and Fredrik Bakke. Torsion-free groups (#813).