random issue: transporting definitions and theorems along...

Stream: triage

[Random Issue Bot]

Today I chose issue 408 for discussion!

transporting definitions and theorems along isomorphisms.
Created by @Kevin Buzzard (@kbuzzard) on 2018-10-08
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

I would say that this is still a relevant issue, although for the use cases I had in mind we have managed to work around the problems I was having in 2018 by learning not to use e.g. "the field of fractions of A" but instead to use "any ring satisfying the universal property which the field of fractions of A satisfies".

[Eric Wieser]

Do you have a link to an example of this workaround?

[Kevin Buzzard]

An integral domain is a commutative ring where $ab=0\implies a=0$ or $b=0$. Example: the integers. Given an integral domain $A$, one can formally invert all non-zero elements using some standard equivalence relation/equivalence class construction, and make a field $F=Frac(A)$, the so-called field of fractions of $A$. Mathematicians refer to this object as "the" field of fractions of $A$. But there's a subtlety here. If I were to abstractly implement the field of fractions construction on $\mathbb{Z}$ then I would start with the set $\mathbb{Z}\times(\mathbb{Z}-\{0\})$, put an equivalence relation on it ($(a,b)\sim (c,d)$ iff morally $a/b=c/d$, which I write as $ad=bc$), and the field of fractions $Frac(\mathbb{Z})$ of $\mathbb{Z}$ would be the equivalence classes.

As every mathematician knows, "the" field of fractions of $\mathbb{Z}$ is $\mathbb{Q}$. But thinking about it, this is not true in Lean, in the sense that rat is defined to be some inductive type consisting of a coprime pair $(n,d)$, not some quotient type like $Frac(\mathbb{Z})$. What is going on here? The quotient construction is not equal to rat, but it is isomorphic to rat, and furthermore there is a unique ring isomorphism from rat to the quotient which commutes with the natural maps from $\mathbb{Z}$ to each of these things.

This becomes an issue, because if I prove a theorem saying that if my integral domain $A$ has some property $X$ then its field of fractions has property $Y$, and then I prove that int has property $X$, I can't deduce that rat has property $Y$, I can only deduce that the field $Frac(\mathbb{Z})$ constructed by the equivalence classes has property $Y$.

In 2018 I wanted to proceed as follows: $Frac(\mathbb{Z})$ is isomorphic torat, and I know $Frac(\mathbb{Z})$ has property $Y$, and I want to map this property along the isomorphism $Frac(\mathbb{Z})\cong\mathbb{Q}$ to deduce it for $\mathbb{Q}$. To my horror, it was pointed out to me that there existed properties which could not be mapped along isomorphisms! These properties could be called "non-mathematical". For example, the property that something equals $Frac(\mathbb{Z})$ is true for $Frac(\mathbb{Z})$ but not true (or at least, not provable) for rat (one is an inductive type, the other is a quotient type). It's probably worth remarking that in a HoTT system, this problem does not occur: any property can be pushed along an isomorphism, although there are issues with computability (my understanding is that newer type theories are supposed to be trying to deal with this).

So what sounded like a trivial exercise suddenly became a complicated problem. In 2018 my vision was that there should be a system which tags a property as being "mathematical" (i.e. isomorphism-invariant) and a tactic which pushes mathematical structure along isomorphisms of mathematical objects.

However, such a tactic has not appeared, for several reasons; Scott Morrison wrote something, but Mario always complained that the problem had not been well-specified by the mathematicians, and then we discovered another approach, called at the time by me "Stricklandization" after Neil Strickland, but now often referred to here as the "characteristic predicate" approach.

The idea here is that $Frac(A)$ is uniquely defined up to unique isomorphism by some mathematical property -- for example one could use here that $Frac(A)$ has the property that for any field $K$ and any injective ring homomorphism $A\to K$, there's a unique way to extend it to a field homomorphism $Frac(A)\to K$ (and there are other choices -- there are several characteristic predicates typically). The idea now is not to prove many theorems or make much API about $Frac(A)$ itself, the explicit construction, but instead to prove theorems about all fields $F$ which satisfy the characteristic predicate. A simpler example would be the claim that one shouldn't be proving theorems about real, one should instead be proving theorems about complete archimedean ordered fields, because up to unique isomorphism the reals are the only one.

This approach is somehow better than the tactic approach, because one does not have to make the tactic! However the tactic approach is perhaps still of independent interest.

An example of where you can see the characteristic predicate approach is in dedekind_domain.lean. The definition of a Dedekind domain says that it's an integral domain $A$ which, amongst other things, is integrally closed in the field of fractions $Frac(A)$ that we explicitly construct as a quotient. However, immediately afterwards it is proved that $A$ is a Dedekind domain iff (all the other conditions +) it is integrally closed in any field satisfying the characteristic predicate. Here f : fraction_map A K means that $K$ satisfies the characteristic predicate for being isomorphic to the field of fractions of $A$ (rather than the stronger statement of being actually equal to the concrete construction fraction_ring A).

[Reid Barton]

I guess this is as good a time as any to mention that I've been working on this isomorphism invariance problem in https://github.com/rwbarton/scone/ although the project is still at an embryonic stage, probably largely incomprehensible without knowing the underlying theory, and on hold for the moment while I try to get a paper into shape.

[Reid Barton]

(Also, it's possible the approach I'm taking will fail for some reason that's not yet apparent.)

[Eric Wieser]

I suppose specifically what I was asking about was how you embedded the universal property in a structure, when the universal properties I've seen appear to quantify over universe parameters and therefore can't be bundled

[Eric Wieser]

Is there some trick to putting a universe-restricted lemma in the structure, and then deriving a universe-generic version from the restricted version using something like ulift?

[Reid Barton]

There's no trick for it in general, it's a real theorem you have to prove.

[Reid Barton]

I mean there might be some general schema of theorems of this type that can be proved using the same approach, but it's not just applying ulift. You have a universal property with respect to objects in one universe and you want it for objects in a bigger universe, so ulift would go the wrong way.

[Eric Wieser]

Perhaps the trick is just to have a free universe argument in the structure itself

[Eric Wieser]

And have theorems that use the structure instantiate it with a particular universe argument

[Mario Carneiro]

then how do you prove e.g. free_group.{u} X ~= free_group.{v} X when X : Type u?

[Eric Wieser]

My thinking was that if free_group were a typeclass, then I wouldn't ever need that proof

[Mario Carneiro]

well, the whole reason it's a universal object is because you want to hold the object fixed while talking about other groups

[Mario Carneiro]

otherwise you could just use the group itself