Zulip Chat Archive

Stream: triage

Topic: random issue: transporting definitions and theorems along...


view this post on Zulip Random Issue Bot (Oct 31 2020 at 14:13):

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?

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 14:17):

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

view this post on Zulip Eric Wieser (Oct 31 2020 at 22:27):

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

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 23:57):

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

As every mathematician knows, "the" field of fractions of Z\mathbb{Z} is Q\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)(n,d), not some quotient type like Frac(Z)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 Z\mathbb{Z} to each of these things.

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

In 2018 I wanted to proceed as follows: Frac(Z)Frac(\mathbb{Z}) is isomorphic torat, and I know Frac(Z)Frac(\mathbb{Z}) has property YY, and I want to map this property along the isomorphism Frac(Z)QFrac(\mathbb{Z})\cong\mathbb{Q} to deduce it for Q\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(Z)Frac(\mathbb{Z}) is true for Frac(Z)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)Frac(A) is uniquely defined up to unique isomorphism by some mathematical property -- for example one could use here that Frac(A)Frac(A) has the property that for any field KK and any injective ring homomorphism AKA\to K, there's a unique way to extend it to a field homomorphism Frac(A)KFrac(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)Frac(A) itself, the explicit construction, but instead to prove theorems about all fields FF 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 AA which, amongst other things, is integrally closed in the field of fractions Frac(A)Frac(A) that we explicitly construct as a quotient. However, immediately afterwards it is proved that AA 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 KK satisfies the characteristic predicate for being isomorphic to the field of fractions of AA (rather than the stronger statement of being actually equal to the concrete construction fraction_ring A).

view this post on Zulip Reid Barton (Nov 01 2020 at 01:25):

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.

view this post on Zulip Reid Barton (Nov 01 2020 at 01:30):

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

view this post on Zulip Eric Wieser (Nov 01 2020 at 11:44):

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

view this post on Zulip Eric Wieser (Nov 01 2020 at 11:45):

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?

view this post on Zulip Reid Barton (Nov 01 2020 at 11:48):

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

view this post on Zulip Reid Barton (Nov 01 2020 at 11:53):

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.

view this post on Zulip Eric Wieser (Nov 01 2020 at 12:05):

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

view this post on Zulip Eric Wieser (Nov 01 2020 at 12:06):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 12:09):

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

view this post on Zulip Eric Wieser (Nov 01 2020 at 12:12):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 12:16):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 12:16):

otherwise you could just use the group itself


Last updated: May 18 2021 at 23:14 UTC