What is a quotient?

Undergraduate mathematicians usually have a hard time defining functions from quotients in Lean, because they have been taught a specific model for quotients in their classes, which is not the model that Lean uses. This post is an attempt to explain what’s going on.

What are the natural numbers?

Before I start on what quotients are, let’s talk about what the natural numbers are. What is 37? What is it made of?

If you asked Euclid or Euler or Gauss or Riemann this question, they would think you were talking nonsense. 37 is a number, and it’s not made of anything. If you asked Peano, you would perhaps get a more nuanced answer: Peano might say that it doesn’t matter what 37 is made of, all that matters is that the natural numbers satisfy Peano’s axioms, because this is all you need to set up the theory (and if you don’t believe him, you should play the natural number game ).

But if you were to ask someone who knows something about the foundations of mathematics, they would say that it is possible to give an answer, but only after you have decided which foundations you are using. If you build mathematics within set theory then the natural numbers are a set, as is 37, and under the usual conventions we have that 37 is the set {0,1,2,3,…,36}. If you build things within type theory then the natural numbers are typically an inductive type, and 37 is the term succ (succ (succ (succ... (succ 0)))...) of this type. Finally, if you build mathematics within category theory then the natural numbers are typically an object of a certain category, and 37 will be a certain morphism from a terminal object into this natural number object.

But the point here is that the actual details of what 37 “is” do not matter. Gauss was proving quadratic reciprocity before any of these foundational theories were even proposed. All that matters is that the natural numbers, however they are modelled, satisfy Peano’s axioms. Peano’s axioms characterise the natural numbers uniquely up to unique isomorphism. In other words, if you have two models of the natural numbers and they both satisfy Peano’s axioms then those models are in a very strong sense “the same thing”.

Similarly, it doesn’t matter what the real numbers actually are, they can be a set, a type or an object of a category, and their elements can be Cauchy sequences, Dedekind cuts, Bourbaki uniform space completions, Eudoxus reals or whatever your favourite construction of the real numbers is; all that matters is that they are a complete archimedean ordered field. This hypothesis characterises the reals uniquely up to unique isomorphism, and you can build all of modern analysis from it (indeed my first analysis lecturer did just this: they developed all the basic theory of sequences, sums and integrals just from this assumption).

What is a quotient?

When I was a kid, I was into the maths olympiad scene, and I knew about the integers mod n. For example I knew that the integers mod 10 were {0,1,2,3,4,5,6,7,8,9} with addition and multiplication redefined so that if you go above 10 then you just subtract 10 until you’re back less than 10. For example 9 + 3 = 2 in the integers mod 10, because 10=0 and 11=1 and so on. This was my childhood model of the integers mod 10. But then I went to the University of Cambridge and there I was told by my algebra lecturer that this model was wrong. The integers mod 10, or as I was now expected to call them, were a quotient group, and so by definition the elements were cosets. Turns out that 3 wasn’t an element of the integers mod 10 after all, turns out that the thing I was calling 3 was actually the infinite set {...-17,-7,3,13,23,33,43,...}, or or [3].

At the time, I was confused, because I had hard evidence that my model for the integers mod 10 worked fine, and nobody had hauled me up on this when marking my solutions to olympiad questions. But it was explained to me that my idea of choosing a canonical set of coset representatives did not generalise well, and that I would be better off modelling quotients as sets of sets. Whatever. It took me decades to understand that this claim was not the end of the story (and I thank Patrick Massot for pointing this out to me).

The point of this post is to explain that, just as it doesn’t matter what the natural numbers are as long as they satisfy Peano’s axioms, and just as it doesn’t matter what the real numbers are as long as they are a complete ordered archimedean field, it also doesn’t matter what the elements of a quotient group are, as long as a certain axiom is satisfied, which will characterise quotient groups uniquely up to unique isomorphism.

“Well-defined” functions.

So what is the “axiom for quotients”? It is typically very well-hidden in an undergraduate mathematics curriculum, and is usually explained in terms which heavily rely on the “set of sets” model for quotients. The axiom is often not clearly stated (I looked back in my undergraduate notes and it never seems to be made explicit). However I do understand why not; the axiom is actually a universal property, which is quite an abstract concept. One would like to talk about things like quotient groups as early as possible in the mathematics curriculum (for example, to state the first isomorphism theorem for groups); but students are typically only told about universal properties in more advanced algebra courses covering, for example, tensor products and localisations (both of which are, uncoincidentally, constructed as quotients).

The axiom we seek is typically hidden behind this strange idea that a function is “well-defined”. Let’s keep running with our example of the additive group of integers mod 10. If we want to define a function to this set, it’s very easy. There is a canonical “reduction mod 10” function from the integers to the integers mod 10; let’s call it.

If we now have some other set and want to give a function from to, then one way to do so would simply be to give a function from to, and then just compose this with.

Given, we can just make by composing with.

If happens to be a group and happens to be a group homomorphism, then will also be a group homomorphism, because is. So we have a perfectly good way of defining maps into the quotient, which doesn’t rely on anything fancy. The fun starts when we want to define a map out of the quotient. This is where we have to check that something is “well-defined”.

Let’s work through a mathematically simple example to remind us of the “well-defined yoga” which we put undergraduates through. To know a positive integer mod 10 is to know its last digit, and if you know the last digit of a number then you can figure out if it’s even or odd. So there should be some natural map from the integers mod 10 to the set {Even,Odd}. Let’s write this map with a dotted arrow and then discuss how we can go about defining it.

We want to define the map and check it’s “well-defined”.

Let’s now run through the way we are formally taught how to construct. First we choose an integer mod 10, for example 8, or, as my algebra lecturer would have called it, [8]. Then we remember that secretly this element is actually an infinite set {...-12,-2,8,18,28,...}. So now we choose a random element in this set, for example 28. Now 28 is clearly even, so we define.

But there’s a catch! The catch is that at some point in the procedure we made a completely random choice of an element of an infinite set. What if we had chosen 108 or 1000008 instead? Well, here’s a funny thing: both 108 and 1000008 are also even, as indeed is every element of the equivalence class, so it didn’t actually matter which element we chose; we always got the same answer. This means that our definition of s([8]) is “well-defined”. Indeed, we can dress up the key point of this argument as a theorem:

Theorem. If x and y are integers which are congruent mod 10, then x is even if and only if y is even, and x is odd if and only if y is odd.

Proof. If x and y are congruent mod 10…