Zulip Chat Archive

Stream: maths

Topic: promoting equiv


view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:13):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:14):

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

view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:17):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:18):

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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:20):

which I can produce

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:20):

with an inverse

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:21):

and just push through all the theorems I want

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:21):

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

view this post on Zulip Gabriel Ebner (Apr 10 2018 at 09:21):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:21):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:21):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:22):

however

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:22):

because I am doing maths and not type theory

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:22):

there is some sort of implicit understanding

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:24):

I have planned the proof

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:26):

I know how to prove all of these things

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:26):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:26):

because I have just been reading about UniMath

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:26):

and I see that equality is not a Prop there

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:27):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:27):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:28):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:28):

and when the explosion of obligations occurs

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:28):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:28):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:28):

and then to ask again.

view this post on Zulip 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)

view this post on Zulip Johannes Hölzl (Apr 10 2018 at 09:29):

transfer is not only for integers

view this post on Zulip Andrew Ashworth (Apr 10 2018 at 09:29):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:30):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:31):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:35):

satisfying Y f f = id

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:36):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:39):

The proof in Lean is a diagram chase

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:39):

but I have a gazillion of such diagram chases

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:39):

I want the proof to be a tactic or something

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:40):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:40):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:40):

I want to say that this is all obvious

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:40):

What about using the limit ring?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:41):

Yes, the projective limit. I have considered this

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:41):

But do you think that this is what mathematicians do?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:41):

I am not so sure

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:41):

This is what they do when then get cornered

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:41):

I have seen Lean do impressive things

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:41):

But not otherwise

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:41):

automatically

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:42):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:42):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:45):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:47):

Of course we all want magic for free

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:47):

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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:48):

eq.refl is just some constructor

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:48):

Definitional (or judgemental) equality is not inside type theory

view this post on Zulip 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...)

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:49):

eq.refl is something else

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:50):

It doesn't solve the problem

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:51):

does it?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:51):

It just moves the work I think

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:51):

I prove that some image equals some kernel

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:51):

wait

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:52):

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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:53):

X f

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:54):

You need to do the full proof in the limit world

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:54):

I guess

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:54):

that can't happen

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

the proof only works

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

in the world where I have one f

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

because the proof depends on f

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

The maps don't

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

but the proof does

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

the proof of exactness

view this post on Zulip Patrick Massot (Apr 10 2018 at 09:55):

What are you proving exactly?

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:55):

I want to go from this:

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:56):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:58):

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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 09:59):

because this involves choosing ff.

view this post on Zulip 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)

view this post on Zulip 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)]

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:01):

but which is uniquely isomorphic to it as RR-algebra

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:01):

and now I have to push the diagram chase over

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:01):

It's just a little thing

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 10:02):

but I feel like it's some variant of rfl

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 10 2018 at 10:59):

(getting there...)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 10 2018 at 11:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:54):

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


Last updated: May 12 2021 at 06:14 UTC