Skip to content

Commit

Permalink
some work on integer fractions
Browse files Browse the repository at this point in the history
  • Loading branch information
@EgbertRijke
EgbertRijke committed Oct 26, 2024
1 parent 48b74ec commit 7952fc4
Show file tree
Hide file tree
Showing 5 changed files with 99 additions and 64 deletions.
80 changes: 33 additions & 47 deletions src/elementary-number-theory/integer-fractions.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module elementary-number-theory.integer-fractions where
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.natural-numbers
open import elementary-number-theory.nonzero-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers
Expand Down Expand Up @@ -64,6 +65,10 @@ 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)

nat-denominator-fraction-ℤ : fraction-ℤ → ℕ
nat-denominator-fraction-ℤ x =
nat-positive-ℤ (positive-denominator-fraction-ℤ x)
```

### Inclusion of the integers
Expand Down Expand Up @@ -129,12 +134,32 @@ fraction-ℤ-Set : Set lzero
fraction-ℤ-Set = fraction-ℤ , is-set-fraction-ℤ
```

### The standard equivalence relation on integer fractions

Two integer fractions `a/b` and `c/d` are said to be equivalent if they satisfy

```text
ad ＝ cb.
```

This relation is obviously reflexive and symmetric. To see that it is transitive, suppose that `a/b ~ c/d` and that `c/d ~ e/f`. Since `d` is positive, we have the implication

```text
(af)d ＝ (eb)d → af ＝ eb.
```

Therefore it suffices to show that `d(af) ＝ d(eb)`. To see this, we calculate

```text
(af)d ＝ (ad)f ＝ (cb)f ＝ (cf)b ＝ (ed)b ＝ (eb)d.
```

```agda
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))
( 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)
Expand All @@ -150,54 +175,15 @@ symmetric-sim-fraction-ℤ x y r = inv r

abstract
transitive-sim-fraction-ℤ : is-transitive sim-fraction-ℤ
transitive-sim-fraction-ℤ x y z s r =
transitive-sim-fraction-ℤ (a , b , pb) y@(c , d , pd) (e , f , pf) 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))))
( right-swap-mul-ℤ a f d ∙
ap (_*ℤ f) r ∙
right-swap-mul-ℤ c b f ∙
ap (_*ℤ b) s ∙
right-swap-mul-ℤ e d b)

equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ
pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop
Expand Down
14 changes: 11 additions & 3 deletions src/elementary-number-theory/irrationality-square-root-of-2.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,14 @@ module elementary-number-theory.irrationality-square-root-of-2 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.natural-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.identity-types
open import foundation.negation
```

</details>
Expand Down Expand Up @@ -46,6 +53,7 @@ a reduced fraction.

```agda
not-two-square-reduced-fraction-ℤ :
?
not-two-square-reduced-fraction-ℤ = ?
(x : fraction-ℤ) (H : is-reduced-fraction-ℤ x) →
¬ (sim-fraction-ℤ (mul-fraction-ℤ x x) (in-fraction-ℤ (int-ℕ 2)))
not-two-square-reduced-fraction-ℤ x H K = {!!}
```
43 changes: 32 additions & 11 deletions src/elementary-number-theory/multiplication-integer-fractions.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.positive-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
Expand All @@ -31,16 +32,36 @@ on the [integers](elementary-number-theory.integers.md) to
the basic properties of multiplication on integer fraction only hold up to
fraction similarity.

## Definition
## Definitions

### Multiplication of integer fractions

```agda
numerator-mul-fraction-ℤ :
(x y : fraction-ℤ) → ℤ
numerator-mul-fraction-ℤ x y =
numerator-fraction-ℤ x *ℤ numerator-fraction-ℤ y

positive-denominator-mul-fraction-ℤ :
(x y : fraction-ℤ) → positive-ℤ
positive-denominator-mul-fraction-ℤ x y =
mul-positive-ℤ
( positive-denominator-fraction-ℤ x)
( positive-denominator-fraction-ℤ y)

denominator-mul-fraction-ℤ :
(x y : fraction-ℤ) → ℤ
denominator-mul-fraction-ℤ x y =
int-positive-ℤ (positive-denominator-mul-fraction-ℤ x y)

is-positive-denominator-mul-fraction-ℤ :
(x y : fraction-ℤ) → is-positive-ℤ (denominator-mul-fraction-ℤ x y)
is-positive-denominator-mul-fraction-ℤ x y =
is-positive-int-positive-ℤ (positive-denominator-mul-fraction-ℤ x y)

mul-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
pr1 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos)) =
m *ℤ m'
pr1 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
n *ℤ n'
pr2 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
is-positive-mul-ℤ n-pos n'-pos
pr1 (mul-fraction-ℤ x y) = numerator-mul-fraction-ℤ x y
pr2 (mul-fraction-ℤ x y) = positive-denominator-mul-fraction-ℤ x y

mul-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
mul-fraction-ℤ' x y = mul-fraction-ℤ y x
Expand Down Expand Up @@ -98,8 +119,8 @@ right-unit-law-mul-fraction-ℤ (n , d , p) =
associative-mul-fraction-ℤ :
(x y z : fraction-ℤ) →
sim-fraction-ℤ
(mul-fraction-ℤ (mul-fraction-ℤ x y) z)
(mul-fraction-ℤ x (mul-fraction-ℤ y z))
( mul-fraction-ℤ (mul-fraction-ℤ x y) z)
( mul-fraction-ℤ x (mul-fraction-ℤ y z))
associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz))
```
Expand All @@ -119,8 +140,8 @@ commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
left-distributive-mul-add-fraction-ℤ :
(x y z : fraction-ℤ) →
sim-fraction-ℤ
(mul-fraction-ℤ x (add-fraction-ℤ y z))
(add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z))
( mul-fraction-ℤ x (add-fraction-ℤ y z))
( add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z))
left-distributive-mul-add-fraction-ℤ
(nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
( ap
Expand Down
18 changes: 18 additions & 0 deletions src/elementary-number-theory/multiplication-integers.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -378,6 +378,24 @@ interchange-law-mul-mul-ℤ =
associative-mul-ℤ
```

### Swapping the order of multiplication from one side

```agda
right-swap-mul-ℤ :
(x y z : ℤ) → (x *ℤ y) *ℤ z ＝ (x *ℤ z) *ℤ y
right-swap-mul-ℤ x y z =
associative-mul-ℤ x y z ∙
ap (x *ℤ_) (commutative-mul-ℤ y z) ∙
inv (associative-mul-ℤ x z y)

left-swap-mul-ℤ :
(x y z : ℤ) → x *ℤ (y *ℤ z) ＝ y *ℤ (x *ℤ z)
left-swap-mul-ℤ x y z =
inv (associative-mul-ℤ x y z) ∙
ap (_*ℤ z) (commutative-mul-ℤ x y) ∙
associative-mul-ℤ y x z
```

### Computing multiplication of integers that come from natural numbers

```agda
Expand Down
8 changes: 5 additions & 3 deletions src/elementary-number-theory/reduced-integer-fractions.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,14 @@ open import foundation.universe-levels

## Idea

A reduced fraction is a fraction in which its numerator and denominator are
coprime.
A {{#concept "reduced fraction" Agda=reduced-fraction-ℤ}} is a
[fraction](elementary-number-theory.integer-fractions.md) in which its
numerator and denominator are
[coprime](elementary-number-theory.relatively-prime-integers.md).

## Definitions

### Reduced fraction
### The predicate of being a reduced fraction

```agda
is-reduced-fraction-ℤ : fraction-ℤ → UU lzero
Expand Down

0 comments on commit 7952fc4

Please sign in to comment.