promoting equiv

Stream: maths

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and moreover there is a unique isomorphism between $R[1/f]$ and $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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

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]

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

[Kevin Buzzard]

which I can produce

[Kevin Buzzard]

with an inverse

[Kevin Buzzard]

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

[Kevin Buzzard]

and just push through all the theorems I want

[Kevin Buzzard]

from theorems about $R[1/f]$

[Gabriel Ebner]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

however

[Kevin Buzzard]

because I am doing maths and not type theory

[Kevin Buzzard]

there is some sort of implicit understanding

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

I have planned the proof

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I know how to prove all of these things

[Kevin Buzzard]

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

[Kevin Buzzard]

because I have just been reading about UniMath

[Kevin Buzzard]

and I see that equality is not a Prop there

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and when the explosion of obligations occurs

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and then to ask again.

[Andrew Ashworth]

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]

transfer is not only for integers

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

satisfying Y f f = id

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The proof in Lean is a diagram chase

[Kevin Buzzard]

but I have a gazillion of such diagram chases

[Kevin Buzzard]

I want the proof to be a tactic or something

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I want to say that this is all obvious

[Patrick Massot]

What about using the limit ring?

[Kevin Buzzard]

Yes, the projective limit. I have considered this

[Kevin Buzzard]

But do you think that this is what mathematicians do?

[Kevin Buzzard]

I am not so sure

[Patrick Massot]

This is what they do when then get cornered

[Kevin Buzzard]

I have seen Lean do impressive things

[Patrick Massot]

But not otherwise

[Kevin Buzzard]

automatically

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Of course we all want magic for free

[Patrick Massot]

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

[Kevin Buzzard]

eq.refl is just some constructor

[Patrick Massot]

Definitional (or judgemental) equality is not inside type theory

[Scott Morrison]

(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]

eq.refl is something else

[Patrick Massot]

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]

It doesn't solve the problem

[Patrick Massot]

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

[Kevin Buzzard]

does it?

[Kevin Buzzard]

It just moves the work I think

[Kevin Buzzard]

I prove that some image equals some kernel

[Kevin Buzzard]

wait

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

X f

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

You need to do the full proof in the limit world

[Patrick Massot]

I guess

[Kevin Buzzard]

that can't happen

[Kevin Buzzard]

the proof only works

[Kevin Buzzard]

in the world where I have one f

[Kevin Buzzard]

because the proof depends on f

[Kevin Buzzard]

The maps don't

[Kevin Buzzard]

but the proof does

[Kevin Buzzard]

the proof of exactness

[Patrick Massot]

What are you proving exactly?

[Kevin Buzzard]

I want to go from this:

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

because this involves choosing $f$.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

or I could also do some construction involving inverting all $g$ which are non-vanishing on $U$

[Kevin Buzzard]

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

[Kevin Buzzard]

but which is uniquely isomorphic to it as $R$-algebra

[Kevin Buzzard]

and now I have to push the diagram chase over

[Kevin Buzzard]

It's just a little thing

[Kevin Buzzard]

but I feel like it's some variant of rfl

[Kevin Buzzard]

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

[Patrick Massot]

"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 $f$, the associated system of rings $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]

(getting there...)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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