Zulip Chat Archive

Stream: maths

Topic: promoting equiv


Kevin Buzzard (Apr 10 2018 at 09:13):

In mathematics, people constantly invoke the idea that an object is "defined up to unique isomorphism".

Kevin Buzzard (Apr 10 2018 at 09:14):

I have seen this really full in the face in my work on schemes

Kevin Buzzard (Apr 10 2018 at 09:15):

I am defining a certain gadget in algebraic geometry called "the structure sheaf on an affine scheme"

Kevin Buzzard (Apr 10 2018 at 09:16):

and in the mathematics literature it typically goes like this: "the open set is of the form D(f)D(f) (f is an element of a ring) and define the structure sheaf on this set to be R[1/f]R[1/f]" (this is just some ring)

Kevin Buzzard (Apr 10 2018 at 09:16):

and the catch is that the open set can be of the form D(g)D(g) for other elements gg of the ring

Kevin Buzzard (Apr 10 2018 at 09:17):

but R[1/f]R[1/f] and R[1/g]R[1/g] are isomorphic

Kevin Buzzard (Apr 10 2018 at 09:17):

and moreover there is a unique isomorphism between R[1/f]R[1/f] and R[1/g]R[1/g] which has some properties, and this is the isomorphism which mathematicians use to hide behind the issue that they have not actually defined the structure sheaf on this open set.

Kevin Buzzard (Apr 10 2018 at 09:18):

Now if this isomorphism were an equality, then eq.rec would be really helpful

Kevin Buzzard (Apr 10 2018 at 09:19):

because I would be able to promote a claim involving R[1/f]R[1/f] to a claim involving any R[1/g]R[1/g]

Kevin Buzzard (Apr 10 2018 at 09:19):

But it's not an equality -- R[1/f]R[1/f] and R[1/g]R[1/g] are most definitely different types

Gabriel Ebner (Apr 10 2018 at 09:19):

You can make it into an equality, by taking a quotient on the ring extensions. Not sure this makes it any simpler, though.

Kevin Buzzard (Apr 10 2018 at 09:20):

However there is a special map R[1/f]R[1/g]R[1/f]\to R[1/g]

Kevin Buzzard (Apr 10 2018 at 09:20):

which I can produce

Kevin Buzzard (Apr 10 2018 at 09:20):

with an inverse

Kevin Buzzard (Apr 10 2018 at 09:21):

and I think what I want is a recursor which enables me to effortlessly change between these rings

Kevin Buzzard (Apr 10 2018 at 09:21):

and just push through all the theorems I want

Kevin Buzzard (Apr 10 2018 at 09:21):

from theorems about R[1/f]R[1/f]

Gabriel Ebner (Apr 10 2018 at 09:21):

Hmm, do you care about elements of R[1/f]R[1/f]?

Kevin Buzzard (Apr 10 2018 at 09:21):

to theorems about any choice of R[1/g]R[1/g].

Kevin Buzzard (Apr 10 2018 at 09:21):

I do care about elements of R[1/f]R[1/f]

Kevin Buzzard (Apr 10 2018 at 09:22):

however

Kevin Buzzard (Apr 10 2018 at 09:22):

because I am doing maths and not type theory

Kevin Buzzard (Apr 10 2018 at 09:22):

there is some sort of implicit understanding

Kevin Buzzard (Apr 10 2018 at 09:22):

that any theorem I prove will only depend on my object up to "canonical isomorphism"

Kevin Buzzard (Apr 10 2018 at 09:22):

and the map R[1/f]R[1/g]R[1/f]\to R[1/g] is a canonical isomorphism

Kevin Buzzard (Apr 10 2018 at 09:23):

The word "canonical" does not have a general definition, but in any given case one can supply one

Kevin Buzzard (Apr 10 2018 at 09:23):

for example in this case I can supply some technical maths definition of the form "the unique map with some property"

Kevin Buzzard (Apr 10 2018 at 09:24):

But I do have maps between products of such rings and want to make claims about sets of elements which go to certain other sets of elements

Kevin Buzzard (Apr 10 2018 at 09:24):

And whilst I have not yet embarked upon writing what will be the last proof that I will need for proving that an affine scheme is a scheme

Kevin Buzzard (Apr 10 2018 at 09:24):

I have planned the proof

Kevin Buzzard (Apr 10 2018 at 09:25):

and I know that at some point I will have to replace R[1/f]R[1/f] with R[1/g]R[1/g] and instantly I will be hit with 10 proof obligations

Kevin Buzzard (Apr 10 2018 at 09:25):

all of which will be of the form "you need to check that the composite of this canonical map with this canonical map is this canonical map"

Kevin Buzzard (Apr 10 2018 at 09:26):

I know how to prove all of these things

Kevin Buzzard (Apr 10 2018 at 09:26):

but I was idly wondering whether I could set up the infrastructure more cleverly

Kevin Buzzard (Apr 10 2018 at 09:26):

because I have just been reading about UniMath

Kevin Buzzard (Apr 10 2018 at 09:26):

and I see that equality is not a Prop there

Kevin Buzzard (Apr 10 2018 at 09:27):

and indeed equality is much more strongly related to equiv than in DTT

Kevin Buzzard (Apr 10 2018 at 09:27):

which made me think that maybe I was missing a trick here.

Kevin Buzzard (Apr 10 2018 at 09:28):

I think that perhaps the way forward here is to actually write the proof

Kevin Buzzard (Apr 10 2018 at 09:28):

and when the explosion of obligations occurs

Kevin Buzzard (Apr 10 2018 at 09:28):

to really think about the simp lemmas I need to kill all of them

Kevin Buzzard (Apr 10 2018 at 09:28):

(or maybe they won't be valid lemmas for simp)

Kevin Buzzard (Apr 10 2018 at 09:28):

and then to ask again.

Andrew Ashworth (Apr 10 2018 at 09:29):

is transfer as written for the integers at all helpful? here's the paper from isabelle (https://www21.in.tum.de/~kuncar/documents/huffman-kuncar-cpp2013.pdf)

Johannes Hölzl (Apr 10 2018 at 09:29):

transfer is not only for integers

Andrew Ashworth (Apr 10 2018 at 09:29):

of course, i only meant in lean that's where you'll find it used

Kevin Buzzard (Apr 10 2018 at 09:30):

At first glance, this looks like it might be the sort of thing I need

Johannes Hölzl (Apr 10 2018 at 09:31):

there are still many things are missing. I never continued to work on it, I think with all the subtypes and quotient types we have now it may worth a try

Kevin Buzzard (Apr 10 2018 at 09:31):

Here is a toy example of the kind of thing I might need

Kevin Buzzard (Apr 10 2018 at 09:33):

It is ridiculous to continually write R[1/f]R[1/f], I may as well write X f where f : R (RR is a ring but may as well be a type) and X : Π (f : R), Type

Kevin Buzzard (Apr 10 2018 at 09:34):

There is an equivalence relation on R, and if f and g are equivalent then, in my language, X f and X g are canonically isomorphic.

Kevin Buzzard (Apr 10 2018 at 09:35):

This means in practice that if f and g are equivalent then there is a map Y f g : X f -> X g

Kevin Buzzard (Apr 10 2018 at 09:35):

satisfying Y f f = id

Kevin Buzzard (Apr 10 2018 at 09:36):

and Y f g composed with Y g h equals Y f h

Kevin Buzzard (Apr 10 2018 at 09:37):

Now I might have maps X f₁ -> X f₂ and X f₂ -> X f₃ and a theorem saying that the image of the first map is precisely the preimage of 0 of the second map

Kevin Buzzard (Apr 10 2018 at 09:37):

(X f is a ring and Y f g sends 0 to 0)

Kevin Buzzard (Apr 10 2018 at 09:38):

and now I want to know _immediately_ that if f_1 is equivalent to g_1 etc

Kevin Buzzard (Apr 10 2018 at 09:38):

then the image of X g_1 -> X g_2 equals the preimage of 0 in X g_2 -> X g_3

Kevin Buzzard (Apr 10 2018 at 09:39):

The proof in Lean is a diagram chase

Kevin Buzzard (Apr 10 2018 at 09:39):

but I have a gazillion of such diagram chases

Kevin Buzzard (Apr 10 2018 at 09:39):

I want the proof to be a tactic or something

Kevin Buzzard (Apr 10 2018 at 09:40):

I want the proof to follow from some foundational properties which I do not need to invoke explicitly.

Kevin Buzzard (Apr 10 2018 at 09:40):

That's what going on in my head as a mathematician

Kevin Buzzard (Apr 10 2018 at 09:40):

I don't want to have to invoke lemmas from the mathlib set files

Kevin Buzzard (Apr 10 2018 at 09:40):

I want to say that this is all obvious

Patrick Massot (Apr 10 2018 at 09:40):

What about using the limit ring?

Kevin Buzzard (Apr 10 2018 at 09:41):

Yes, the projective limit. I have considered this

Kevin Buzzard (Apr 10 2018 at 09:41):

But do you think that this is what mathematicians do?

Kevin Buzzard (Apr 10 2018 at 09:41):

I am not so sure

Patrick Massot (Apr 10 2018 at 09:41):

This is what they do when then get cornered

Kevin Buzzard (Apr 10 2018 at 09:41):

I have seen Lean do impressive things

Patrick Massot (Apr 10 2018 at 09:41):

But not otherwise

Kevin Buzzard (Apr 10 2018 at 09:41):

automatically

Kevin Buzzard (Apr 10 2018 at 09:42):

I have seen quite complex goals being solved by refl because I set stuff up right

Kevin Buzzard (Apr 10 2018 at 09:42):

but this will not be refl because X f is not _equal_ to X g

Kevin Buzzard (Apr 10 2018 at 09:43):

Can you see my point Patrick? If X f_i were _equal_ to X g_i then this [image = kenel] would be refl

Kevin Buzzard (Apr 10 2018 at 09:43):

and they're not equal, but they're sufficiently equal that everything that I will be doing with them would yield to some analogue of refl

Kevin Buzzard (Apr 10 2018 at 09:44):

I think that's my point. I have seen the power of rfl and I want it more generally

Kevin Buzzard (Apr 10 2018 at 09:45):

and I don't see why I can't have something like it here

Kevin Buzzard (Apr 10 2018 at 09:45):

because I must be only using some specific collection of ideas which are invariant under canonical isomorphism

Kevin Buzzard (Apr 10 2018 at 09:46):

and I would love to just be able to write down these ideas in this specific case and then just get everything for free

Patrick Massot (Apr 10 2018 at 09:47):

Of course we all want magic for free

Patrick Massot (Apr 10 2018 at 09:47):

But rfl magic is very special. It's meta-theoretic magic

Kevin Buzzard (Apr 10 2018 at 09:48):

eq.refl is just some constructor

Patrick Massot (Apr 10 2018 at 09:48):

Definitional (or judgemental) equality is not inside type theory

Scott Morrison (Apr 10 2018 at 09:49):

(I suspect Kevin wants univalence here, but having read the HoTT book doesn't seem to qualify me to speak coherent sentences about univalence in practice...)

Patrick Massot (Apr 10 2018 at 09:49):

eq.refl is something else

Patrick Massot (Apr 10 2018 at 09:50):

You could try to write a proof and then see if some tactic could help. But the mathematical way to solve this problems seems to be using the projective limit

Kevin Buzzard (Apr 10 2018 at 09:50):

It doesn't solve the problem

Patrick Massot (Apr 10 2018 at 09:50):

The fact that we don't need it in the real world is the power of sloppy maths discussion

Kevin Buzzard (Apr 10 2018 at 09:51):

does it?

Kevin Buzzard (Apr 10 2018 at 09:51):

It just moves the work I think

Kevin Buzzard (Apr 10 2018 at 09:51):

I prove that some image equals some kernel

Kevin Buzzard (Apr 10 2018 at 09:51):

wait

Kevin Buzzard (Apr 10 2018 at 09:51):

the theorem I have is that the image equals the kernel in the R[1/f]R[1/f] world

Kevin Buzzard (Apr 10 2018 at 09:52):

I then have to promote this theorem to the projective limit world

Kevin Buzzard (Apr 10 2018 at 09:52):

so I get some canonical object which depends only on the equivalence class of f and is canonically isomorphic to R[1/f]R[1/f]

Kevin Buzzard (Apr 10 2018 at 09:53):

X f

Kevin Buzzard (Apr 10 2018 at 09:53):

and now I still have to prove that the image equals the kernel in the projective limit world

Kevin Buzzard (Apr 10 2018 at 09:54):

the only difference being that before X g depended on g, known to be in the same equivalence class of f, whereas now I have some new object X-univ [[f]] which depends only on the equivalence class of f

Patrick Massot (Apr 10 2018 at 09:54):

You need to do the full proof in the limit world

Patrick Massot (Apr 10 2018 at 09:54):

I guess

Kevin Buzzard (Apr 10 2018 at 09:54):

that can't happen

Kevin Buzzard (Apr 10 2018 at 09:55):

the proof only works

Kevin Buzzard (Apr 10 2018 at 09:55):

in the world where I have one f

Kevin Buzzard (Apr 10 2018 at 09:55):

because the proof depends on f

Kevin Buzzard (Apr 10 2018 at 09:55):

The maps don't

Kevin Buzzard (Apr 10 2018 at 09:55):

but the proof does

Kevin Buzzard (Apr 10 2018 at 09:55):

the proof of exactness

Patrick Massot (Apr 10 2018 at 09:55):

What are you proving exactly?

Kevin Buzzard (Apr 10 2018 at 09:55):

I want to go from this:

Kevin Buzzard (Apr 10 2018 at 09:56):

https://stacks.math.columbia.edu/tag/00EJ

Kevin Buzzard (Apr 10 2018 at 09:56):

to the statement that the sheaf axiom holds for finite covers of Spec(R) by basic open sets of the form D(f_i)

Kevin Buzzard (Apr 10 2018 at 09:57):

and the proof is "those two statements say the same thing"

Kevin Buzzard (Apr 10 2018 at 09:57):

just like Chris' lemma the other day which he found hard to prove, which was that sum from 1 to n of f(i) equalled sum from 1 to n of f(i) formalised in a different way

Kevin Buzzard (Apr 10 2018 at 09:58):

But the problem is that if UU is an open set which equals D(f)D(f) for some ff

Kevin Buzzard (Apr 10 2018 at 09:58):

then it is almost certainly equal to D(g)D(g) for lots of other gg

Kevin Buzzard (Apr 10 2018 at 09:59):

and I am not allowed to define the global sections on D(f)D(f) to be R[1/f]R[1/f]

Kevin Buzzard (Apr 10 2018 at 09:59):

because this involves choosing ff.

Kevin Buzzard (Apr 10 2018 at 10:00):

So like you say I can do some projective limit construction over all gg with D(f)=D(g)D(f)=D(g)

Kevin Buzzard (Apr 10 2018 at 10:00):

[the equivalence relation on RR is that f and g are equivalent iff D(f)=D(g)D(f)=D(g)]

Kevin Buzzard (Apr 10 2018 at 10:01):

or I could also do some construction involving inverting all gg which are non-vanishing on UU

Kevin Buzzard (Apr 10 2018 at 10:01):

and either way I get a new ring which is not definitionally equal to R[1/f]R[1/f]

Kevin Buzzard (Apr 10 2018 at 10:01):

but which is uniquely isomorphic to it as RR-algebra

Kevin Buzzard (Apr 10 2018 at 10:01):

and now I have to push the diagram chase over

Kevin Buzzard (Apr 10 2018 at 10:01):

It's just a little thing

Kevin Buzzard (Apr 10 2018 at 10:02):

but I feel like it's some variant of rfl

Kevin Buzzard (Apr 10 2018 at 10:02):

"you're only chasing around images and kernels of maps, so everything is fine if you replace your rings with isomorphic rings"

Patrick Massot (Apr 10 2018 at 10:49):

"you're only chasing around images and kernels of maps, so everything is fine if you replace your rings with isomorphic rings"

I though about this, and I think you are cheating a bit here. You still need the maps in your exact sequence to commute with your canonical isomorphisms. I think you can only hope for automation if you have a really fancy categorical way of defining both your canonical isomorphisms and the maps entering the exact sequence. Otherwise you can still define standard open subsets as equivalence classes of ff, the associated system of rings R[1/f]R[1/f], and the sheaf on such an open subsets as the limit of this system. And you can have many lemmas about diagrams of rings (or modules), their limits and how to build exact sequences of limits out of exact sequences and commutation relations. Actually this should probably all be provided by @Scott Morrison's category theory lib.

Scott Morrison (Apr 10 2018 at 10:59):

(getting there...)

Kevin Buzzard (Apr 10 2018 at 11:02):

My maps are also "canonical" in the sense that they are "built from" the unique R-algebra maps between these rings.

Kevin Buzzard (Apr 10 2018 at 11:04):

By which I mean the map R[1/f]R[1/fg]R[1/f]\to R[1/fg] is the unique RR-algebra map, and then everything is put together just from such maps in such a way as to not break anything.

Kevin Buzzard (Apr 10 2018 at 11:05):

Maybe this is going towards telling me exactly which lemmas I need to prove.

Kevin Buzzard (Apr 27 2018 at 07:52):

Two weeks later and I have all the infrastructure I need to prove that all my diagrams commute painlessly

Kevin Buzzard (Apr 27 2018 at 07:53):

In particular, Patrick said "I though about this, and I think you are cheating a bit here. You still need the maps in your exact sequence to commute with your canonical isomorphisms.", and he's right, and I now have this

Kevin Buzzard (Apr 27 2018 at 07:54):

so now I start the painful task of taking some exact sequence, replacing every term with an isomorphic term, and then proving that it's still exact

Kevin Buzzard (Apr 27 2018 at 07:54):

not painful because it's hard, but painful because it's obvious :-)


Last updated: Dec 20 2023 at 11:08 UTC