Zulip Chat Archive

Stream: maths

Topic: valuations


view this post on Zulip Kevin Buzzard (May 25 2018 at 22:47):

Both the Fibonacci Squares project and the Adic Space project need valuations on rings -- one in rather more generality than the other. But let's start at the beginning. Does Lean have p-adic valuations on Z? In other words, is the function vp()v_p(\cdot) on the non-zero integers (or even rationals) sending pnNp^nN (with NN coprime to the prime pp) to nn? The key theorems are vp(ab)=vp(a)+vp(b)v_p(ab)=v_p(a)+v_p(b) and vp(a+b)min{vp(a),vp(b)}v_p(a+b)\geq\min\{v_p(a),v_p(b)\} (where vp(0)v_p(0) is usually taken to be ++\infty).

view this post on Zulip Kevin Buzzard (May 25 2018 at 22:48):

Perfectoid space valuations would take values in a certain kind of totally ordered monoid

view this post on Zulip Kevin Buzzard (May 25 2018 at 22:49):

(and are of a slightly different nature -- they are really norms not valuations, so the total function Mpvp(M)M \mapsto p^{-v_p(M)} with target the non-negative reals would be an example).

view this post on Zulip Reid Barton (May 25 2018 at 23:20):

I have approximately this lying around somewhere

view this post on Zulip Reid Barton (May 25 2018 at 23:27):

https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

view this post on Zulip Reid Barton (May 25 2018 at 23:28):

I guess ord_add is missing, but it should be easy to prove from the other stuff

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:37):

line 91 should now be

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:37):

... = p * (p^r * k) : by unfold pow nat.pow; ac_refl,

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:37):

[adding pow, probably because of some relatively recent change with ^]

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:40):

Thanks so much! This is exactly what I wanted!

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:40):

What a great little community we are getting here!

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:41):

I'm just going to dump it in a subdirectory in my project called Reid_Barton. Is that OK?

view this post on Zulip Kevin Buzzard (May 25 2018 at 23:42):

Is there a better way of doing things?

view this post on Zulip Reid Barton (May 25 2018 at 23:53):

Sure, no problem.
The better way is probably to try to PR things into mathlib, but that's more effort.

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:02):

example : has_le (ℕ+) := by apply_instance -- fails

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:03):

Noticed this along the way. You've not proved the valuation of a + b but you've proved everything but. I've never worked with \N+ before.

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:04):

Is there a good reason for not having le on \N+? I am making a little collection of random short mathlib proposals. I understand how mathlib works much better after my schemes exercise.

view this post on Zulip Reid Barton (May 26 2018 at 00:09):

I doubt there is any good reason. pnat isn't used that much, it seems. I remember finding it a little more annoying to use than I would have liked

view this post on Zulip Reid Barton (May 26 2018 at 00:09):

Particularly as there are coercions in both directions between nat and pnat

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:10):

Is ord_pow broken?

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:10):

Or did I break it myself?

view this post on Zulip Reid Barton (May 26 2018 at 00:11):

It's quite possibly broken because it is about 2.5 months old

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:11):

do computer scientists really need a _coercion_ from nat to pnat?

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:11):

I just can't even guess what it would be

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:11):

"any one of a couple of random examples"

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:14):

lemma ord_pow {k : ℕ} {a : ℕ+} : ord p (a^k) = k * ord p a := ord_ppow

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:14):

:-)

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:14):

I think some coercion magic happened?

view this post on Zulip Kevin Buzzard (May 26 2018 at 00:58):

Is there a type Nat union {infinity}? I mean, it's option Nat but I want the obvious le, add and min functions (and don't want to write them if they're already there). The reason I ask is to extend p-adic valuation to zero, and I think I do have to add infinity, because the standard CS answer of just defining it to be 37 or whatever and ploughing on regardless doesn't seem to work here, because then things like min are wrong.

view this post on Zulip Kenny Lau (May 26 2018 at 00:59):

it's called the ordinal omega+1 :D

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:00):

:D

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:01):

Things which I want to be there, are more and more often beginning to be there :D

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:03):

Anyone fancy univariate polynomials over a field (division algorithm, degree function with the usual problems at 0, gcd, unique factorization?)

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:04):

I'm seeing that pop up more and more. Lean has multivariate polynomials but I think these deserve to be a special class rather than constantly carrying around the type "unit" for your list of variables.

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:05):

@Nicholas Scheel do you want to try this? I'm going to show your work on Z[alpha] to the British Maths Olympiad squad tomorrow! See what they make of it.

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:07):

Some stuff is there by a student of Johannes in his mason-stother directory but I don't think it's all there. And didn't someone do some Euclidean Algorithm stuff recently? Some student of Scott maybe? That might help I guess.

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:07):

We need univariate polynomials for the Fibonacci project, as you know.

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:07):

Or maybe Kenny or Chris will do it now their exams are over.

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:08):

A fair amount of this stuff should be tidied up and put in mathlib, so it's all in one place.

view this post on Zulip Andrew Ashworth (May 26 2018 at 01:12):

hah, won't you soon have your own army of undergraduates working for you over the summer?

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:13):

Over 20 undergrads now

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:13):

They start 2nd July

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:13):

It's going to be a crazy summer!

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:14):

2 months!

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:39):

I am so rubbish at coe

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:39):

@[simp] lemma pgcd_coe_something (a b : ) : pgcd a b = gcd a b := begin
unfold pgcd,
--rw pnat.coe_nat_coe a, -- I am so rubbish at coe
sorry
end

view this post on Zulip Kevin Buzzard (May 26 2018 at 01:39):

This is Reid's pgcd from his gist from earlier

view this post on Zulip Kevin Buzzard (May 26 2018 at 02:01):

https://gist.github.com/rwbarton/599327954b01b2e840894189981172ea

view this post on Zulip Mario Carneiro (May 26 2018 at 02:06):

Is there a type Nat union {infinity}?

As of this morning, there is a with_top A structure that adds an infinity element to any order. So with_top nat is just what you want.

view this post on Zulip Kenny Lau (May 26 2018 at 02:14):

wow what a coincidence lol

view this post on Zulip Mario Carneiro (May 26 2018 at 02:28):

do computer scientists really need a _coercion_ from nat to pnat?

Hm, my original concern was that if you wanted to write 5 as a pnat you would need to write <5, dec_trivial> which is obviously cumbersome. But actually since pnat has has_one and has_add that's actually enough for bit0 and bit1 to work, meaning that (5 : pnat) works fine (being defined as bit1 (bit0 1) where the 1 and addition are interpreted in pnat). So maybe this isn't needed. I'll see what breaks if I remove it, I agree it's not great to have a non-identity looking coercion

view this post on Zulip Mario Carneiro (May 26 2018 at 02:30):

I was thinking of using pnat for the domain of Z/nZ btw, which will give it a better algebraic theory than fin n

view this post on Zulip Kevin Buzzard (May 26 2018 at 02:34):

Is there a type Nat union {infinity}?

As of this morning, there is a with_top A structure that adds an infinity element to any order. So with_top nat is just what you want.

Mario -- did you see Remark 1.5 of www2.math.uni-paderborn.de/fileadmin/Mathematik/People/wedhorn/Lehre/AdicSpaces.pdf (page 4)? There is a fundamental construction in adic spaces -- adding a "bottom" element zero to a a totally ordered group (e.g the group of positive reals) and creating a totally ordered monoid. Is this sort of thing easy to do now?

view this post on Zulip Nicholas Scheel (May 26 2018 at 02:35):

@Kevin Buzzard I could spend an hour or two on it ... should I use multivariate polynomials, should I use finsupp, or just do a direct list encoding?

view this post on Zulip Mario Carneiro (May 26 2018 at 02:39):

Actually your comment got me thinking about this. There is a related construction, let's say with_zero A, which adds a unit to any additive semigroup; and if the zero and bottom coincide then you get a composite structure which works well on some kinds of ordered groups, I would imagine. Similarly you can make sense of addition with infinity, and that structure coheres with the order of with_top, so that you can add an infinity element to an ordered additive semigroup.

view this post on Zulip Mario Carneiro (May 26 2018 at 02:40):

This could be used to factor ennreal into with_top nnreal

view this post on Zulip Kenny Lau (May 26 2018 at 02:41):

rip ennreal 2017-2018

view this post on Zulip Kenny Lau (May 26 2018 at 02:42):

born Aug 30, 2017

view this post on Zulip Mario Carneiro (May 26 2018 at 02:42):

It probably wouldn't go away as a definition, it has enough properties on its own that make it worthy of study, but it would simplify and generalize some theorems

view this post on Zulip Mario Carneiro (May 26 2018 at 02:43):

But to answer your question, currently with_bot and with_top only deal with the order structure, they don't have any monoid stuff

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:00):

do computer scientists really need a _coercion_ from nat to pnat?

Hm, my original concern was that if you wanted to write 5 as a pnat you would need to write <5, dec_trivial> which is obviously cumbersome. But actually since pnat has has_one and has_add that's actually enough for bit0 and bit1 to work, meaning that (5 : pnat) works fine (being defined as bit1 (bit0 1) where the 1 and addition are interpreted in pnat). So maybe this isn't needed. I'll see what breaks if I remove it, I agree it's not great to have a non-identity looking coercion

Is it possible to keep the coercion but demand that the type class resolution system produces a proof of positivity before it is applied? I think that this would very much mirror the way a mathematician thought about the issue.

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:00):

You might find that if proofs of positivity are carried around

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:01):

with instances like "a > 0 and b > 0 implies a + b > 0"

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:01):

then the coercions work fine.

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:01):

With the current system you just occasionally see these \u \u x things

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:02):

and it's only at the point where you go to cancel them and they won't cancel that you realise you've made a mathematical slip

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:03):

Can we make the coercion part of type class resolution better?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:10):

this isn't how coercions work

view this post on Zulip Mario Carneiro (May 27 2018 at 13:10):

they are functions A -> B, nothing else is allowed in there

view this post on Zulip Mario Carneiro (May 27 2018 at 13:10):

in particular, coercions cannot be partial

view this post on Zulip Mario Carneiro (May 27 2018 at 13:10):

except the coercion Prop -> bool which is magical

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:31):

CS 101 question alert :-/

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:32):

What's the theorem \<a,h\>.val = a called for subtypes?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:32):

rfl

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:32):

I was trying not to use rfl

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:32):

I was looking at the proof that \u \u a =a

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

I just figured that I had a bunch of stuff about coercions that I needed to understand better before I said too much more about this

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

and then I ended up going down a rabbit hole watching the type class resolution system unfold :-/

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

Actually I don't understand.

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

How do I rewrite \u \u a as a?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

Wait

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

I was asking for the name of the theorem

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:33):

not the proof

view this post on Zulip Mario Carneiro (May 27 2018 at 13:34):

you haven't given me enough info to answer the question

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:34):

I'll formulate something precise.

view this post on Zulip Mario Carneiro (May 27 2018 at 13:34):

lots of theorems look like \u \u a = a

view this post on Zulip Mario Carneiro (May 27 2018 at 13:35):

I need to know what is the type of a, and the type of \u a

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:35):

[pause whilst we discover if Kevin is talking nonsense]

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:41):

variables (α : Type) (p : α  Prop)
theorem what_am_i_called (a : α) (h : p a) : (subtype.mk a h).val = a := rfl

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:41):

The question.

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:42):

because I want to use you in a rewrite

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:42):

so I need to know your name

view this post on Zulip Mario Carneiro (May 27 2018 at 13:42):

the theorem doesn't have a name, it is done automatically by dsimp

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:43):

And there's you guys saying our naming conventions are bad

view this post on Zulip Mario Carneiro (May 27 2018 at 13:43):

same as how beta reduction isn't a named theorem

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:43):

dsimp is what?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:43):

I used it a couple of times recently

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:43):

Kenny told me "just use dsimp" and I'm like "ooh my goal has gone from 1 page to 5 lines"

view this post on Zulip Mario Carneiro (May 27 2018 at 13:44):

it's simp for definitional rewrites

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:44):

which way does it go?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:44):

What does it actually do?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:44):

If it sees my subtype.mk.val stuff it just says "ooh I'll remove that"

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:44):

but does it ever add it?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:44):

it does exactly the same sort of thing as simp

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

oh great :-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

Another black box :-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

I see

view this post on Zulip Mario Carneiro (May 27 2018 at 13:45):

it cancels projections applied to structure mk

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

What else does it do?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:45):

this is the structure iota rule

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

What's a complete list of what it does?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

Would I be able to understand the source code?

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:45):

Kenny says that Lean does not do magic but this is still magic to me

view this post on Zulip Mario Carneiro (May 27 2018 at 13:46):

dsimp has a config too

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:46):

53 extra options?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:46):

that has a fairly complete list of the kinds of automatic reductions it does, beta, eta, zeta, iota etc

view this post on Zulip Mario Carneiro (May 27 2018 at 13:47):

and it also uses @[simp] lemmas that are also rfl lemmas

view this post on Zulip Mario Carneiro (May 27 2018 at 13:47):

as well as definition unfolding when you give it to the bracket list or use !

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:47):

I would be really interested in watching a video or seeing an article about what dsimp and/or simp do. If I understood what they were doing I wouldn't still just be hopefully typing simp every now and then just to see if I can make the goal go away

view this post on Zulip Mario Carneiro (May 27 2018 at 13:48):

Haven't we had this conversation before?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:48):

I'm pretty sure you wrote that article

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:48):

I feel like there's still a whole bunch of things I don't fully understand with all this business

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:48):

I'll read my own docs and see if this enlightens me

view this post on Zulip Andrew Ashworth (May 27 2018 at 13:50):

The textbook "term rewriting and all that" is pretty good on this subject, if your uni library has it

view this post on Zulip Nicholas Scheel (May 27 2018 at 13:52):

simplification using definition equalities, I believe

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:54):

So my real question was "how do I do a definitional rewrite in tactic mode", and the answer is "don't use rw, use show"

view this post on Zulip Mario Carneiro (May 27 2018 at 13:55):

change with is literally definitional rw

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:55):

The textbook "term rewriting and all that" is pretty good on this subject, if your uni library has it

Thanks Andrew. My university can get any book for me.

view this post on Zulip Mario Carneiro (May 27 2018 at 13:56):

but dsimp is nice for just cleaning up some common patterns

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:56):

Equality is asymmetric for you people, isn't it

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:57):

This is only just dawning on me

view this post on Zulip Mario Carneiro (May 27 2018 at 13:57):

yes, with term rewrites direction really matters

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:57):

If you write a = b, and if one side was more complicated than the other

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:57):

you would put the more complicated side first

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:57):

Is this just some general principle?

view this post on Zulip Mario Carneiro (May 27 2018 at 13:57):

yeah, simp simplifies

view this post on Zulip Mario Carneiro (May 27 2018 at 13:58):

it's not called complexify

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:58):

I had not realised that = was asymmetric

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:58):

in any way whatsoever

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:58):

I have a different definition of = to you

view this post on Zulip Mario Carneiro (May 27 2018 at 13:58):

= itself is symmetric

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:58):

symmetric in some theorem sense

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:59):

but you have to decide which goes first

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:59):

and we don't care

view this post on Zulip Mario Carneiro (May 27 2018 at 13:59):

but simp and dsimp takes the list of simp lemmas and use them as a rewrite graph

view this post on Zulip Mario Carneiro (May 27 2018 at 13:59):

and this is directed

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:59):

Right, I've just been learning this from my own notes

view this post on Zulip Kevin Buzzard (May 27 2018 at 13:59):

Aah!

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:00):

I've just realised what my question actually is.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:00):

My question is this: "I never ever tag anything with @[simp]. I make loads of structures. Can you give me some basic advice over which trivial lemmas I should be (a) proving and (b) tagging with simp?"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:01):

Unfortunately, the answer is "depends on the structure"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:01):

some axioms of a structure should be simp lemmas

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:01):

subtype

view this post on Zulip Mario Carneiro (May 27 2018 at 14:01):

like zero_add

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:01):

A type and a proof

view this post on Zulip Mario Carneiro (May 27 2018 at 14:02):

I don't think subtype has any simp lemmas

view this post on Zulip Mario Carneiro (May 27 2018 at 14:02):

which is to say, there is nothing that sticks out as necessary

view this post on Zulip Mario Carneiro (May 27 2018 at 14:02):

oh, <a, h1> = <b, h2> <-> a = b should be a simp lemma

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:03):

What about presheaf of types on a topological space?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:03):

I made that structure once

view this post on Zulip Mario Carneiro (May 27 2018 at 14:03):

but actually I think simp might do that automatically anyway

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:03):

I'll find you a link

view this post on Zulip Mario Carneiro (May 27 2018 at 14:04):

simp will already do a few things by default on all structures, which more or less covers all the general recommendations

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:05):

https://github.com/kbuzzard/lean-stacks-project/blob/6617de7dd5f11af46f0c7e0d2223ee065d71b9f3/src/tag006E.lean#L4

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:05):

I am proud to say that I did actually write a simp lemma for that

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:05):

My simp lemma says "crap, I made a poor design decision when designing that structure, but I can't be bothered to change it now"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:05):

that's just what I would have recommended

view this post on Zulip Mario Carneiro (May 27 2018 at 14:06):

except possibly for the dependent args

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:06):

You would recommend the change in the structure?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:06):

that doesn't matter so much

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:06):

Oh!

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:06):

You don't care which definition I use if they're all equivalent?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:07):

I was going to bite the bullet one day and edit the definition of that structure. You're saying that's a crazy idea?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:07):

it affects the proof goals when defining structures with { stuff := ... }

view this post on Zulip Mario Carneiro (May 27 2018 at 14:07):

so it depends on how you usually prove such goals

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:07):

I was going to change "f = g circ h" with "forall x, g (h x) = f x"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:08):

if the first thing you do is always funext, then that's a hint

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:08):

Note the equality "f = g circ h"

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:08):

the more complicated side on the right

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:08):

is that also unwise?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:08):

actually here I recommend that ordering

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:08):

The thing about funext was that there were a few times when the fact that it was comp was really useful, it made some proofs really nice and short

view this post on Zulip Mario Carneiro (May 27 2018 at 14:08):

because the argument to f is getting simpler

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:08):

boggle

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:09):

I don't understand

view this post on Zulip Mario Carneiro (May 27 2018 at 14:09):

think of it as f (comp a b) = f a o f b

view this post on Zulip Mario Carneiro (May 27 2018 at 14:10):

here simp will want to go left to right to make the argument to f as simple as possible

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:10):

It's res U W x = res V W (res U V x)

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:10):

that's what it is really

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:10):

You still want it that way round?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:11):

that's not a good simp lemma

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:11):

"restriction of a function on U down to V and then down to W equals restriction directly down to W"

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:11):

Either way round?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:12):

Okay, I guess in this case since it's a proof arg it shouldn't be a metric of simplicity

view this post on Zulip Mario Carneiro (May 27 2018 at 14:12):

so in that case you want res V W (res U V x) = res U W x

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:12):

This is the thing I don't understand. It takes two functions res U V and res W V and it returns one function. It's made it simpler. I don't understand what should be a simp lemma.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:13):

Aah so you do want to switch the order?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:13):

And then make a simp lemma?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:14):

Okay, I guess in this case since it's a proof arg it shouldn't be a metric of simplicity

I don't understand that either :-/

view this post on Zulip Mario Carneiro (May 27 2018 at 14:15):

You have this extra argument that has a big term in it

view this post on Zulip Mario Carneiro (May 27 2018 at 14:15):

I've mentioned that proof args are bad for rewrites before

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:16):

Why?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:16):

proof args are fundamental statements about the situation

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:17):

Are you saying that associativity of addition should not be a simp lemma?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:18):

associativity of addition is both a simp lemma and seems to have the more complicated side on the right.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:19):

None of it adds up to me. I am still nowhere near understanding what should be a simp lemma.

view this post on Zulip Mario Carneiro (May 27 2018 at 14:19):

assoc is a special case

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:19):

boggle

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:19):

I'll add it to the docs

view this post on Zulip Mario Carneiro (May 27 2018 at 14:19):

simp has special handling for comm/assoc operations

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:20):

which uses a convention which goes against the "simpler argument on the right" convention?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:20):

it would not normally be a good simp lemma, because it doesn't simplify the term

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:20):

mul_one is a simp lemma and it's a proof arg, if I've understood the last term correctly

view this post on Zulip Mario Carneiro (May 27 2018 at 14:21):

But simp will notice if you give it a lemma that looks like associativity and apply special algorithms to do smart things with that

view this post on Zulip Mario Carneiro (May 27 2018 at 14:21):

None of those have proof args

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:21):

oh

view this post on Zulip Mario Carneiro (May 27 2018 at 14:21):

I'm talking about proofs as arguments to functions you want to rewrite

view this post on Zulip Mario Carneiro (May 27 2018 at 14:22):

so in this case that would be like proof arguments to mul or one

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:22):

I thought you were talking about proofs as arguments used to create a structure

view this post on Zulip Mario Carneiro (May 27 2018 at 14:22):

in your case I'm talking about res which has three proof args

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:23):

Would your opinion change if made them all work magically using type class resolution?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:23):

yes

view this post on Zulip Mario Carneiro (May 27 2018 at 14:24):

that's an interesting idea, I'd have to see how messy the arguments can get

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:24):

The reason I didn't use type class resolution for those things was that when I wrote that code I had no idea how typeclass resolution system worked

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:25):

so I just over-rode it and would always pass the proofs manually

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:25):

and then later on in the project I was forced to work with rings and ring homs

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:25):

so I was forced to learn the system

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:25):

and we had that long thread with me moaning and learning about letI

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:32):

Ok so coercions.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:32):

theorem eew (Y : ℕ+) : ((Y : ℕ) : ℕ+) = Y := rfl -- fails

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:32):

That's not good, right?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:32):

Should that be a simp lemma?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:33):

ℕ+ is one of my favourite sets in ZFC

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:34):

Why is it so hard to work with here?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:34):

Just because it's not a stupid semiring

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:34):

maybe it's a demisemiring

view this post on Zulip Mario Carneiro (May 27 2018 at 14:35):

that is a simp lemma, I think

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:35):

Aah here's a question.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:35):

Let's say we ripped out the definition of pnat

view this post on Zulip Mario Carneiro (May 27 2018 at 14:35):

coe_nat_coe

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

and replaced it with a straight inductive structure with one and succ

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

Would that make any difference to anything

view this post on Zulip Mario Carneiro (May 27 2018 at 14:36):

not really

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

or you just write the new interface

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

and that's it

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

No issue with compile time or running time

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:36):

or simp not working as well

view this post on Zulip Mario Carneiro (May 27 2018 at 14:36):

anything not using the interface would be affected, of course

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:37):

Aah

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:37):

anything accessing the innards of the structure

view this post on Zulip Mario Carneiro (May 27 2018 at 14:37):

i.e. if someone creates a pnat by writing <2, dec_trivial>

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:37):

instead of (2 : pnat)

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:37):

then they should be punished?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:37):

How does that work?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:38):

"You only use official constructors"

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:38):

"not inbuilt stuff"

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:38):

Oh wait -- surely anyone writing a proof in term mode with pnat will have constructors like that everywhere

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:39):

because it's a super-cool way of being fancy in fancy term mode

view this post on Zulip Kenny Lau (May 27 2018 at 14:39):

right

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:39):

eew

view this post on Zulip Mario Carneiro (May 27 2018 at 14:39):

well, the thing is that I don't want to avoid structure constructors, because they are very nice

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:39):

So there is a question left

view this post on Zulip Mario Carneiro (May 27 2018 at 14:39):

you can't replicate that functionality with an interface

view this post on Zulip Mario Carneiro (May 27 2018 at 14:40):

unless the interface is to pass in a specially defined structure

view this post on Zulip Mario Carneiro (May 27 2018 at 14:40):

like simp_config

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:40):

you've lost me now

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:41):

but I do see that there is a huge argument for structure constructors and this presumably has some bearing on exactly which constructors you choose and maybe even in which order?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:41):

maybe order irrelevant

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:41):

but you never know

view this post on Zulip Mario Carneiro (May 27 2018 at 14:41):

yes

view this post on Zulip Mario Carneiro (May 27 2018 at 14:41):

order is relevant for anonymous constructors

view this post on Zulip Mario Carneiro (May 27 2018 at 14:42):

Here are my currrent thoughts on presheaf fyi:

structure order_presheaf (α : Type u) [preorder α] :=
(F : α → Type u)
(res : ∀ x {y}, x ≤ y → F y → F x)
(Hid : ∀ x h a, res x h a = a)
(Hcomp : ∀ x y z h₁ h₂ (a : F z),
  res x h₁ (res y h₂ a) = res x (le_trans h₁ h₂) a)

view this post on Zulip Kenny Lau (May 27 2018 at 14:42):

what is an order_presheaf?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

Would you want presheaves in mathlib?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

oh eew

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

what just happened there

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

with the open sets

view this post on Zulip Kenny Lau (May 27 2018 at 14:43):

oh, they form a preorder under inclusion!

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

he thinks he's being clever

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:43):

but we need the etale site ;-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:44):

so he's still not general enough ;-)

view this post on Zulip Mario Carneiro (May 27 2018 at 14:44):

if you add enough axioms to the preorder you can capture exactly the open sets of some topology

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:44):

yeah, I was just remarking that at some point later on algebraic geometry needs the notion of sheaf on something more general than a topological space

view this post on Zulip Mario Carneiro (May 27 2018 at 14:44):

but this part of the definition only needs a preorder

view this post on Zulip Kenny Lau (May 27 2018 at 14:45):

yeah, I was just remarking that at some point later on algebraic geometry needs the notion of sheaf on something more general than a topological space

what do you need?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:45):

sheaf on a site

view this post on Zulip Reid Barton (May 27 2018 at 14:45):

[category \a]

view this post on Zulip Kenny Lau (May 27 2018 at 14:45):

i.e. there may be more than one morphisms?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:45):

if you want a category then this is just functor

view this post on Zulip Reid Barton (May 27 2018 at 14:45):

Right

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:45):

but it has to satisfy the sheaf axiom

view this post on Zulip Mario Carneiro (May 27 2018 at 14:45):

point me to that

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:46):

and you need more than a category to formalise that

view this post on Zulip Kenny Lau (May 27 2018 at 14:46):

@Mario Carneiro so they may have two "proofs" of x \le y and they want the two things to be unequal

view this post on Zulip Reid Barton (May 27 2018 at 14:46):

well, so far we are only talking about presheaf I thought

view this post on Zulip Mario Carneiro (May 27 2018 at 14:46):

I am actually very fine with that

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:46):

that's true but I am interested in more than presheaves here

view this post on Zulip Mario Carneiro (May 27 2018 at 14:46):

that's the remaining problem with this definition

view this post on Zulip Mario Carneiro (May 27 2018 at 14:46):

as I said, I don't like proof args

view this post on Zulip Reid Barton (May 27 2018 at 14:47):

well then great! They won't be proofs once you generalize to a category :simple_smile:

view this post on Zulip Mario Carneiro (May 27 2018 at 14:47):

but you can't easily remove them from this... what's the structure of that argument otherwise?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:47):

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

view this post on Zulip Mario Carneiro (May 27 2018 at 14:47):

I guess Hom x y?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:48):

That's a site

view this post on Zulip Reid Barton (May 27 2018 at 14:48):

Right, just a morphism in some category.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:49):

Did you see https://stacks.math.columbia.edu/tag/00VI

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:50):

Mario, I think this says "if a computer scientist tries to do this, they will have universe issues. But in all the cases that a mathematican cares about, these issues can be avoided and we can do everything in Type"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:51):

Presheaves are already rather large

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:51):

"This definition uses two universes u and v, but when we apply it I claim that we can get away with one universe"

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:51):

How do you formalise that? ;-)

view this post on Zulip Mario Carneiro (May 27 2018 at 14:52):

It looks like sites have to be small though

view this post on Zulip Mario Carneiro (May 27 2018 at 14:52):

but what's a (pre)sheaf on a site?

view this post on Zulip Mario Carneiro (May 27 2018 at 14:52):

all I see is a bunch of covering stuff

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:53):

Also relevant

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:53):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:54):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:54):

sheaf!

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:54):

Still no presheaf :-)

view this post on Zulip Johan Commelin (May 27 2018 at 14:54):

Scott is doing sites in the his category stuff

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:54):

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

view this post on Zulip Mario Carneiro (May 27 2018 at 14:54):

and what is the site corresponding to a top space?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:54):

OK so presheaf on a category, sheaf on a site

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:55):

The site corresponding to a top space is this

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:55):

The category has an object for each open set

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:55):

Homs from U to V are empty unless V sub U in which case there is one elment

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:55):

Coverings: a set of morphisms U_i -> U covers U iff the union of the image of the U_i is U

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:56):

The sheaf axiom says this.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:56):

"If U is an open set, and it is covered by opens U_i, then to give a continuous function on U is to give a continuous function f_i on each U_i such that f_i and f_j agree on U_i intersect U_j"

view this post on Zulip Reid Barton (May 27 2018 at 14:57):

You can equivalently describe the category like this. The objects are topological spaces equipped with a map to X which is an open immersion. A morphism is a continuous map which is compatible with the structural maps to X.

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:57):

They say "continuity can be checked locally"

view this post on Zulip Mario Carneiro (May 27 2018 at 14:58):

isn't that just true?

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:58):

Reid's changing of my category to an equivalent category was something which turned out to be really important

view this post on Zulip Mario Carneiro (May 27 2018 at 14:58):

like as a statement of topology

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:58):

It's precisely the statement that continuity is a local condition

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:58):

So the presheaf of continuous functions on a topological space

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:58):

is actually a sheaf!

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:58):

But the presheaf of constant functions is not a sheaf

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

because if I have two disjoint open sets

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

and define a function to be 1 on one of them but 2 on the other one

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

it's locally constant

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

but not constant

view this post on Zulip Mario Carneiro (May 27 2018 at 14:59):

ah okay, so locally constant functions is a sheaf

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

right

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

it's the sheafification of the presheaf of constant functions

view this post on Zulip Kevin Buzzard (May 27 2018 at 14:59):

sheafification is an adjoint to the forgetful functor

view this post on Zulip Mario Carneiro (May 27 2018 at 15:00):

so how much does it matter that these are poset categories?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:00):

Exactly

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:00):

it doesn't matter at all

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:00):

and in general they won't be

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:00):

is a poset category one where the hom sets have size <= 1?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:00):

yes

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:01):

so the etale site attached to a scheme does not have this property I guess

view this post on Zulip Mario Carneiro (May 27 2018 at 15:01):

maybe it would be better to do this with honest categories

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:02):

I think Scott said that quite a long time ago

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:02):

but I just wanted to get on

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:02):

Sheaves of sets on a site are a Mathematician's Topos Mario.

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:02):

This is distinct to the CS topos

view this post on Zulip Mario Carneiro (May 27 2018 at 15:03):

like in the literal sense?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:03):

You have some more general notion I think

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:03):

Topos is used to mean two different things, I believe

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:03):

I like Grothendieck topoi

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:03):

you like elmentary topoi

view this post on Zulip Mario Carneiro (May 27 2018 at 15:03):

I am not sure I would say that...

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:03):

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

view this post on Zulip Mario Carneiro (May 27 2018 at 15:04):

topoi is usually where I get off the bus

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:04):

It took me a while, in the pre-Wikipedia age, to understand that the two uses of the word were distinct

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:04):

I knew this guy as an UG who would go round saying "a topos is a category which is finitely complete, finitely cocomplete, has exponentiation and a subobject classifier"

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:04):

and I had no idea what any of those things meant

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:05):

and then years later I found some topoi I was actually interested in

view this post on Zulip Mario Carneiro (May 27 2018 at 15:05):

that's about where I am

view this post on Zulip Kenny Lau (May 27 2018 at 15:05):

as an UG :o

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:05):

and then it turned out they were a different kind of topos

view this post on Zulip Mario Carneiro (May 27 2018 at 15:05):

I learn and forget those things every year

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:06):

There was once some debate about whether Wiles/Taylor-Wiles used Grothendieck topoi in their proof of FLT

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:06):

and the answer turned out to be

view this post on Zulip Mario Carneiro (May 27 2018 at 15:06):

because that means large universes, right?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:07):

"well, mathematicians are always a bit vague about what exactly they are using, and there is no mention of set-theoretic difficulties, but Brian Conrad went away and checked every single cohomology group in the entire proof and verified that it was OK, everything happened within one universe"

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:07):

Wiles most definitely used etale cohomology in his proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:07):

and I am almost certain that he cited some papers which at some point use flat cohomology

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:08):

and they probably cite some papers which at some point mention fpqc cohomology

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:09):

so we really needed an expert who could come along and say "I know exactly which parts of the theory of etale cohomlogy and other cohomology theories he used and can verify that all the stuff he uses can be formalised in ZFC"

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:09):

before that debate died down

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:11):

Some people really care about universes. If Lean really cannot keep track of them then these people might be skeptical

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:11):

My current personal viewpoint on this is simply to accept the large cardinals. If they make maths easier and more fun to do then I'm in

view this post on Zulip Mario Carneiro (May 27 2018 at 15:11):

For the most part, if it lives in Type it can be constructed in ZFC

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:12):

Right, but any file which uses "universes u v" is open to question right?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:12):

Or even "universe u" perhaps

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:12):

if it uses Type as well

view this post on Zulip Mario Carneiro (May 27 2018 at 15:12):

no, as long as at the end you build something in Type

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:12):

Oh

view this post on Zulip Mario Carneiro (May 27 2018 at 15:12):

The part which makes this not quite true is impredicativity of Prop

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

aie

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

so you get a proof which lived in another universe

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

but you can't get a proof in your own universe

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

so you use propext

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

cunning

view this post on Zulip Mario Carneiro (May 27 2018 at 15:13):

you can construct proofs of propositions in Prop in Type, which assert existence of large cardinals

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

ha ha

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

oh I hadn't realised that

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:13):

Prop covers its tracks

view this post on Zulip Mario Carneiro (May 27 2018 at 15:13):

that's what impredicativity does for you

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:14):

But still to construct the proof you need the extra universes, right?

view this post on Zulip Kenny Lau (May 27 2018 at 15:14):

is @Kevin Buzzard being impredicative?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:14):

you could talk about configurations in Type 63 and it wouldn't make the proof large

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:15):

I am just interested in exactly what can go wrong with regards to translating a DTT proof into ZFC

view this post on Zulip Mario Carneiro (May 27 2018 at 15:15):

right, there are large universes in the proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:15):

Because one day someone serious is going to ask me about this

view this post on Zulip Kenny Lau (May 27 2018 at 15:15):

DTT

view this post on Zulip Kenny Lau (May 27 2018 at 15:15):

?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:15):

so that wouldn't translate

view this post on Zulip Mario Carneiro (May 27 2018 at 15:15):

However, this sort of sleight of hand is very rare

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:15):

And the problem is that the proof might not be mine

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:15):

The theorem could be formulated about Type in some library

view this post on Zulip Kenny Lau (May 27 2018 at 15:15):

so they work in a system stronger than ZFC?

view this post on Zulip Kenny Lau (May 27 2018 at 15:15):

like how PA can't prove Goodstein?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:15):

and I never look at the proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:16):

Yes Kenny

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:16):

they work in ZFC + infinitely many inaccessible cardinals here

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:16):

It's infinitely less likely to be consistent than ZFC

view this post on Zulip Mario Carneiro (May 27 2018 at 15:16):

which is weaker than Tarski Grothendieck set theory btw

view this post on Zulip Kenny Lau (May 27 2018 at 15:16):

Grothendieck?!

view this post on Zulip Mario Carneiro (May 27 2018 at 15:16):

which is what most category theorists use

view this post on Zulip Mario Carneiro (May 27 2018 at 15:17):

That is equivalent to ZFC + proper class of inaccessible cardinals

view this post on Zulip Mario Carneiro (May 27 2018 at 15:17):

here we only need omega many

view this post on Zulip Kenny Lau (May 27 2018 at 15:17):

fascinating

view this post on Zulip Kenny Lau (May 27 2018 at 15:17):

logic never fails to fascinate me

view this post on Zulip Mario Carneiro (May 27 2018 at 15:17):

and for any particular proof you can say "this used 3 universes" or such

view this post on Zulip Mario Carneiro (May 27 2018 at 15:18):

it's impossible to use all the universes in a proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:18):

But I am specifically interested in the proofs which only use one universe

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:18):

For example does FLT definitely only use one universe?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:18):

well, actually you want zero universes

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:18):

Oh yes I just want Type

view this post on Zulip Mario Carneiro (May 27 2018 at 15:18):

ZFC has zero universes

view this post on Zulip Kenny Lau (May 27 2018 at 15:19):

ZFC has zero universes

zero built-in universes

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:19):

So currently the reference for "Wiles/TW proof of FLT is in ZFC" is "Email from Conrad"

view this post on Zulip Mario Carneiro (May 27 2018 at 15:19):

It's a bit tricky to work with DTT with zero universes

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:19):

Why?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:19):

Say I globally exchange all the type u for type

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:19):

how far do I get before the errors appear?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:20):

Start with core lean

view this post on Zulip Mario Carneiro (May 27 2018 at 15:20):

you have to be careful: Gamma |- A : Type is okay, but Type is not a type, in the sense Gamma |- Type : Type 1 doesn't exist

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:20):

Yeah, I promise I will never ask Type its type.

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:20):

ZFC people are used to making promises

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

and they're usually quite good at keeping them

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

This is the world I have lived in all my life

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

and you are claiming to offer me more

view this post on Zulip Mario Carneiro (May 27 2018 at 15:21):

Also you can have things like A : Type -> Type in ZFC

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

but I don't see anything of interest out there

view this post on Zulip Mario Carneiro (May 27 2018 at 15:21):

but again you can't quantify over them

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

Yes

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:21):

no

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:22):

oh wait

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:22):

I can quantify over them

view this post on Zulip Mario Carneiro (May 27 2018 at 15:22):

A : (Type -> Type) -> Type is starting to get weird

view this post on Zulip Mario Carneiro (May 27 2018 at 15:22):

A : Type -> Type is a proper class function

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:22):

I just have to write some footnote explaining about how it can all be done properly if you ask a set theorist

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:22):

because no object I consider in my paper has size greater than 2^2^2^2^aleph_0 so it's all OK

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:23):

who needs inaccessible cardinals

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:23):

I just something closed under a few iterations of the power set axiom and I'll be fine

view this post on Zulip Mario Carneiro (May 27 2018 at 15:23):

That's really hard to do formally

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:23):

There will be people out there who care about this.

view this post on Zulip Mario Carneiro (May 27 2018 at 15:23):

at least if you didn't literally do that in the proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:23):

Right, and who wants to do that?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:23):

We just wanna have fun

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:24):

I don't see any reason why ZFC should stay as the prevalent model of mathematics

view this post on Zulip Mario Carneiro (May 27 2018 at 15:24):

What you want is a way to take a proof and shrink all the things in it to ZFC things

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:24):

but without a doubt it is the prevalent model of mathematics

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:24):

I don't

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:24):

but some people might

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:24):

and I have them in mind

view this post on Zulip Mario Carneiro (May 27 2018 at 15:25):

or 2^2^2^2^aleph_0 things

view this post on Zulip Mario Carneiro (May 27 2018 at 15:25):

and it's my job to figure out how to make sense of your request

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:25):

There are theorems of the form "if you proved X using 3 universes then you could have done it in ZFC" I think

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:26):

I think someone might have told me that even though wiles certainly used AC in his proof, FLT was now known to be a theorem of ZF

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:26):

because one of these magic meta-theorem things

view this post on Zulip Mario Carneiro (May 27 2018 at 15:26):

yes, it's a pi01 statement so magic happens

view this post on Zulip Mario Carneiro (May 27 2018 at 15:44):

here's the sheaf axiom using the poset presheaf definition:

def gluing {α} [complete_lattice α] (F : order_presheaf α)
  (X : α) {ι : Type*} (Y : ι → α) (Hcov : X = ⨆ i, Y i)
  (r : F.F X) :
  {a : Π i, F.F (Y i) | ∀ (i j : ι),
    F.res (Y i ⊓ Y j) inf_le_left (a i) =
    F.res (Y i ⊓ Y j) inf_le_right (a j) } :=
⟨λ i, F.res (Y i) (by rw Hcov; apply le_supr) r,
 λ i j, by simp [F.comp]⟩

def is_order_sheaf {α : Type u} [complete_lattice α]
  (F : order_presheaf α) : Prop :=
∀ (X : α) {ι : Type u} (Y : ι → α) (Hcov : X = ⨆ i, Y i),
function.bijective (gluing F X Y Hcov)

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:47):

Did you look at what I did?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:47):

yes, it was based on your definition

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:47):

ha ha hope I didn't make a mistake :-)

view this post on Zulip Mario Carneiro (May 27 2018 at 15:48):

I think probably bijective makes more axioms than you really need here

view this post on Zulip Mario Carneiro (May 27 2018 at 15:48):

like it's probably already injective

view this post on Zulip Mario Carneiro (May 27 2018 at 15:49):

I would just state the actual condition you want, and prove it implies this function is bijective

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:51):

https://stacks.math.columbia.edu/tag/009I

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:51):

Actually I guess I just copied everything from the stacks project (and spotted a mistake or two along the way :-) )

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:52):

no, injective needs checking

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:52):

A presheaf is just a functor

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:52):

It takes an open set to a type

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:52):

I could easily replace its value on X with some gigantic type that maps to the old value

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:53):

If you think of them as sheaves of functions then injectivity may well be obvious

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:53):

but this is a true pi type -- it takes an open set to a random type, not functions on U or anything

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:54):

and res is part of the data, not restriction of functions

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:55):

So are you interested in putting this presheaf and sheaf stuff in mathlib?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:55):

I'm not bothered either way

view this post on Zulip Mario Carneiro (May 27 2018 at 15:55):

but it is compositional

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:55):

yes but that's an axiom

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:55):

one of the two axioms of functor

view this post on Zulip Mario Carneiro (May 27 2018 at 15:55):

Of course, I'm assuming it's a presheaf already

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:55):

gotcha

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:56):

I don't know whether I should bother tidying everything up

view this post on Zulip Mario Carneiro (May 27 2018 at 15:56):

I mean the condition of being a sheaf can be stated more directly given it's a presheaf

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:56):

right

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:56):

but you still don't get injectivity for free

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:56):

because I can replace F X

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:56):

with with a random type Y that mapped to the old F X

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:57):

X the whole space

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:57):

and then it's still a presheaf

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:57):

but there's no reason Y -> old F X is injective

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:57):

so I broke the sheaf property precisely by breaking injectivity

view this post on Zulip Sean Leather (May 28 2018 at 06:40):

@Kevin Buzzard Re: @[simp] and left-to-right rewriting, perhaps, by browsing through the @[simp] theorems in this file, you can get an idea of why they are structured the way they are.


Last updated: May 14 2021 at 18:28 UTC