[FOM] Foundational Challenge

[Timothy Y. Chow]

On Sat, 11 Jan 2020, Harvey Friedman wrote:
> We go merrily along in this style. What is the simplest case where a 
> nasty time consuming situation arises? There may be some need to know 
> something about the isomorphisms themselves. Of course, here we might as 
> well prove that for two relevant gadgets, there is a unique isomorphism.

I understand why you repeatedly ask for the "simplest nontrivial case," 
but I suspect that this may be akin to asking for the smallest number of 
grains of sand in a heap.

That is, there is a good chance that any specific example that one might 
try to exhibit ends up being trivial to handle.  This doesn't necessarily 
mean that problems can't pile up to the point where they become a 
significant nuisance to handle.

Part of the problem is that working in an isomorphism-invariant way is 
something that mathematicians do instinctively.  It's often not written 
down, and the appropriate notion of "isomorphism" can switch from one 
context to another without warning.

Having stated my reservations about the wisdom of trying to give explicit 
examples, I will now propose a strawman example to think about: An 
elliptic curve.  What is an elliptic curve?

A colloquium lecturer might define an elliptic curve by writing down the 
equation

   y^2 = x^3 + ax + b

and saying that an elliptic curve is defined by an equation of this form, 
subject to a non-singularity condition, which can be expressed by the 
inequality

   4a^3 + 27b^2 != 0.

So far, this doesn't look too bad.  However, as soon as one starts to be 
more careful, annoying issues start to arise.  First of all, where do the 
coefficients a and b live?  Well, they're supposed to live in some field. 
Any field, you ask?  Um, well, as long as the characteristic isn't 2 or 3, 
because then you have to use a slightly different form of the equation. 
Okay, fine.  So let's start over.  Let's use a canonical form that is 
valid in arbitrary characteristic.  Are we done yet?

Of course not.  We don't want to say that the elliptic curve defined by 
the equation y^2 = x^3 - x is literally that equation.  The curve is 
supposed to live in some geometric space.  The affine plane, perhaps?  No, 
usually we are interested in projective space.  After all, we usually want 
the point at infinity to be the base point O.  Oops, did I forget to say 
that an elliptic curve is supposed to have a base point?

So maybe an elliptic curve is really a set of points in the projective 
plane (satisfying a certain equation)?  No, that's not right.  Two 
different sets of points might define *isomorphic* elliptic curves, and we 
don't want to think of them as "different" curves.  Worse, thinking of a 
curve as a set of points in a geometric space over a fixed field is a 
mistake anyway.  The curve is *defined* over some field (this is the field 
where the coefficients a and b live), but one typically wants to be able 
to perform "base change" freely.  We might want to think of y^2 = x^3 - x 
over a finite field, or over the complex numbers.  The curve itself should 
not be confused with its set of F-rational points over any particular 
field F.

So maybe we should start by setting up a category and defining the 
relevant morphisms.  If we're going to go to all that trouble, then 
perhaps we shouldn't limit ourselves to elliptic curves.  After all, 
elliptic curves are just the special case of genus one.  So maybe we 
should define elliptic curves as smooth curves of genus one?  With a base 
point, of course.  Let's not worry about Neron models for now.  Hold on, 
we're going to want to talk about the conductor of an elliptic curve.  Can 
we do that without Neron models?  Hmmm...

In practice, of course, one does not work at a maximum level of generality 
at the outset.  For elementary calculations, one introduces a naive 
definition that suffices for the purposes at hand.  We instinctively know 
what kind of "isomorphism" is needed.  If we need more abstraction then we 
introduce it, and we "know" that everything we have proved in an 
isomorphism-invariant manner still carries over to our new notion of 
isomorphism.

If we want to formalize everything, though, then we can't cut corners.  We 
have to carefully define isomorphism at each step.  We also want to make 
sure that if we then subtly change our notion of isomorphism in a 
"manifestly legal manner" then we don't have to re-prove everything from 
scratch.

Now, there's going to a certain amount of unavoidable overhead here, no 
matter what foundational approach you use.  I don't fully understand what 
the Univalence Axiom says, but regardless of what it is, there is not 
going to be any way to get around having to sit down at some point and say 
what it means for two things to be isomorphic.  No approach is going to 
magically make all this honest toil disappear completely.  The question, 
however, is whether there is some approach that will make it easier to 
"grow" one's database of mathematical knowledge in a graceful manner, that 
doesn't require re-programming everything from scratch when a slightly 
more general abstraction is introduced.

To be even more concrete, how about this?  Suppose we start with the 
equational form y^2 = ax^3 + b, and we define the group law on the 
elliptic curve and prove that it is associative.  Then we belatedly 
realize that we're interested in characteristics 2 and 3.  Unavoidably, we 
have to introduce a new equational form, and provide a proof that works in 
those cases.  Suppose we have a separate argument that works in 
characteristics 2 and 3 only.  Can we make a smooth transition, and reuse 
the associativity proof from before to cover characteristics other than 2 
and 3, even though we've changed our definition of the isomorphism class 
of an elliptic curve?  We have to do some work to show that our old and 
new definitions are "equivalent," of course, but what we'd like to avoid 
is re-writing all our old proofs in terms of the new definitions.

Tim