nLab rational number

Rational numbers

Context

Arithmetic

Algebra

Rational numbers

Definition

A rational number is a fraction of two integer numbers.

As a field

The field of rational numbers, \mathbb{Q}, is the field of fractions of the commutative ring of integers, \mathbb{Z}, hence the field consisting of formal fractions (“ratios”) of integers.

As a commutative ring

Let ( +,1: +,s: + +)(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+) be the set of positive integers. The positive integers are embedded into every commutative ring RR: there is an injection inj: +Rinj:\mathbb{N}^+\to\R such that inj(1)=1inj(1) = 1 and inj(s(n))=inj(n)+1inj(s(n)) = inj(n) + 1 for all n: +n:\mathbb{N}^+.

Suppose RR has an injection inv: +Rinv:\mathbb{N}^+\to\R such that inj(n)inv(n)=1inj(n) \cdot inv(n) = 1 and inv(n)inj(n)=1\inv(n) \cdot \inj(n) = 1 for all n: +n:\mathbb{N}^+. Then RR is called a \mathbb{Q} -algebra, and the commutative ring of rational numbers \mathbb{Q} is the initial commutative \mathbb{Q}-algebra.

It can then be proven from the ring axioms and the properties of the integers that every rational number apart from zero and has a multiplicative inverse, making \mathbb{Q} a field.

As an sequential colimit in CRing

Let [1/n!]\mathbb{Z}[1/n!] be the localization of the integers \mathbb{Z} away from the factorial n!n!, and for each ii \in \mathbb{N}, there is a unique commutative ring homomorphism h i:[1/i!][1/(i+1)!]h_{i}:\mathbb{Z}[1/i!]\to\mathbb{Z}[1/(i + 1)!] defined by the universal property of localisation of [1/i!]\mathbb{Z}[1/i!] away from i+1i + 1. Then the commutative ring of rational numbers \mathbb{Q} is the sequential colimit of the diagram

[1/0!]h 0[1/1!]h 1[1/2!]h 2\mathbb{Z}[1/0!] \overset{h_0}\to \mathbb{Z}[1/1!] \overset{h_1}\to \mathbb{Z}[1/2!] \overset{h_2}\to \ldots

As an abelian group

Let ( +,1: +,s: + +)(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+) be the set of positive integers and let (,0,+,,1)(\mathbb{Z},0,+,-,1) be the free abelian group on the set 1{1}.

Let AA be an abelian group containing \mathbb{Z} as an abelian subgroup. The positive integers are embedded into the function abelian group AAA \to A, with id A:AAid_A:A \to A being the identity function on AA; i.e. there is an injection inj: +(AA)inj:\mathbb{N}^+\to (A \to A) such that inj(1)=id Ainj(1) = id_A and inj(s(n))=inj(n)+id Ainj(s(n)) = inj(n) + id_A for all n: +n:\mathbb{N}^+.

Suppose AA has an injection inv: +(AA)inv:\mathbb{N}^+\to (A \to A) such that for all n: +n:\mathbb{N}^+, inj(n)inv(n)=id Ainj(n) \circ inv(n) = id_A and inv(n)inj(n)=id Ainv(n) \circ inj(n) = id_A. Then the abelian group of rational numbers \mathbb{Q} is the initial such abelian group.

As an initial object in a category

Let \mathbb{Z} be the integers and let

#0{a|a<00<a}\mathbb{Z}_{#0} \coloneqq \{a \in \mathbb{Z} \vert a \lt 0 \vee 0 \lt a \}

be the set of integers apart from zero.

For lack of a better name, let us define a set with rational numbers to be a set AA with a function ι× #0A\iota \in \mathbb{Z} \times \mathbb{Z}_{#0} \to A with domain the Cartesian product × #0\mathbb{Z} \times \mathbb{Z}_{#0} and codomain AA, such that

a.b #0.c.d #0.(ad=cb)(ι(a,b)=ι(c,d))\forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}_{#0}. \forall c \in \mathbb{Z}. \forall d \in \mathbb{Z}_{#0}. (a \cdot d = c \cdot b) \implies (\iota(a, b) = \iota(c, d))

A homomorphism of sets with rational numbers between two sets with rational numbers AA and BB is a function fB Af \in B^A such that

a.b #0.f(ι A(a,b))=ι B(a,b)\forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}_{#0}. f(\iota_A(a, b)) = \iota_B(a, b)

The category of sets with rational numbers is the category SwRNSwRN whose objects Ob(SwRN)Ob(SwRN) are sets with rational numbers and whose morphisms Mor(A,B)Mor(A,B) for sets with rational numbers AOb(SwDF)A \in Ob(SwDF), BOb(SwRN)B \in Ob(SwRN) are homomorphisms of sets with rational numbers. The set of rational numbers, denoted \mathbb{Q}, is defined as the initial object in the category of sets with rational numbers.

 In dependent type theory

In dependent type theory, there are multiple different definitions of the type of rational numbers.

As a dependent sum type

Let \mathbb{Z} be the integers, let

0 a:max(a,a)>0\mathbb{Z}_{\neq 0} \coloneqq \sum_{a:\mathbb{Z}} \max(a,-a) \gt 0

be the non-zero integers, and let gcd:×\gcd:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} be the greatest common divisor on the integers. Then the rational numbers is defined as the type of pairs of integers and non-zero integers such that the greatest common divisor is equal to one:

x: y: 0gcd(x,π 1(y))= 1\mathbb{Q} \coloneqq \sum_{x:\mathbb{Z}} \sum_{y:\mathbb{Z}_{\neq 0}} \gcd(x, \pi_1(y)) =_\mathbb{Z} 1

We define the function ()/():× 0(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{\neq 0} \rightarrow \mathbb{Q} for all integers a:a:\mathbb{Z} and non-zero integers b: 0b:\mathbb{Z}_{\neq 0} by

a/b(a÷gcd(a,π 1(b)),π 1(b)÷gcd(a,π 1(b)),p(a,b))a/b \coloneqq (a \div \gcd(a, \pi_1(b)), \pi_1(b) \div \gcd(a, \pi_1(b)), p(a, b))

where p(a,b)p(a, b) is the witness that the greatest common divisor of a÷gcd(a,π 1(b))a \div \gcd(a, \pi_1(b)) and π 1(b)÷gcd(a,π 1(b))\pi_1(b) \div \gcd(a, \pi_1(b)) is equal to 1, and a÷ba \div b is integer division, since integers are an Euclidean domain and thus have a division and remainder operation.

As a higher inductive type

In homotopy type theory, the type of rational numbers, denoted \mathbb{Q}, is defined (UBP13, §11.1) as the higher inductive type generated by:

  • A function ()/():× 0(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{\neq 0} \rightarrow \mathbb{Q}, where

    0 a:max(a,a)>0\mathbb{Z}_{\neq 0} \coloneqq \sum_{a:\mathbb{Z}} \max(a,-a) \gt 0
  • A dependent product of functions between identities representing that equivalent fractions are equal:

    equivfrac: a: b: 0 c: d: 0(aπ 1(d)=cπ 1(b))(a/b=c/d),equivfrac : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}_{\neq 0}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{Z}_{\neq 0}} (a \cdot \pi_1(d) = c \cdot \pi_1(b)) \to (a/b = c/d)\,,
  • A set-truncator

    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)

Properties

Let ii be the inclusion of the non-zero integers into the integers.

Commutative ring structure on the rational numbers

Definition

The rational number zero 00 \in \mathbb{Q} is defined as

00/10 \coloneqq 0/1
Definition

The binary operation addition ()+():×(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

a/b+c/d(ai(d)+ci(b))/(bd)a/b + c/d \coloneqq (a \cdot i(d) + c \cdot i(b))/(b \cdot d)

for aina \ in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}, cc \in \mathbb{Z}, d #0d \in \mathbb{Z}_{#0}.

Proposition

For any qq \in \mathbb{Q} and rr \in \mathbb{Q}, q+r=r+qq + r = r + q.

Proof

TODO

Definition

The unary operation negation ():-(-):\mathbb{Q} \to \mathbb{Q} is defined as

(a/b)(a)/b-(a/b) \coloneqq (-a)/b

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}

Definition

The binary operation subtraction ()():×(-)-(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

a/bc/d(ai(d)ci(b))/(bd)a/b - c/d \coloneqq (a \cdot i(d) - c \cdot i(b))/(b \cdot d)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}, cc \in \mathbb{Z}, d #0d \in \mathbb{Z}_{#0}

Definition

The rational number one 11 \in \mathbb{Q} is defined as

11/11 \coloneqq 1/1
Definition

The binary operation multiplication ()():×(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

a/bc/d(ac)/(bd)a/b \cdot c/d \coloneqq (a \cdot c)/(b \cdot d)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}, cc \in \mathbb{Z}, d #0d \in \mathbb{Z}_{#0}

Definition

The right \mathbb{N}-action exponentiation () ():×(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q} is defined as

(a/b) n(a n)/(b n)(a/b)^n \coloneqq (a^n)/(b^n)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}, nn \in \mathbb{N}.

This makes the rational numbers into a commutative ring.

Order structure on the rational numbers

Definition

The predicate is positive, denoted as isPositive(a/b)isPositive(a/b), is defined as

isPositive(a/b)(a>0)(i(b)>0)(a<0)(i(b)<0)isPositive(a/b) \coloneqq (a \gt 0) \wedge (i(b) \gt 0) \vee (a \lt 0) \wedge (i(b) \lt 0)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The predicate is negative, denoted as isNegative(a/b)isNegative(a/b), is defined as

isNegative(a/b)(a>0)(i(b)<0)(a<0)(i(b)>0)isNegative(a/b) \coloneqq (a \gt 0) \wedge (i(b) \lt 0) \vee (a \lt 0) \wedge (i(b) \gt 0)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The predicate is zero, denoted as isZero(a/b)isZero(a/b), is defined as

isZero(a/b)a=0isZero(a/b) \coloneqq a = 0

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The predicate is non-positive, denoted as isNonPositive(a/b)isNonPositive(a/b) is defined as

isNonPositive(a/b)¬isPositive(a/b)isNonPositive(a/b) \coloneqq \neg isPositive(a/b)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The predicate is non-negative, denoted as isNonNegative(a/b)isNonNegative(a/b), is defined as

isNonNegative(a/b)¬isNegative(a/b)isNonNegative(a/b) \coloneqq \neg isNegative(a/b)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The predicate is non-zero, denoted as isNonZero(a/b)isNonZero(a/b), is defined as

isNonZero(a/b)isPositive(a/b)isNegative(a/b)isNonZero(a/b) \coloneqq isPositive(a/b) \vee isNegative(a/b)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}.

Definition

The relation is less than, denoted as p<qp \lt q, is defined as

p<qisPositive(qp)p \lt q \coloneqq isPositive(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The dependent type is greater than, denoted as p>qp \gt q, is defined as

p<qisNegative(qp)p \lt q \coloneqq isNegative(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The dependent type is apart from, denoted as p#qp \# q, is defined as

p<qisNonZero(qp)p \lt q \coloneqq isNonZero(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The dependent type is less than or equal to, denoted as pqp \leq q, is defined as

p<qisNonNegative(qp)p \lt q \coloneqq isNonNegative(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The dependent type is greater than or equal to, denoted as pqp \leq q, is defined as

p<qisNonPositive(qp)p \lt q \coloneqq isNonPositive(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Pseudolattice structure on the rational numbers

Definition

The ramp function ramp:ramp:\mathbb{Q} \to \mathbb{Q} is defined as

ramp(a/b)(ramp(a)ramp(i(b))+ramp(a)ramp(i(b)))/(bb)ramp(a/b) \coloneqq (ramp(a) \cdot ramp(i(b)) + ramp(-a) \cdot ramp(i(-b)))/(b \cdot b)

for aa \in \mathbb{Z}, b #0b \in \mathbb{Z}_{#0}, ramp:ramp:\mathbb{Z} \to \mathbb{Z}.

Definition

The minimum min:×min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

min(p,q)pramp(pq)\min(p,q) \coloneqq p - ramp(p - q)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The maximum max:×max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

max(p,q)p+ramp(qp)\max(p, q) \coloneqq p + ramp(q - p)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Definition

The absolute value |()|:\vert(-)\vert:\mathbb{Q} \to \mathbb{Q} is defined as

|p|max(p,p)\vert p \vert \coloneqq \max(p, -p)

for p:p:\mathbb{Q}.

Definition

The metric ρ:×\rho:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

ρ(p,q)max(p,q)min(p,q)\rho(p, q) \coloneqq \max(p, q) - \min(p, q)

for p:p:\mathbb{Q}, q:q:\mathbb{Q}.

Uniform structure on the rational numbers

We define the ternary relation x ϵyρ(x,y)<ϵx \sim_\epsilon y \coloneqq \rho(x, y) \lt \epsilon for xx \in \mathbb{Q}, yy \in \mathbb{Q}, and ϵ +\epsilon \in \mathbb{Q}_+, called “xx and yy are within a distance of ϵ\epsilon”. One could show that the rational numbers are a uniform space with respect to the uniformity ternary relation x ϵyx \sim_\epsilon y.

  1. For every xx \in \mathbb{Q} and ϵ +\epsilon \in \mathbb{Q}_+, x ϵxx \sim_\epsilon x

  2. For every xx \in \mathbb{Q}, yy \in \mathbb{Q}, zz \in \mathbb{Q} and δ +\delta \in \mathbb{Q}_+, ϵ +\epsilon \in \mathbb{Q}_+, x δyx \sim_\delta y and y ϵzy \sim_\epsilon z implies that x δ+ϵzx \sim_{\delta + \epsilon} z.

  3. For every xx \in \mathbb{Q}, yy \in \mathbb{Q} and ϵ +\epsilon \in \mathbb{Q}_+, x ϵyx \sim_\epsilon y implies that y ϵxy \sim_\epsilon x.

  4. For every xx \in \mathbb{Q}, yy \in \mathbb{Q}, x 1yx \sim_1 y if and only if ρ(x,y)<1\rho(x, y) \lt 1.

  5. For every xx \in \mathbb{Q}, yy \in \mathbb{Q} and δ +\delta \in \mathbb{Q}_+, ϵ +\epsilon \in \mathbb{Q}_+, x min(δ,ϵ)yx \sim_{\min(\delta, \epsilon)} y implies that x δyx \sim_{\delta} y and x ϵyx \sim_{\epsilon} y.

  6. For every xx \in \mathbb{Q}, yy \in \mathbb{Q} and δ +\delta \in \mathbb{Q}_+, ϵ +\epsilon \in \mathbb{Q}_+, δϵ\delta \leq \epsilon and x δyx \sim_{\delta} y implies that x ϵyx \sim_{\epsilon} y.

Algebraic closure

The algebraic closure ¯\overline{\mathbb{Q}} of the rational numbers is called the field of algebraic numbers. The absolute Galois group Gal(¯|)Gal(\overline{\mathbb{Q}}\vert \mathbb{Q}) has some curious properties, see there.

Topologies

There are several interesting topologies on \mathbb{Q} that make \mathbb{Q} into a topological group under addition, allowing us to define interesting fields by taking the completion with respect to this topology:

  1. The discrete topology is the most obvious, which is already complete.

  2. The absolute-value topology is defined by the metric d(x,y)|xy|d(x,y) \coloneqq {|x - y|}; the completion is the field of real numbers. The rational numbers are thus a Hausdorff space.

    (This topology is totally disconnected (this exmpl.))

  3. Fixing a prime number pp, the pp-adic topology is defined by the ultrametric d(x,y)1/nd(x,y) \coloneqq 1/n where nn is the highest exponent on pp in the prime factorization of |xy|{|x - y|}; the completion is the field of pp-adic numbers.

According to Ostrowski's theorem this are the only possibilities.

Interestingly, (2) cannot be interpreted as a localic group, although the completion \mathbb{R} can. (Probably the same holds for (3); I need to check.)

Analysis

One could analytically define the concepts of limit of a function and continuous function with respect to the absolute-value topology, and prove that the limit of a function satisfy the algebraic limit theorem. Since the reciprocal function on the rational numbers is well defined for non-zero rational numbers 0\mathbb{Q}_{\neq 0}, given a continuous function f:If:I \to \mathbb{Q} for open interval II \subseteq \mathbb{Q} the difference quotient function exists and thus the derivative is well-defined for continuous functions. One could thus define smooth functions on the rational numbers, and because the rational numbers are a Hausdorff space, analytic functions on the rational numbers, despite the fact that the rational numbers are a totally disconnected space.

For example,

  • A rational metric space is a type XX with a function d X:X×X 0d_X:X \times X \to \mathbb{Q}_{\geq 0} such that

    • for all xXx \in X and yXy \in X, d X(x,y)=d X(y,x)d_X(x, y) = d_X(y, x)
    • for all xXx \in X, yXy \in X, and zXz \in X, d X(x,z)d X(x,y)+d X(y,z)d_X(x, z) \leq d_X(x, y) + d_X(y, z)
    • for all xXx \in X, x=yd X(x,y)=0x = y \iff d_X(x, y) = 0

One could show that any open interval, half-open interval, and closed interval in the rational numbers is a rational metric space, with its metric inherited from the Euclidean metric on the rational numbers d (x,y)=|ab|d_\mathbb{Q}(x, y) = {|a - b|}. Thus one could do analysis with partial functions in the rational numbers, such as the reciprocal function x1xx \mapsto \frac{1}{x} and the rational functions on the rational numbers.

Then, given a rational metric space (X,d X)(X, d_X):

  • if it exists, the (Weierstrass) limit of a function f:Xf:X \to \mathbb{Q} from XX to the rational numbers approaching an element aXa \in X is a rational number LL \in \mathbb{Q} with a function on the positive rational numbers M: + +M:\mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵ +\epsilon \in \mathbb{Q}_+ and for all elements bXb \in X, 0<d X(a,b)<M(ϵ)0 \lt d_X(a, b) \lt M(\epsilon) implies |f(b)L|<ϵ{|f(b) - L|} \lt \epsilon

  • similarly, if it exists, the (Bourbaki) limit of a function f:Xf:X \to \mathbb{Q} from XX to the rational numbers approaching an element aXa \in X is a rational number LL \in \mathbb{Q} with a function on the positive rational numbers M: + +M:\mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵ +\epsilon \in \mathbb{Q}_+ and for all elements bXb \in X, d X(a,b)<M(ϵ)d_X(a, b) \lt M(\epsilon) implies |f(b)L|<ϵ{|f(b) - L|} \lt \epsilon

  • a pointwise continuous function from XX to the rational numbers is a function f:Xf:X \to \mathbb{Q} with a function from XX to the set of endofunctions on the positive rational numbers M:X + +M:X \to \mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵ +\epsilon \in \mathbb{Q}_+ and for all rational numbers aXa \in X and bXb \in X, δ X(a,b)<M(a,ϵ)\delta_X(a, b) \lt M(a, \epsilon) implies that |f(a)f(b)|<ϵ{|f(a) - f(b)|} \lt \epsilon.

  • a uniformly continuous function from XX to the rational numbers is a function f:Xf:X \to \mathbb{Q} with a function on the positive rational numbers M: + +M:\mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵ +\epsilon \in \mathbb{Q}_+ and for all elements numbers aXa \in X and bXb \in X, δ X(a,b)<M(ϵ)\delta_X(a, b) \lt M(\epsilon) implies that |f(a)f(b)|<ϵ{|f(a) - f(b)|} \lt \epsilon.

Now, given an injection i:Xi:X \hookrightarrow \mathbb{Q}, so that XX is a subset of the rational numbers,

  • a pointwise differentiable function from XX to the rational numbers is a function f:Xf:X \to \mathbb{Q} with a derivative function f:Xf':X \to \mathbb{Q} on the rational numbers and a function from XX to the set of endofunctions on the positive rational numbers M:X + +M:X \to \mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵQ +\epsilon \in \mathrm{Q}_+ and for all elements aXa \in X and bXb \in X, |f(a)f(b)|<M(a,ϵ){|f(a) - f(b)|} \lt M(a, \epsilon) implies that

    |f(b)f(a)f(a)(i(b)i(a)))|<ϵ|f(a)f(b)|{|f(b) - f(a) - f'(a)(i(b) - i(a)))|} \lt \epsilon {|f(a) - f(b)|}
  • a uniformly differentiable function from XX to the rational numbers is a function f:Xf:X \to \mathbb{Q} with a derivative function f:Xf':X \to \mathbb{Q} on the rational numbers and a function on the positive rational numbers M: + +M:\mathbb{Q}_+ \to \mathbb{Q}_+ such that for all positive rational numbers ϵQ +\epsilon \in \mathrm{Q}_+ and for all elements aXa \in X and bXb \in X, |f(a)f(b)|<M(ϵ){|f(a) - f(b)|} \lt M(\epsilon) implies that

    |f(b)f(a)f(a)(i(b)i(a)))|<ϵ|f(a)f(b)|{|f(b) - f(a) - f'(a)(i(b) - i(a)))|} \lt \epsilon {|f(a) - f(b)|}
  • a smooth function in rational numbers is a function f:f:\mathbb{Q} \to \mathbb{Q} with a sequence of functions D ()f:()D^{(-)}f:\mathbb{N} \to (\mathbb{Q} \to \mathbb{Q}) and a sequence of functions M ()f:( + +)M^{(-)}f:\mathbb{N} \to (\mathbb{Q}_+ \to \mathbb{Q}_+) in the positive rational numbers, such that

    • for every element xXx \in X, (D 0f)(x)=f(x)(D^{0}f)(x) = f(x)

    • for every natural number nn \in \mathbb{N}, for every positive rational number ϵ +\epsilon \in \mathbb{Q}_+, for every rational number hh \in \mathbb{Q} such that 0<|h|<M nf(ϵ)0 \lt | h | \lt M^{n}f(\epsilon), and for every rational number xx \in \mathbb{Q},

|f(x+h) i=0 nh i(D if)(x)i!|<ϵ|h n|\left|f(x + h) - \sum_{i=0}^n \frac{h^i (D^{i}f)(x)}{i!}\right| \lt \epsilon |h^n|

Alternatively, we could use infinitesimals. Let [ϵ]/(ϵ 2=0)\mathbb{Q}[\epsilon]/(\epsilon^2 = 0) be the dual rational numbers, and let [[ϵ]]\mathbb{Q}[[\epsilon]] be the commutative ring of formal power series on the rational numbers. The former is equivalent to the product ×\mathbb{Q} \times \mathbb{Q} and the latter is equivalent to the function set \mathbb{Q}^\mathbb{N}.

Both of these are commutative rational algebras with ring homomorphism h:[ϵ]/(ϵ 2=0)h:\mathbb{Q} \to \mathbb{Q}[\epsilon]/(\epsilon^2 = 0) and k:[[ϵ]]k:\mathbb{Q} \to \mathbb{Q}[[\epsilon]].

  • A function f:Xf:X \to \mathbb{Q} is differentiable if it has a function lift f:[ϵ]/(ϵ 2=0)[ϵ]/(ϵ 2=0)\mathrm{lift}_f:\mathbb{Q}[\epsilon]/(\epsilon^2 = 0) \to \mathbb{Q}[\epsilon]/(\epsilon^2 = 0) such that lift f(h(i(a)))=h(i(a))\mathrm{lift}_f(h(i(a))) = h(i(a)) and a function f:Xf':X \to \mathbb{Q} such that for all elements aXa \in X,
lift f(h(i(a))+ϵ)=h(i(a))+h(f(a))ϵ\mathrm{lift}_f(h(i(a)) + \epsilon) = h(i(a)) + h(f'(a)) \epsilon
  • A function f:Xf:X \to \mathbb{Q} is smooth if it has a function lift f:[[ϵ]][[ϵ]]\mathrm{lift}_f:\mathbb{Q}[[\epsilon]] \to \mathbb{Q}[[\epsilon]] such that lift f(h(i(a)))=h(i(a))\mathrm{lift}_f(h(i(a))) = h(i(a)) and a sequence of functions d fdx :×X\frac{d^{-} f}{d x^{-}}:\mathbb{N} \times X \to \mathbb{Q} with d 0fdx 0(a)=a\frac{d^0 f}{d x^0}\left(a\right) = a for all aXa \in X, such that for all natural numbers nn \in \mathbb{N}
    lift f(h(j(a))+ϵ)= i=0 1i!h(d ifdx i(a))ϵ i\mathrm{lift}_f(h(j(a)) + \epsilon) = \sum_{i = 0}^{\infty} \frac{1}{i!} h\left(\frac{d^i f}{d x^i}\left(a\right)\right) \epsilon^i

References

See also:

Discussion in univalent foundations of mathematics (homotopy type theory with the univalence axiom):

and specifically in Agda:

Last revised on November 5, 2023 at 02:34:23. See the history of this page for a list of all contributions to it.