← Back to context

Comment by ndriscoll

1 year ago

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).

3 comments

ndriscoll

Reply
tobbe2064  1 year ago

Most people define it as the smallest set extending (the smallest set extending Z\{0} where * is invertible) where + is invertible

  • ndriscoll  1 year ago

    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.