Comment by zarzavat
1 year ago
This doesn’t sound right to me. The rational numbers are a superset of the integers. We know that there’s only one 1 in the rational numbers, then it must be the same 1 object as the 1 in the integers.
The statement “3/3 is in Z” is true. There’s no conversion happening: 3/3 is a notation for 1, just like 0.999… is a notation for 1. Many notations, but only one 1 object.
The case of R x R^2 = R^3 is different because the Cartesian product is defined to produce a set of ordered pairs. So it cannot give rise to a set of triples any more than a dog can give birth to a cat. So either x is not a Cartesian product or = is isomorphism not equality.
Your statements such as
> We know that there’s only one 1 in the rational numbers, then it must be the same 1 object as the 1 in the integers. > The statement “3/3 is in Z” is true.
make it sound very trivial while in reality it is not. I do not quite understand your example with R^3 but the defined applies equally to your statements. There are many ways to define and think about the objects you mentioned -- there is not one single truth. Unless you are a devoted platonist, in which case, it's still like your opinion, man.
Q is (usually) a set of equivalence classes of ZxZ\{0}, so obviously it's not a superset of Z since they're not even the same types of things.
There is however a canonical embedding of Z into Q, sending n to the class of (n,1).
Most people define it as the smallest set extending (the smallest set extending Z\{0} where * is invertible) where + is invertible
How do you "extend" Z (what are you adding to it)? How do you prove there is a field containing Z? Assuming you are working in ZFC, what is an example of an element of Q? What is an example of an element of Z?
One way to do things is to define N as von Neumann ordinals:
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...
Then you define Z as an equivalence relation of NxN by the equivalence (a,b) ~ (c,d) iff a+d=c+b. This means each integer is itself an infinite set of pairs of natural numbers.
Then you define Q as an equivalence relation of ZxZ\{0} by (a,b) ~ (c,d) iff ad = cb. Again, each rational is now an infinite set of pairs of integers.
The point of the OP post is that we want to define things by their properties, but then we are defining what a set of rational numbers is, not what the set of rational numbers is, and we need to make sure we do all proofs in terms of the properties we picked (e.g. that Q is a field, there is a unique injective ring homomorphism i_ZQ: Z->Q, and if F is a field such that there is an injective ring homomorphism i_ZF: Z->F, then there is a unique field homomorphism i_QF: Q->F such that i_ZF = i_QF after i_ZQ) rather than relying on some specific encoding and handwaving that the proof translates to other encodings too. This might be easier or harder to do depending on which properties we use to characterize the thing, and the OP paper gives adding inverses to a ring as one of its examples in section 5 ("localization" is a generalization of the process of constructing Q from Z. For example, you could just add inverses for powers of 2 without adding inverses of other primes), proposing a different set of properties that they assert is easier to work with in Lean.
But such a set is not unique...
0.999… always reminds me of my favorite definition of the real numbers:
“A real number is a quantity x that has a decimal expansion
x = n + 0.d₁d₂d₃…, (1)
where n is an integer, each dᵢ is a digit between 0 and 9, and the sequence of digits doesn't end with infinitely many 9s. The representation (1) means that
n + d₁/10 + d₂/100 + ⋯ + dₖ/10^k ≤ x < n + d₁/10 + d₂/100 + ⋯ + dₖ/10^k + 1/10^k
for all positive integers k.”[1]
Defining the reals in terms of binary expansion is left as an exercise for the reader[2].
[1] Knuth, The Art of Computer Programming, Volume 1, Third Edition, p. 21.
[2] Ibid., p. 25, exercise 5.
You can easily define a Cartesian product that works on more than two sets at a time. See https://en.wikipedia.org/wiki/Cartesian_product#Cartesian_pr...
In the formalization of mathematics, things are built up structurally. Zero is the empty set. Natural numbers are sets that contain smaller natural numbers. Integers are pairs of natural numbers under an equivalence relation (a,b) ~ (c,d) if a + d = c + b. Rationals are pairs of integers under the equivalence relationship as above but if a * d = c * b. Reals are bounded sets of rationals (e.g. all the rationals q such that q * q < 2). Complex numbers are pairs of reals with addition and multiplication defined with i^2 = -1. Functions are really large sets with ordered pair (x,y) in the set f means f(x) = y. Etc.